A Lambda-Calculus Turing Machine

This is just for a bit of fun.. Moof was asking about (pure logic) formal definitions of Turing machines, which got me pondering a bit. I think that a lambda definition of a turing machine should do the job, though it'll be a wacky lambda-term. Fortunately, I have a lambda computer (even if it is a bit broken, segfaults, not logic).

So straight in, some standard stuff and list-handling terms, since we're going to use lists to represent the tape:

  # true and false
  K = \xy.x
  F = \xy.y

  # list building and smashing
  _cons = \xys.(sxy)
  _nil = \x.K
  _hd = \p.(p K)
  _tl = \p.(p F)

The tape is represented as a list consisting of the symbol under the read/write head, and two sub-lists containing the left and right sides of the tape w.r.t. the read/write head. As such, the left-hand side of the tape is 'backwards', e.g. the tape "1,2,3,4", with the read/write head over the "3", would be something like: "[3,[[2,1],[4]]]". In the lambda computer, we'll represent the tape "1,1,0", with the read/write head at the start of the tape (over the first "1"):

  _turtape = ("cons" '1 ("cons" "nil" ("cons" '1 ("cons" '0 "nil"))))

Reduced to a normal form this gives the expression:

  (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x)))))))))

To start with, we could use some functions that allow us to read and write the tape, and extract the left and right sides separately:

  _leftsym = \t.("hd" ("hd" ("tl" t)))
  _rightsym = \t.("hd" ("tl" ("tl" t)))
  _lefttape = \t.("hd" ("tl" t))
  _righttape = \t.("tl" ("tl" t))

  _readsym = \t.("hd" t)
  _writesym = \st.("cons" s ("cons" ("lefttape" t) ("righttape" t)))

The "readsym" function just produces the symbol, the "writesym" function produces a new tape with the changes (fairly straightforward). The next thing we need are two functions which can move the tape left and right:

_tapeleft = \t.("cons" ("rightsym" t) ("cons" ("cons" ("readsym" t) ("lefttape" t)) ("tl" ("righttape" t))))
_taperight = \t.("cons" ("leftsym" t) ("cons" ("tl" ("lefttape" t)) ("cons" ("readsym" t) ("righttape" t))))

This is where things start getting a little less obvious.. The normal forms of these aren't too crazy (pasted from the interpreter):

(\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y))))))
== tapeleft

(\ts.(s t (\xy.y) (\xy.x) (\xy.x) (\s.(s t (\xy.y) (\xy.x) (\xy.y) (\s.(s t (\xy.x) (t (\xy.y) (\xy.y))))))))
== taperight

Now we're about ready to try and write a machine that does something with the tape. In this example, something which reads two numbers from the tape and writes their sum to the next position. If we start with the tape "1,1,0" positioned at the first item, we should end up with the tape "1,1,2" positioned at the last item. Here's the program which does that:

  _churchadd = \xy.((\mnsz.(m s (n s z))) x y)

  _addadjacent = \t.("churchadd" ("readsym" t) ("readsym" ("tapeleft" t)))
  _turprogram = \t.("writesym" ("addadjacent" t) ("tapeleft" ("tapeleft" t)))

The result tape ought to be:

  _resulttape = ("cons" '2 ("cons" ("cons" '1 ("cons" '1 "nil")) "nil"))

So, we should be able to evalulate the program '("turprogram" "turtape")' and end up with something alpha equivalent to "resulttape". Here's the raw program and its input in lambda:

  ((\t.((\sta.(a s (\s.(s t (\xy.y) (\xy.x) (t (\xy.y) (\xy.y)))))) (\t.((\xy.((\mnsz.(m s (n s z))) x y))
    (\t.(t (\xy.x))) t ((\t.(t (\xy.x))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x))))
    (t (\xy.y) (\xy.y) (\xy.y)))))) t)))) t ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x))))
    (t (\xy.y) (\xy.y) (\xy.y)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x))))
    (t (\xy.y) (\xy.y) (\xy.y)))))) t)))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))))
  == ("turprogram" "turtape")

And once we reduce this:

  (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) (\xxy.x)))))
  == resulttape

So, yay! There it is: one plus one equals two on a lambda-calculus Turing machine. Extra bits:

Deficiencies: the representation of the program isn't ideal, but it should be possible to define a list-based representation of the machine's program (if you really wanted to!).

Last modified: 2007-08-06 08:58:23.000000000 +0100 by Fred Barnes.