// stephen cole kleene: INTRODUCTION TO METAMATHEMATICS, chapter IX, section $44 // primitive recursive functions = basic operations + composition + primitive recursion // general recursive functions = primitive recursion + minimization / basic operations: zero, project, constant, successor z:{0} p:{y x} c:{y} s:1+ / compose o:{x y@\:z} One:o[s][z] One() / primitive recursion r:{{y z,x}/[x@*|z;y;|1_ z:|(-1_ z),/:!1+*|z,:!0]} Add:r[p[0]][o[s][p[2]]] Add 2 3 Mult:r[z][o[Add][(p[0];p[2])]] Mult 2 3 Pred:r[z][p[0]] Pred 10 Sub:r[p[0]][o[Pred][p[2]]] Sub 5 2 Not:o[Sub][(One;c[0])] Not'2 0 Lte:o[Not][Sub] Lte'(2 3;3 3;4 3) Pow:r[One][o[Mult][(p[0];p[2])]] Pow 2 3 Min:o[Sub][(p[1];o[Sub][(p[1];p[0])])] Min'(2 4;4 2) Max:o[Sub][(Add;Min)] Max'(2 4;4 2) Diff:o[Add][(Sub;o[Sub][(p[1];p[0])])] Diff'(3 10;10 3) Sg:o[Not][Not] Sg'10 0 Eq:o[Not][Diff] Eq'(2 3;3 3;3 2) Gt:o[Not][Lte] Gt'(2 3;3 3;3 2) Gte:o[Not][o[Sub][(p[1];p[0])]] Gte'(2 3;3 3;3 2) Lt:o[Not][Gte] Lt'(2 3;3 3;3 2) And:o[Sg][Mult] And'(0 0;0 1;1 0;1 1) Or:o[Sg][Add] Or'(0 0;0 1;1 0;1 1) Fac:r[One][o[Mult][(o[s][p[0]];p[1])]] Fac 4 / minimization m:{(x y,)(1+)/0} Div:m[o[Lte][(o[Mult][(o[s][p[2]];p[1])];p[0])]] Div'(15 3;15 4) Rem:o[Sub][(p[0];o[Mult][(p[1];Div)])] Rem'(15 3;15 4) \ base: add(x,0) = p[0]x rec : add(x,y+1) = s(add(x,y)) f: N^n -> N g: N^n+2 -> N h = r^n(f,g): N^n+1 -> N X = x1,..,xn base: h(X,0) = f(X) rec : h(X,y+1) = g(X,y,h(X,y)) a div b = least q s.t. (q+1)b > a f(a,b,q) = 1 if (q+1)b <= a 0 if (q+1)b > a f(a,b,q) = lte[mult[s[q],b],a] f = lte o[mult o[s o[p2],p1],p 0] f = o[lte](o[mult](o[s]p 2;p 1);p 0) \ 1 5 6 9 3 0 1 1 1 0 8 2 2 4 4 7 7 1 0 0 1 0 0 0 1 0 1 1 1 0 0 0 0 0 1 0 1 1 1 24 5 3 0 3 \ / recursive, iterative, reduce scan r:{:[*|z;y z,r[x;y]z-:|1,1_&#z;x z]} r:{r:,z;do[*|z;r,:,z-:|1,1_&#z];{y z,x}/[x@*|r;y;|1_ r]} r:{{y z,x}/[x@*|z;y;|1_ z:(*|z){x-|1,1_&#x}\z]}