// 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:{x;0}
p:{y x}
c:{y}
s:1+

/ compose
o:{[f;g;x]f g@\:x}

One:o[s]z
One()

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

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;c 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

Min:o[Sub](p 1;o[Sub]p@/:1 0)
Min'(2 4;4 2)

Max:o[Sub](Add;Min)
Max'(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}

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)