Hatter's Turing-completeness

An informal proof (almost)

Version 0.1, 2011-05-21.

Hatter's Turing-completeness can be proven by showing that any program in some other Turing-complete formalism can be mapped into a Hatter program. For such purpose we shall take NORMA, a somewhat obscure machine conceived by Richard Bird in 1976, and used to teach theory of computation in some Brazilian universities and about nowhere else.

NORMA has the advantage of being much more similar to modern architectures than the Turing machine or the lambda calculus. It is a machine with infinite registers capable of holding naturals of infinite size (though it can be proven that only two registers are needed for Turing-completeness), and an instruction set with two operations (incrementing and decrementing a register) and one test (check whether a register is zero). Programs for NORMA can be represented in many equivalent ways; we shall choose to represent them as a set of the following commands:

(label, inc, reg, next)	Increments the register reg and jumps to the label next
(label, dec, reg, next)	Decrements the register reg and jumps to the label next
(label, zerop, reg, iftrue, iffalse)	If reg is zero, jumps to iftrue; otherwise, jumps to iffalse

Each program command must have a unique label. Execution begins with the command labeled main, and finishes when a jump is made to a non-existing label (we shall use end for this purpose).

Registers can be mapped to hats, initialized to contain a 0 in their argument stack. Each program command can be mapped to an individual hat with the same name as the label, whose inmagic performs the corresponding operation. The inmagic can be written as follows:

NORMA	Hatter
(label, inc, reg, next)	reg->[succ->reg]->next
(label, dec, reg, next)	reg->[pred->reg]->next
(label, zerop, reg, iftrue, iffalse)	reg->[horn->reg]->[[if<-\iftrue]<-\iffalse]->apply<-0

Jumping to end can be done by doing nothing (which can be accomplished by invoking nop); the stack will be unwound and the program will end.

Of course, this mapping does not result in idiomatic Hatter programs (as much as it makes sense to talk about idiomatic Hatter), and for sufficiently large programs would probably overflow the execution stack, but this is not of concern for the proof. What is of concern is that Hatter values are of fixed size, while NORMA registers can hold any natural. This can be overcome by storing more than one value on each hat, which turns pred, succ and horn in the above mapping into something more complicated. This modification is left as an exercise to the reader.