Binary successor: `n ↦ n+1`

Parent: examples

Idea: starting at the rightmost bit, flip trailing 1s to 0 (carrying), and the first 0 (or blank) to 1.

The 7-tuple (Q, Γ, b, Σ, δ, q₀, F).

Q = {carry, done}; q₀ = carry; F = {done}.
Γ = {0, 1, b} (b = blank); Σ = {0, 1}.
δ — the "guide book":

δ(carry, 1) = (carry, 0, L)     a trailing 1 becomes 0, keep carrying left
δ(carry, 0) = (done,  1, R)     first 0 absorbs the carry -> 1, stop
δ(carry, b) = (done,  1, R)     ran off the left (e.g. 11 -> 100): blank -> 1

Trace on input 1011 (= 11), head on the rightmost bit (^ = head; state on the left):

carry:  1 0 1 1        scanned Γ-symbol = 1
              ^        look up δ(carry,1)=(carry,0,L)   [uses δ + Q]
carry:  1 0 1 0        wrote 0 (Γ); moved L; stayed carry (Q)
            ^
carry:  1 0 1 0        scanned 1  ->  δ(carry,1)=(carry,0,L)
            ^
carry:  1 0 0 0        wrote 0; moved L
          ^
carry:  1 0 0 0        scanned 0  ->  δ(carry,0)=(done,1,R)
          ^
done:   1 1 0 0        wrote 1; moved R; entered done
            ^

done ∈ F → halt. Output 1100 = 12. ✓

Which component acts, per step: the head + Γ give the scanned symbol → δ + Q pick the action → Γ is written, the {L,R} direction moves the head, Q updates → halting is the F test.

As code — idiomatically Haskell

A TM's δ is literally a pattern-matched function, Q/Γ/{L,R} are algebraic data types, and the tape is a list zipper (left-reversed, current, right). The transition table maps one-to-one onto the clauses:

data St = Carry | Done deriving Eq
data Mv = L | R

-- delta: each rule of the table is one pattern-match clause
delta :: St -> Char -> (St, Char, Mv)
delta Carry '1' = (Carry, '0', L)   -- trailing 1 -> 0, carry left
delta Carry '0' = (Done,  '1', R)   -- first 0 -> 1, stop
delta Carry _   = (Done,  '1', R)   -- blank -> 1 (ran off the left)

-- tape zipper: ls is the left half reversed, c the scanned cell, rs the right
run :: St -> [Char] -> Char -> [Char] -> [Char]
run Done ls c rs = reverse ls ++ c : rs                 -- F-test: halt
run q    ls c rs =
  let (q', w, m) = delta q c                            -- look up delta
  in case m of                                          -- write w, then move
       L -> case ls of (l:ls') -> run q' ls'      l   (w:rs)
                       []      -> run q' []        'b' (w:rs)
       R -> case rs of (r:rs') -> run q' (w:ls)    r   rs'
                       []      -> run q' (w:ls)    'b' []

-- run Carry (reverse "101") '1' ""  ==>  "1100"   (11 + 1 = 12)

The clean fit is the point: δ = pattern matching, states = an ADT, the tape = a zipper — a Turing machine is a tiny functional program. Swap delta for another table and the same run executes a different machine — which is exactly the universal machine with δ as data.

Binary successor: n ↦ n+1

As code — idiomatically Haskell

Binary successor: `n ↦ n+1`