Turing machine in lambda calculus

turing.txt

; Church encodings for booleans, pairs, and lists

TRUE = λx.λy.x
FALSE = λx.λy.y
PAIR = λx.λy.λf.f x y
FST = λp.p TRUE
SND = λp.p FALSE
NIL = λc.λn.n
CONS = λh.λt.λc.λn.c h (t c n)
HEAD = λl.l (λh.λt.h) NIL
TAIL = λl.l (λh.λt.t) NIL
ISNIL = λl.l (λh.λt.FALSE) TRUE

; Church numerals

ZERO = λf.λx.x
ONE = λf.λx.f x
TWO = λf.λx.f (f x)
ISZERO = λn.n (λx.FALSE) TRUE
SUCC = λn.λf.λx.f (n f x)
PRED = λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)

; Tape encoding: (left, current, right)
; Symbols: 0 (ZERO), 1 (ONE), B (blank, ZERO)
TAPE = λleft.λcurrent.λright.PAIR left (PAIR current right)

; Head movement
MOVE_LEFT = λtape.λstate.
  ISNIL (FST tape) (TAPE NIL (FST (SND tape)) NIL) ; If left is empty, use blank
  (TAPE (TAIL (FST tape)) (HEAD (FST tape)) (CONS (FST (SND tape)) (SND (SND tape)))) state

MOVE_RIGHT = λtape.λstate.
  ISNIL (SND (SND tape)) (TAPE (CONS (FST (SND tape)) (FST tape)) ZERO NIL) ; If right is empty, use blank
  (TAPE (CONS (FST (SND tape)) (FST tape)) (HEAD (SND (SND tape))) (TAIL (SND (SND tape)))) state

; States

Q0 = λsymbol.λtape.
  ISZERO symbol (MOVE_RIGHT tape Q0) ; (q0, 0) -> (q0, 0, R)
  (ISZERO (SUCC symbol) (MOVE_LEFT tape Q1) ; (q0, B) -> (q1, B, L)
  (MOVE_RIGHT tape Q0)) ; (q0, 1) -> (q0, 1, R)

Q1 = λsymbol.λtape.
  ISZERO symbol (TAPE (FST tape) ONE (SND (SND tape)) QH) ; (q1, 0) -> (qh, 1, R)
  (ISZERO (SUCC symbol) (TAPE (FST tape) ONE (SND (SND tape)) QH) ; (q1, B) -> (qh, 1, R)
  (TAPE (FST tape) ZERO (SND (SND tape)) (MOVE_LEFT tape Q1))) ; (q1, 1) -> (q1, 0, L)

; Halt state returns tape
QH = λsymbol.λtape.tape

; Step function: applies one transition
STEP = λconfig.FST config (FST (SND config)) (SND config)

; Example tape: binary number 11 (3 in decimal), head at leftmost 1
; Tape: ([], 1, [1])
TAPE_EXAMPLE = TAPE NIL ONE (CONS ONE NIL)

; Run the Turing machine starting in q0
RUN = STEP (PAIR Q0 TAPE_EXAMPLE)