User:GUAqwq/TCproof to Lambda calculus
One of my friend doubted whether lambda-calculus is Turing complete.So I proved it. Here's my solution:
Recursion
Y := λf.(λx.f(x x))(λx.f(x x))
=>Y f = f(Y f)
Boolean
True := λx y.x False := λx y.y NOT := λa.a False True AND := λa b.a b False
Pair
Binary pair:
Pair := λa b.λx.x a b
Ternary pair:
Fst := λx y z.x Mid := λx y z.y Lst := λx y z.z TP := λa b c.λs.s a b c
Natural Numbers
Declaration:
0 := λs z.z Inc := λx.λs z.s(x s z)
Comparation:
Cmp := λa b.Y (λf a b.AND (IsZero a) (IsZero b) Fst (AND (NOT (IsZero a)) (IsZero b) Mid (AND (IsZero a) (NOT (IsZero b)) Lst (f (Dec a) (Dec b) ))) ) a b EQ = λa b.Cmp a b True False False LT = λa b.Cmp a b False False True
P.S.: Cmp
was designed for more comparations, but only 2 of them were useful, and 4 were discarded.
Operations:
Add := λx y. x Inc y IsZero := λx.x (λn.False) True Dec := λx.x (λp.Pair (p False) (Inc (p False))) (Pair 0 0) True Mul := λa b.b (Add a) 0 Pow := λa b.b (Mul a) 1 Div := λa b.Y (λf a b.LT a b 0 (Inc (f (Sub a b) b))) a b Mod := λa b.Y (λf a b.LT a b a (f (Sub a b) b)) a b
Turing Machine
Tape
A Tape
corresponds to a binary pair (M, n)
, where M
stores the symbol string, and n
equals to card(symbol_set)
.
A Tape
should be able to be read and be write:
Get := λT x.Mod (Div (T True) (Pow (T False) x)) (T False) Set := λT x d. Pair (Add (Sub (T True) (Mul (Get T x) (Pow (T False) x))) (Mul d (Pow (T False) x ))) (T False)
Situations
A Situation
corresponds to a ternary pair (Tape, State, Pointer)
.
Transformations
Left := Dec Right := Inc Rule := λa x b y d. λR. λS.And (Eq a (Mid S)) (Eq x (Get (Fst S) (Lst S))) (TP (Set (Fst S) (Lst S) y) b (d (Lst S))) (R S)
By chaining Rule
s together, we got a transforming-sheet to our Turing machine.
R1(R2(R3(...(λx.x))))
P.S.: λx.x
is meaningless to our purpose, just made it whatever you like (maybe 114514
).
Looping & Halting
F
refers to the transforming-sheet.
halt
refers to halting state.
n
refers to the size of the symbol set.
M
refers to the default data to the tape.
Turing Machine := (Y λf.λS.Eq halt (Mid S) (Fst S) (f (F D))) (TP (Pair M n) 0 0)