Recursive functions
Open the console page of Firefox (Firefox, web developpment).
Primitive recursive functions
Here are the functions you can use:
You have access to projection(i) (or shortly proj(i)): it is the projection over the ith coordinate.
Ex: projection(2)(3, 4, 5, 22) is 4
projection(1)(3, 4, 5, 22) is 3
nul: it is the function that returns 0 whatever the arguments are
Ex: nul() is 0
succ: it is the successor function. It returns the argument where we added 1.
Ex: succ(5) is 6
composition(g, h1, ... hn), written shortly o(g, h1, ..., hn) is the function x |--> g(h1(x), ... hn(x))
Ex: composition(succ, projection(2)) is the function succ(projection(2)(x)). For instance, composition(succ, projection(2))(3, 30, 300, 3000) is succ(projection(2)(3, 30, 300, 3000) = succ(30) = 31.
recursivite(g, h), or shortly rec(g, h), where g has l arguments and h has l+2 arguments is the recursivity scheme applied with g and h and has l+1 arguments where:
g is the function to compute the basic case
h is the function to compute the recursive case.
More precisely:
rec(g, h)(n, 0) = g(n)
rec(g, h)(n, k+1) = h(n, k, f(n, k))
That is, g has l arguments. It corresponds to the first l arguments of rec(g, h). Arguments of h are:
the first l arguments of rec(g, h), the level of recursion k and the value already computed recursively.
Ex: f = rec(proj(1), h) where h = o(succ, proj(3)) is the function + that takes two arguments and returns the sum of them. Indeed, f(n, 0) = proj(1)(n) = n
f(n, k+1) = h(n, k, f(n, k)). But h takes the third argument, add one to it and returns the result. Thus, f(n, k+1) = f(n, k) + 1.
Unbound minimisation
mu(q) is the unbounded minimisation of the predicate q : N^{l+1} ---> {0, 1} and mu(q)(n) is defined as the smallest i such that q(n, i) = 1 and is undefined when there is no such i.
Ex: mu(function(n, i) {if(i>2*n) return 1; else return 0;})(5) is 11
Constructions
See source of this page.
We provide examples of primitive recursive functions: plus, mult, puiss, fact, pred, diff, and, not, or, sign, sup, inf, ifthenelse, leq, geq, equal, mod2...
For instance, the definition of plus is:
plus = rec(proj(1), o(succ, proj(3)));
Indeed, plus(n,0) = n (that is proj(1))
plus(n, k+1) = h(n, k, plus(n, k))
where h(x, y, z) = 1 + z (that is h = o(succ, proj(3)))