A Turing Machine

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

turing.js · 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 eyecode: the machine

// t([State, Read, Write, Move], NextState). State 0 scans right over the
// digits; state 1 adds one: a 1 becomes 0 and the carry moves left, a 0 or a
// blank becomes 1 and the machine halts.
fact(start('add1', 0))
fact(t([0, 0, 0, 'r'], 0))
fact(t([0, 1, 1, 'r'], 0))
fact(t([0, '#', '#', 'l'], 1))
fact(t([1, 0, 1, 's'], 'halt'))
fact(t([1, 1, 0, 'l'], 1))
fact(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 eyecode: the interpreter

// One step: look up the transition, write and move, then continue.
implied_by(
  find(State, Left, Cell, Right, OutTape),
  [
    t([State, Cell, Write, Move], Next),
    move(Move, Left, Write, Right, A, B, C),
    struct('continue', Next, A, B, C, OutTape),
  ],
)

// In state halt, put the tape back together; in any other state, take
// another step.
implied_by(
  struct('continue', 'halt', Left, Cell, Right, OutTape),
  [reverse(Left, R), append(R, [Cell, ...Right], OutTape)],
)
implied_by(
  struct('continue', State, Left, Cell, Right, OutTape),
  [not_unify(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'. (continue is a reserved word in JavaScript, so that step is written as struct('continue', ...).) [Cell, ...Right] is the list whose first element is Cell, followed by the elements of Right.

The tape is held in three parts: the cells to the left of the head (in reverse order, nearest first), the cell under the head, and the cells to the right. Moving off either end of the tape reaches a fresh blank cell. These interpreter rules work for any instruction table, not just this one.

What eyecode 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 just past the last digit, which the machine visited; it is not a digit.

Why: the proof in plain words

For 101001, the proof records every move:

  1. Start in state 0, reading the first 1. Rule t([0, 1, 1, 'r'], 0): keep the 1, move right.
  2. Read 0: keep it, move right. … and so on to the blank at the end.
  3. At the blank, switch to state 1 and step left.
  4. Read 1: write 0, step left (the carry).
  5. 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.

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

Try it

eyecode examples/turing.js            # the answers
eyecode --proof examples/turing.js    # answers with their proof

Or open it in the playground. Add query(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.