// 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}

/ primitive recursion
r:{[f;g;x]$[*|x,:();g x,r[f;g]x-:(1_&#x),1;f x]}

one:o[s]z
one()

add:r[p 0]o[s]p 2
add 2 3

mult:r[z]o[add]@p'0 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;p 0)
not'2 0

lte:o[not]sub
lte'(2 3;3 3;4 3)

pow:r[one]o[mult]@p'0 2
pow 2 3

xmin:o[sub](p 1;o[sub]@p'1 0)
xmin'(2 4;4 2)

xmax:o[sub](add;min)
xmax'(2 4;4 2)

diff:o[add](sub;o[sub]@p'1 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 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:{[f;x](f x,;1+)/:0}

xdiv:m o[lte](o[mult](o[s]p 2;p 1);p 0)
xdiv'(15 3;15 4)

rem:o[sub](p 0;o[mult](p 1;xdiv))
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)