// 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, successor z:{0} p:{y x} s:1+ / compose o:{[f;g;x]*f((),g)@\:(),x} / next release: o:{[f;g;x]f g@\:x} / primitive recursion r:{[f;g;x]\$[*|x;g x,r[f;g]x-:|1,1_&#x;f x]} f.one:o[s]z f.one() f.add:r[p 0]o[s]p 2 f.add 2 3 f.mult:r[z]o[f.add]p@'0 2 f.mult 2 3 f.pred:r[z]p 0 f.pred 10 f.sub:r[p 0]o[f.pred]p 2 f.sub 5 2 f.not:o[f.sub](f.one;p 0) f.not'2 0 f.lte:o[f.not]f.sub f.lte'(2 3;3 3;4 3) f.pow:r[f.one]o[f.mult]p@'0 2 f.pow 2 3 f.min:o[f.sub](p 1;o[f.sub]p@'1 0) f.min'(2 4;4 2) f.max:o[f.sub](f.add;f.min) f.max'(2 4;4 2) f.diff:o[f.add](f.sub;o[f.sub]p@'1 0) f.diff'(3 10;10 3) f.sg:o[f.not]f.not f.sg'10 0 f.eq:o[f.not]f.diff f.eq'(2 3;3 3;3 2) f.gt:o[f.not]f.lte f.gt'(2 3;3 3;3 2) f.gte:o[f.not]o[f.sub]p@'1 0 f.gte'(2 3;3 3;3 2) f.lt:o[f.not]f.gte f.lt'(2 3;3 3;3 2) f.and:o[f.sg]f.mult f.and'(0 0;0 1;1 0;1 1) f.or:o[f.sg]f.add f.or'(0 0;0 1;1 0;1 1) f.fac:r[f.one]o[f.mult](o[s]p 0;p 1) f.fac 4 / minimization m:{[f;x](f x,)(1+)/0} f.div:m o[f.lte](o[f.mult](o[s]p 2;p 1);p 0) f.div'(15 3;15 4) f.rem:o[f.sub](p 0;o[f.mult](p 1;f.div)) f.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)