A LambdaCalculus 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 lambdaterm. Fortunately, I have a lambda computer
(even if it is a bit broken, segfaults, not logic).
So straight in, some standard stuff and listhandling terms, since we're going to use lists to represent the tape:
K = \xy.x
F = \xy.y
_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 sublists containing the left and right sides of the tape w.r.t. the read/write head. As such,
the lefthand 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 lambdacalculus Turing machine. Extra bits:
 lambdarc resource file with all the relevant definitions (and some irrelevant).
 typescript of the betareduction for the result.
Deficiencies: the representation of the program isn't ideal, but it should be possible to define a listbased representation of the machine's program (if you really wanted to!).
