User:Jan jelo/TC proof to partial recursive function

From Esolang
Jump to navigation Jump to search

This article comes from my article in Zhihu.

define

zero function 

(Z x1 x2 x3...) = 0

successor function 

(S x) = x+1

projection 

((P m n) x1 x2...xn...xm) = xn

function compose 

((C f g1 g2...gm) x1 x2...xn) = (f (g1 x1 x2...xn)(g2 x1 x2...xn)...(gm x1 x2...xn))

primitive recursive 

((R h g) x1...x_n-1 0) = (h x1...x_n-1) (base case)
((R h g) x1...x_n-1 xn) = (g x1...x_n-1 (xn-1)((R h g) x1...x_n-1 xn-1)) (recursive case)

minimalization 

((M f) x1...xn) = the smallest A that makes (f x1...xn A) equals to 0

functions

additive function

add = (R (P 1 1)(C S (P 3 3)))

predecessor function

pred = (R Z (P 2 1))

subtraction function

sub = (R (P 1 1)(C pred (P 3 3)))

multiplication function

mul = (R Z (C add (P 3 1)(P 3 3)))

test if a number is zero

isZ = (R (C S Z) Z)

test if a number is less than or equal to another number

leq = (C isZ (C sub (P 2 1)(P 2 2)))

condition

if = (C (R (P 2 2)(P 4 1)) (P 3 2)(P 3 3)(P 3 1))

square

square = (C mul (P 1 1)(P 1 1))

square root

(C (R Z (C if (C leq (C square (C S (P 3 2)))(P 3 1))(C S (P 3 3))(P 3 3))) (P 1 1)(P 1 1))

pairing function 

pair = (C if (C leq (P 2 2)(P 2 1))(C add (C square (P 2 1))(P 2 2))(C sub (C add (C square (P 2 2))(C add (P 2 2)(P 2 2)))(P 2 1))))
q = (C add (C square (C sqrt (P 1 1)))(C sqrt (P 1 1)))
left = (C if (C leq (C q (P 1 1))(P 1 1))(C sub (C sqrt (P 1 1))(C sub (P 1 1)(C q (P 1 1))))(C sqrt (P 1 1)))
right = (C if (C leq (C q (P 1 1))(P 1 1))(C sqrt (P 1 1))(C sub (P 1 1)(C square (C sqrt (P 1 1)))))

eq

eq = (C mul (C leq (P 2 1)(P 2 2))(C leq (P 2 2)(P 2 1)))

proof

for any Minsky machine program,it can be encoded as a partial recursive function. First,encode counter A,counter B and instruction pointer IP as a natural number by using pair function. 

build = (C pair (P 3 1)(C pair (P 3 2)(P 3 3)))

Function A,B and IP are used to retrieve the values of corresponding counters,respectively. 

A = (C left (C right (P 1 1)))
B = (C right (C right (P 1 1)))
IP = left

encode the source program into the function next,it takes a natural number encoding the current state of the Minsky machine and return a natural number encoding the next state. for example,if source program is 

incA
incB
decA 1
incA
(line number start from 1)

the corresponding next function is 

(C if (C eq (C IP (P 1 1))(C S Z))(C build (C S (C IP (P 1 1)))(C S (C A (P 1 1)))(C B (P 1 1)))
(C if (C eq (C IP (P 1 1))(C S (C S Z)))(C build (C S (C IP (P 1 1)))(C A (P 1 1))(C S (C B (P 1 1))))
(C if (C eq (C IP (P 1 1))(C S (C S (C S Z))))
(C if (C isZ (C A (P 1 1)))(C build (C S Z) Z (C B (P 1 1)))(C build (C S (C IP (P 1 1)))(C pred (C A (P 1 1)))(C B (P 1 1))))
(C if (C eq (C IP (P 1 1))(C S (C S (C S (C S Z)))))(C build Z (C S (C A (P 1 1)))(C B (P 1 1)))(P 1 1)))))

then,function F takes a number t,returns a natural number encoding state of t-th step 

F = (R (C build (C S Z) Z Z)(C next (P 2 2)))

function isHalt is a predicate,it takes a number encoding the state of the Minsky machine,if the Minsky machine is halting,then returns 0,otherwise it returns a positive integer 

isHalt = IP
(since we use IP=0 to represent the halt state,function isHalt is function IP)

then,((M (C isHalt F))) will provide a number of steps taken by the Minsky machine when is halts(if it can halt). Apply F to this number,it will returns the natural number encoding the final state of the Minsky machine,we can use A and B to get value of counter A and counter B. For any Minsky machine program,it can be encoded as a partial recursive function,and Minsky machine is Turing complete,so partial recursive function is Turing complete.

Retrieved from "https://esolangs.org/w/index.php?title=User:Jan_jelo/TC_proof_to_partial_recursive_function&oldid=148414"