ACL2 Seminar, March 19, 2012

The Turing Equivalence of M1
J Strother Moore

Abstract: M1 is a ``toy'' machine used to teach undergraduates about the ACL2
formalization of the Java Virtual Machine.  M1 is a von Neumann style stack
machine.  The state consists of four components, a program counter, an array
of local variable values (akin to registers), a stack, and an execute-only
program.  The machine provides eight instructions for doing addition and
multiplication on the stack, moving items from the locals to the stack and
back, an unconditional jump and a conditional jump that tests the top of the
stack against 0.  M1 provides unbounded integers.  Because of this, M1 is
Turing equivalent: anything that can be done by a Turing machine can be done
by M1.  This was proved using ACL2.  The model of Turing machines used was
adapted from the 1984 Boyer-Moore paper ``A Mechanical Proof of the Turing
Completeness of PURE LISP,'' an Nqthm proof.  In the present project we
showed that the initial state symbol, tape, and Turing machine program can be
mapped to M1 resources and interpreted with an 800 instruction M1 program
about which we have proved (a) if the Turing machine runs forever, the M1
program runs forever, and (b) if the Turing machine stops with a tape t then
the M1 program stops with (the M1 representation of) tape t.