Exploring the Turing Completeness of Push

[yaskovdev]

Good afternoon,

I’m writing an article about Push, and I noticed that #102 updates the README.md to state that Push is Turing-complete. However, I couldn’t find a formal proof supporting this claim. Could you kindly share any details or references regarding the proof?

Thank you in advance for your assistance!

[lspector]

Hi Sergey, I don’t know if anyone has filled in a proof but I think it should be pretty straightforward. The two issues would be storage and control. At least if you include the yank and shove instructions, which provide random access to stacks, each stack can be treated as an unbounded random-access tape. Actually, I think you could get by without those, since I think you can use a pair of stacks also to simulate an unbounded tape. With respect to control, there are a variety of instructions that can be used implement arbitrary conditionals and loops. One could use the combinators and/or combinations of exec_if and built-in looping instructions. And you could probably build a lot of the necessary control out of exec versions of the generic stack-manipulation instructions. So I’m pretty confident that the claim is true, and that it shouldn’t be too hard to prove. That said, I’d love to see a proof! And maybe a discussion of which sets of instructions produce the most elegant proof. -Lee — Lee Spector (he/him) Chair, Department of Computer Science Class of 1993 Professor of Computer Science Amherst College https://www.amherst.edu/people/facstaff/lspector

…

On Dec 1, 2024, at 6:33 AM, Sergey Yaskov ***@***.***> wrote: Good afternoon, I’m writing an article about Push, and I noticed that #102 <#102> updates the README.md to state that Push is Turing-complete. However, I couldn’t find a formal proof supporting this claim. Could you kindly share any details or references regarding the proof? Thank you in advance for your assistance! — Reply to this email directly, view it on GitHub <#167>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAB4IGGMK5LDFCMPSZV44TL2DLXYHAVCNFSM6AAAAABSZSUKP2VHI2DSMVQWIX3LMV43ERDJONRXK43TNFXW4OZXGU4DONBQGU>. You are receiving this because you are subscribed to this thread.

[yaskovdev]

Hi Lee,

Thank you so much for your detailed response! It’s incredible to hear directly from the creator of Push.

I've implemented a 5-register Universal Register Machine (URM) interpreter in Push, which, given the URM's Turing-completeness, serves as a practical demonstration of Push's Turing-completeness as well. However, I'm not sure if it can be treated as a formal proof.

Leaving a link to the implementation here: https://gist.github.com/yaskovdev/71010ede2d070ed88c11334160fedc88, in case it may be of interest or useful for further discussions.