A Mechanical Proof of the Turing Completeness of Pure Lisp
Robert Boyer, J Strother Moore · Contemporary mathematics - American Mathematical Society · 1984
We describe a proof by a computer program of the Turing completeness of a computational paradigm akin to Pure LISP. That is, we define formally the notions of a Turing machine and of a version of Pure LISP and prove that anything that can be computed by a Turing machine can be computed by LISP. While this result is straightforward, we believe this is the first instance of a machine proving the Turing completeness of another computational paradigm. The work here was supported in part by NSF Grant MCS-8202943 and ONR Contract N00014-81-K-0634. 2 1. Introduction. In our paper [Boyer & Moore 84] we present a definition of a function EVAL that serves as an interpreter for a language akin to Pure LISP, and we describe a mechanical proof of the unsolvability of the halting problem for this version of LISP. We claim in that paper that we have proved the recursive unsolvability of the halting problem. It has been pointed out by a reviewer that we cannot claim to have mechanically proved the r...