Laconic
- This article is not detailed enough and needs to be expanded. Please help us by adding some more information.
| Designed by | Adam Yedidia |
|---|---|
| Appeared in | 2016 |
| Computational class | Turing-complete |
| Major implementations | [1] |
| Influenced | Not-Quite-Laconic |
Laconic is a programming language that compiles to a one-tape two-symbol Turing machine. The goal for its creation was to create two-symbol Turing machines with very few states (a golfed Turing machine) that does something interesting when started on a blank tape. Laconic is a strongly-typed language that supports recursive functions.
Complexity class
Laconic is believed to be Turing-complete.
The original theory studied with Laconic is SRP or "stationary Ramsey property", an extension of ZFC which includes a large cardinal with a particular structural Ramsey property.[1][2] Yedidia wrote a program which searches for contradictions in SRP:
Construction. There is a 7910-state 2-symbol Turing machine which halts if and only if SRP proves ~Con(SRP). (Yedidia, 2016)[3]
If SRP is consistent then SRP does not prove that Yedidia's machine does not halt. Also, if SRP is consistent then Yedidia's machine does not halt. Finally, if SRP is consistent then SRP does not prove that Yedidia's machine halts after some finite number of steps. In summary, if SRP is consistent then whether Yedidia's machine halts is independent of SRP; it's not a question that SRP can answer! This leads to an immediate limitation on what SRP can prove about the busy-beaver function.
Corollary (BB(7910) is independent of SRP). If SRP is consistent then no theorem of SRP implies that the busy-beaver function BB(k) = n for any finite n and any finite k ≥ 7910.
Additionally, since SRP is strictly more powerful than ZFC, this is a limitation on ZFC as well.
Theorem. SRP proves that Con(SRP) implies Con(ZFC). (Friedman, 2014)
Corollary (BB(7910) is independent of ZFC). If ZFC is consistent then no theorem of ZFC implies that the busy-beaver function BB(k) = n for any finite n and any finite k ≥ 7910.
See also
References
- ↑ H. M. Friedman, 2014. Order invariant graphs and finite incompleteness. https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/FIiniteSeqInc062214a-v9w7q4.pdf
- ↑ The k-SRP stationary Ramsey property, 2020. https://math.stackexchange.com/q/3528489
- ↑ A. Yedidia & S. Aaronson, 2016. A relatively small Turing machine whose behavior is independent of set theory. https://arxiv.org/abs/1605.04343