eyedia

A Turing Machine

The simplest model of a computer, adding one to a binary number, step by step.

turing.pl · output · proof · check · try it in the playground

The question

In 1936 Alan Turing described an imaginary machine: a long tape of cells, a head that reads and writes one cell at a time and moves left or right, and a small table of instructions. Anything a modern computer can calculate, such a machine can calculate too.

Here the machine adds one to a binary number (written with only 0 and 1).

What is 101001 + 1? And can we watch every move of the machine?

What we tell Eyedia: the machine

start(add1, 0).
t([0, 0, 0, r], 0).
t([0, 1, 1, r], 0).
t([0, #, #, l], 1).
t([1, 0, 1, s], halt).
t([1, 1, 0, l], 1).
t([1, #, 1, s], halt).

Each line reads: in state S, seeing symbol X, write Y, move (l)eft, (r)ight or (s)tay, and go to the next state. # is a blank cell.

State 0 runs right to the end of the number. State 1 walks back, turning 1s into 0s until it can turn a 0 (or a blank) into a 1: the carry.

What we tell Eyedia: the interpreter

find(State, Left, Cell, Right, OutTape) :-
    t([State, Cell, Write, Move], Next),
    move(Move, Left, Write, Right, A, B, C),
    continue(Next, A, B, C, OutTape).

continue(halt, Left, Cell, Right, OutTape) :- reverse(Left, R), append(R, [Cell|Right], OutTape).
continue(State, Left, Cell, Right, OutTape) :- State \= halt, find(State, Left, Cell, Right, OutTape).

An interpreter is a program that runs another program. This one looks up the instruction, moves the head, and repeats until the state is halt.

What Eyedia concludes

compute([1, 0, 1, 0, 0, 1], [1, 0, 1, 0, 1, 0, #]).
compute([1, 0, 1, 1, 1, 1], [1, 1, 0, 0, 0, 0, #]).
compute([1, 1, 1, 1, 1, 1], [1, 0, 0, 0, 0, 0, 0, #]).
compute([], [1, #]).

In everyday numbers: 41 + 1 = 42, 47 + 1 = 48, 63 + 1 = 64 (the number grows a digit), and an empty tape becomes 1. The trailing # is the blank cell the head stopped next to.

Why: the proof in plain words

For 101001, the proof records every move:

Start in state 0, reading the first 1. Rule t([0, 1, 1, r], 0): keep the 1, move right.
Read 0: keep it, move right. … and so on to the blank at the end.
At the blank, switch to state 1 and step left.
Read 1: write 0, step left (the carry).
Read 0: write 1, halt.

Each move names the instruction it used and the tape before and after.

Checked, not just claimed

The checker went through all four runs: 144 steps.

142 were matched to the exact instruction or program line they cite;
the 2 built-in tests (“state 0 is not halt”, “state 1 is not halt”) were recomputed by the checker itself;
no step depends on itself in a circle, and nothing is extra.

Verdict: checked. All 144 steps verified, nothing taken on trust.

Try it

node bin/eyedia.js examples/turing.pl
node bin/eyedia.js --proof examples/turing.pl

Or open it in the playground. Add true :+ compute([1, 0, 1, 1], _). and run again: you get compute([1, 0, 1, 1], [1, 1, 0, 0, #])., that is 11 + 1 = 12.

Takeaway

A Turing machine is computation at its barest. With a proof, every tick of it becomes something you can read, replay and check.

This site is open source. Improve this page.