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 Rules 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)

Q.E.D --GUAqwq (talk) 14:03, 6 September 2024 (UTC)