$\newcommand{\ensN}{\mathbb{N}}$ $\newcommand{\deffunctionNkN}[3]{\begin{array}{lll}\mathbb{N}^{#1} & \rightarrow & \mathbb{N} \\ #2 & \mapsto & #3 \end{array}}$ $\newcommand{\defcase}[1]{\left\{\begin{array}{l}#1\end{array}\right.}$ $\newcommand{\set}[1]{\left\{#1\right\}}$

Theory of recursive functions

Author: François Schwarzentruber

Primitive recursive functions

Syntax Semantics
nul Nul function
succ Successor function
projection(i,n) $\deffunctionNkN n {(x_1, \dots, x_n)} {x_i}$
composition($g$, $h_1$, ... $h_n$) $\deffunctionNkN k {\vec x} {g(h_1(\vec x), \dots, h_n(\vec x))}$

where:
  • all functions $h_1, \dots, h_n$ are interpreted as functions from $\mathbb{N}^k$ into $\mathbb{N}$
  • $g$ is interpreted as a function from $\mathbb{N}^n$ into $\mathbb{N}$
rec($g$, $h$) $f : \ensN^{\ell+1} \rightarrow \ensN$ defined by

$f(\vec x, k) = {\defcase{g(\vec x) \text{ if $k = 0$} \\ h(\vec x, k-1, f(\vec x, k-1)) & \text{if $k > 0$} } }$

where:
  • $g$ is interpreted as a function from $\mathbb{N}^\ell$ into $\mathbb{N}$
  • $h$ is interpreted as a function from $\mathbb{N}^{\ell+2}$ into $\mathbb{N}$
Remark: we write projection(i) instead of projection(i,n).

Primitive recursive functions as Javascript functions


function nul(x) {
	return 0;
}


function succ(x) {
	return x+1;
}


function projin(x1, ..., xn) {
	return xi;
}


function comp_f_g1_gk(x_1, ... x_n) {
	return f(g1(x_1, ..., x_n), ...gk(x_1, ..., x_n));
}

function rec_f_g(x_1, ..., x_n, k) {
	var r = f(x_1, ..., x_n);

	for(var i = 1; i <= k; i++)
		r = g(x_1, ..., x_n, i-1, r);

	return r;
}

My first examples

Syntax Semantics
composition(succ, composition(succ, composition(succ, nul))) Function that always returns 3
composition(succ, composition(succ, projection(1))) $n \mapsto n+2$
composition(succ, composition(succ, composition(succ, composition(succ, projection(2))))) $(x_1, x_2) \mapsto x_2+4$

My first example using recursivity: plus

Syntax Semantics
plus = rec(proj(1), o(succ, proj(3))) $+ : \ensN^2 \rightarrow \ensN$ defined by
  • $+(x, 0) = g(x, 0) = x$;
  • $+(x, k) = h(x, k-1, +(x, k-1)) = 1+(x, k-1)$ if $k > 0$.
 

function proj11(x) {
	return x;
}

function proj33(x1, x2, x3) {
	return x3;
}

function succ(x) {
	return x+1;
}

function g(x1, x2, x3) {
	return succ(proj33(x1, x2, x3);
}

function plus(x, n) {
	var r = proj11(x);

	for(var i = 1; i <= n; i++)
		r = g(x, i-1, r);

	return r;
}

Other examples using recursivity

Syntax Semantics
mult = rec(nul, o(plus, proj(1), proj(3))) $\times$
puiss = rec(un, o(mult, proj(1), proj(3))) ^
pred = rec(nul, proj(1)) $n \mapsto \defcase{0 & \text{if $n=0$} \\ n-1& \text{if $n>0$}}$
diff = rec(proj(1), o(pred, proj(3))) -
mod2 = rec(nul, o(diff, un, proj(2))) mod2
div2 = rec(nul, o(plus, proj(2), o(mod2, proj(1)))) div2

Comparisons and Boolean operations

Syntax Semantics
sign = rec(nul, un) $n \mapsto \defcase{0 & \text{if $n=0$} \\ 1 & \text{if $n > 0$}}$
sup = o(sign, diff) >
inf = o(sup, proj(2), proj(1)) <
and = mult
or = o(sign, plus)
not = o(diff, un, proj(1))
leq = o(not, sup) $\leq$
geq = o(not, inf) $\geq$
equal = o(and, leq, geq) =

If-then-else

Syntax Semantics
ifthenelse( $cond$, $f_1$, $f_0$)
= o(plus, o(mult, $cond$, $iftrue$), o(mult, o(not, $cond$), $iffalse$)) 		$\deffunctionNkN k {\vec x} {\defcase{f_1(\vec x) & \text{ if $cond(\vec x) = 1$} \\ f_0(\vec x) & \text{ if $cond(\vec x) = 0$} }}$

Syntax Semantics
max = ifthenelse(geq, proj(1), proj(2)) Maximum of two numbers

Bounded minimization

Syntax Semantics
mubounded$\ell+1$($q$)
= rec(ifthenelse( o(q, proj(1) /*, ...., proj($\ell$)*/, nul), nul, o(succ, nul)), ifthenelse( o(leq, proj(3), proj(2)), /*si le plus petit i est <= k-1 (déjà atteint)*/ proj(3), /*on retourne la valeur calculée*/ ifthenelse( o(q, proj(1) /*, ...., proj($\ell$)*/, o(succ, proj(2))), o(succ, proj(2)), o(succ, o(succ, proj(2))) ) ) ) 		$\deffunctionNkN {\ell+1} {\vec x, m} {\defcase{\text{the smallest $i \in \set{0, \dots, m}$ such that $q(\vec x, i) = 1$} \\ m+1 \text{ if such that a $i$ does not exist} }}$

where $q : \ensN^{\ell+1} \rightarrow \{0, 1\}$.

Syntax Semantics
mubounded2(o(leq, proj(1), o(mult, o(succ, o(succ, o(succ, nul))), proj(2)))) the function: $\deffunctionNkN {2} {x, m} {\defcase{\text{the smallest $i \in \set{0, \dots, m}$ such that $x \leq 3\times i$} \\ m+1 \text{ if such that a $i$ does not exist} }}$

Pairing

$\newcommand\pair{pair}$ $\newcommand\decodeun{first}$ $\newcommand\decodedeux{second}$
Syntax Semantics
pair (see the definition in the course) $\pair : \ensN^2 \rightarrow \ensN$ that encodes pairs of integers as one integer
first (see the definition in the course) $\decodeun : \ensN \rightarrow \ensN$ gives the value $x_1$ from $\pair(x_1, x_2)$
second (see the definition in the course) $\decodedeux : \ensN \rightarrow \ensN$ gives the value $x_2$ from $\pair(x_1, x_2)$

Application 1: showing that Fibonnacci's function is primitive recursive

Our goal is to prove that the following function $fib : \ensN^2 \rightarrow \ensN$ is recursive primitive:
We reformulate it via pairing and obtain the following recursive scheme: We get $fib(n) = \decodeun(g(n))$.

Application 2: lists of integers

Syntax Semantics
nil = nul function that returns the empty list
cons = o(plus, one, o(pair, proj(1), proj(2))) constructor: function that takes (x, L) as input, returns the list x::L
head = o(first, pred) function that takes L as input and returns the head of L
tail = o(second, pred) function that takes L as input and returns the tail of L

Recursive functions

We add the pattern of unbounded minimization.
Syntax Semantics
mu($q$) $\deffunctionNkN {\ell} {\vec x} {\defcase{\text{the smallest $i \in \ensN$ such that $q(\vec x, i) \neq 0$} \\ \bot \text{ if such that a $i$ does not exist} }}$

where $q : \ensN^{\ell+1} \rightarrow \{0, 1\}$.

Ex: mu(function(n, i) {if(i>2*n) return 1; else return 0;})(5) is 11

Unbounded minimisation in Javascript


function muq(x1, ... xn) {
	var i = 0;
	while(q(x1, ...xn) == 0)
		i++;
	return i;
}