3 ms·

To me, the use of Turing machines seems a little gimmicky; they're very far removed from the way we actually program, or reason about programs. The difficult pr

To me, the use of Turing machines seems a little gimmicky; they're very far removed from the way we actually program, or reason about programs. The difficult problem here seems to be compilation: going from a usable program definition, either formal or informal, down to the bizarre world of Turing machines, either by hand or automatically. To me, binary combinatory logic and binary lambda calculus seem like much more sensible languages for performing these kinds of algorithmic information theory experiments.

sp332 11y ago
The proof was actually written in Laconic, and then compiled down to a TM. We already know certain things about TMs (like busy beaver and the halting problem) so you don't have to re-prove those things about your new machine if you can just prove that it's equivalent to a TM. It's mainly used as a convenient way to keep score. If some other proof can be proven equivalent to a TM with fewer states, then you have a better upper bound.
tromp 11y ago
Scott commented on the Turing Machine vs lambda calculus approaches in: http://www.scottaaronson.com/blog/?p=2725#comment-1085117 http://www.scottaaronson.com/blog/?p=2725#comment-1085117 showing a clear preference for the "physical" operation of Turing Machines. In the end, complexities are not that far apart, considering that https://gist.github.com/anonymous/a64213f391339236c2fe31f8749a0df6 https://gist.github.com/anonymous/a64213f391339236c2fe31f874... describes a 27 state Goldbach checking TM, which takes no more than 378 bits to encode, while https://github.com/tromp/AIT/blob/master/goldbach.lam https://github.com/tromp/AIT/blob/master/goldbach.lam describes an equivalent 267 bit Lambda Calculus term, which can also be represented as this https://github.com/tromp/AIT/blob/master/goldbach.gif https://github.com/tromp/AIT/blob/master/goldbach.gif lambda diagram, as explained in http://tromp.github.io/cl/diagrams.html http://tromp.github.io/cl/diagrams.html

sp332 11y ago

The proof was actually written in Laconic, and then compiled down to a TM. We already know certain things about TMs (like busy beaver and the halting problem) so you don't have to re-prove those things about your new machine if you can just prove that it's equivalent to a TM. It's mainly used as a convenient way to keep score. If some other proof can be proven equivalent to a TM with fewer states, then you have a better upper bound.

tromp 11y ago

Scott commented on the Turing Machine vs lambda calculus approaches in: http://www.scottaaronson.com/blog/?p=2725#comment-1085117 http://www.scottaaronson.com/blog/?p=2725#comment-1085117 showing a clear preference for the "physical" operation of Turing Machines. In the end, complexities are not that far apart, considering that https://gist.github.com/anonymous/a64213f391339236c2fe31f8749a0df6 https://gist.github.com/anonymous/a64213f391339236c2fe31f874... describes a 27 state Goldbach checking TM, which takes no more than 378 bits to encode, while https://github.com/tromp/AIT/blob/master/goldbach.lam https://github.com/tromp/AIT/blob/master/goldbach.lam describes an equivalent 267 bit Lambda Calculus term, which can also be represented as this https://github.com/tromp/AIT/blob/master/goldbach.gif https://github.com/tromp/AIT/blob/master/goldbach.gif lambda diagram, as explained in http://tromp.github.io/cl/diagrams.html http://tromp.github.io/cl/diagrams.html