A Mechanical Proof of the Turing Completeness of Pure LISP.
Abstract
The authors describe a proof by a computer program of the Turing completeness of a computational paradigm akin to Pure LISP. That is, they 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, they believe this is the first instance of a machine proving the Turing completeness of another computational paradigm. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1983
- Accession Number
- ADA130625
Entities
People
- J. Strother Moore
- Robert S. Boyer
Organizations
- University of Texas at Austin