(* Évaluation en `0` *)
let fonction1 = fun f -> f 0
(* Même fonction ; syntaxe différente *)
let fonction2 f = f 0
(* Somme de deux fonctions *)
let fonction3 f g = fun x -> (f x) + (g x)
(* Même fonction ; syntaxe différente *)
let fonction4 f g x = (f x) + (g x)
(* Ajoute l'identité à une fonction qui doit alors être de type int -> int *)
let fonction5 = fonction3 (fun x -> x)
(* Identité fonctionnelle *)
let fonction6 = fun f -> fun x -> f x
(* Même fonction ; syntaxe différente *)
let fonction7 f = fun x -> f x
(* Même fonction ; syntaxe différente *)
let fonction8 f x = f x
let compose f g = fun x -> f (g x)
(* Autre syntaxe *)
let compose f g =
let f_o_g x =
f (g x)
in
f_o_g
(* 1. et 3. *)
let add x y = x + y
(* 2. *)
let evaluation_en_zero f = (f 0) + 0
let f1 n m = if n = m then n else m
let f2 x y = let z = x + 1 in y || z > 10
let f3 x y = x y
f3
est l'identité fonctionnelle, c'est-à-dire l'identité, mais qui ne peut s'appliquer que sur des fonctions. C'est aussi la fonctionnelle "application" qui prend en entrée une fonction f
et un élément x
et qui renvoie l'évaluation (au sens mathématique) de f
en x
.
let f4 x y z = (x y) z
f4
est encore l'identité, mais pour des fonctions avec trois flèches (au moins) et c'est aussi la fonction "application" d'une fonction à deux arguments (curryfiée).
let f5 x y z = x (y z)
Avec f5
on retrouve la composition de fonctions $(f, g) \rightarrow f \circ g$
let f6 x y z = x y z
f6
est exactement f4
, sans les parenthèses implicites.
let f7 (x, y, z) = fun x -> (x, y, z)
Que l'on peut réécrire plutôt :
let f7 (x, y, z) = function t -> (t, y, z)
let max3 x y z = (max max x) y z
Observer bien le type de la fonction. Il faut que le premier argument soit du même type que max
.
max3 55 0 42
Il faut donc lui fournir une fonction de ce même type :
max3 min 0 42
Mais on ne peut pas comparer les valeurs fonctionnelles, Caml ne sait pas comparer des fonctions, la fonction max3
est inutilisable.
Bien entendu, ce que l'on voulait était :
let max3 x y z = max (max x y) z
max3 55 0 42
let rec composition f n =
if n = 0 then
fun x -> x
else
fun x -> (f ((composition f (n - 1)) x))
C'est la fonctionnelle qui calcule la composée $n$-ième : $f \rightarrow f^n$.
let add1 (x, y) = x + y
let add2 x y = x + y
let uncurry f (x, y) = f x y
let add1_bis = uncurry add2;;
add1_bis (3, 4);;
let curry f x y = f (x, y)
let add2_bis = curry add1
add2_bis 41 1
let rec nombre_chiffres n =
if n < 10 then
1
else
1 + nombre_chiffres (n / 10)
nombre_chiffres 5;;
nombre_chiffres 15;;
nombre_chiffres 123456789;;
On montre par récurrence (forte) sur $n$ dans $\mathbb{N}$ que la fonction termine et renvoie le bon résultat.
Autre version avec accumulateur, récursive terminale :
let nombre_chiffres n =
(* accu + le nombre de chiffres de n = constant *)
let rec nb_chiffres_aux n accu =
if n < 10 then
accu + 1
else
nb_chiffres_aux (n / 10) (accu + 1)
in
nb_chiffres_aux n 0
let rec mult_russe a b =
if a = 0 then
0
else if a mod 2 = 0 then
mult_russe (a / 2) (2 * b)
else
b + (mult_russe (a - 1) b)
mult_russe 3 27
Montrons par récurrence (forte) sur $a \in \mathbb{N}$ que cette fonction se termine et renvoie le produit de $a$ par $b$. Si $a = 0$, il n'y a pas de problème de terminaison et le résultat renvoyé est bien celui escompté. La propriété est donc vraie au rang $0$. Soit $a \geq 1$, tel que la propriété est vraie pour tout $n < a$. Montrons que la propriété est vraie au rang $a$ également. Comme $a \geq 1$, on rentre dans l'un des deux derniers else
. Si $a$ est pair, $a / 2$ est un entier naturel strictement inférieur à $a$ et, par hypothèse de récurrence, l'appel récursif sur $(a / 2)$ et $(2 \times b)$ termine et renvoie $(a / 2) \times (2 \times b) = ab$. Sinon $a - 1$ est aussi un entier naturel strictement inférieur à $a$, et par hypothèse de récurrence, l'appel sur $(a - 1)$ et $b$ termine et renvoie $(a - 1)b$. En ajoutant $b$ à ce résultat on trouve encore $ab$. Dans les deux cas la conditionnelle termine et renvoie $ab$ et la propriété est donc vraie au rang $a$. D'après le principe de raisonnement par récurrence la propriété est ainsi vraie pour tout $a \in \mathbb{N}$.
Bien sûr, cette preuve est élémentaire et on ne fera pas toujours les récurrences lorsqu'elles sont aussi simples. Il faudra cependent bien dire que les appels récursifs se font sur une valeur strictement inférieure (ici $a / 2$ et $a - 1$) et atteignent bien l'un des cas de base. Pour la correction, on explicitera au moins très clairement l'hypothèse qui serait démontrée par récurrence.
Voici une autre manière de faire en utilisant une fonction auxiliaire et un accumulateur :
let mult_russe_bis a b =
(* Diminue a en assurant ab + r constant *)
let rec aux a b r =
if a = 0 then
r
else if a mod 2 = 0 then
aux (a / 2) (2 * b) r
else
aux (a - 1) b (r + b)
in
aux a b 0
mult_russe_bis 3 27
let rec u n =
if n = 0 then
1.
else
sqrt((u (n - 1)) *. (v (n - 1)))
and v n =
if n = 0 then
2.
else
(u (n - 1) +. v (n - 1)) /. 2.
u 10 = v 10
L'arrondi des flottants et la convergence (rapide) des deux suites vers une même limite fait que le résultat de Caml est le même pour u_10
et v_10
, en tout cas sur cette machine.
let suites a b =
let rec u n =
if n = 0 then
a
else
sqrt((u (n - 1)) *. (v (n - 1)))
and v n =
if n = 0 then
b
else
(u (n - 1) +. v (n - 1)) /. 2.
in
(u, v)
let u, v = suites 1. 2. in u 10, v 10
let termes a b n =
let u, v = suites a b in
(u n, v n)
Attention, ce n'est pas du tout efficace ! Voyez-vous pourquoi ?
termes 1. 100. 10;;
termes 2. 487. 10;;
termes 500. 501. 10;;
let rec f n =
(n = 0) || g (n - 1)
and g n =
(n <> 0) && f (n - 1);;
f
teste si $n$ est pair et g
si $n$ est impair. Si $n < 0$, les fonctions ne terminent pas.
f 11;;
f 12;;
g 57;;
g 0;;
let rec f n =
if n = 0 then 1 else 3 + g (n - 1)
and g n =
if n = 0 then 0 else 1 + f (n - 1);;
f n
renvoie $2n + 1$ et g n
renvoie $2n$. Si $n < 0$, les fonctions ne terminent pas.
f 3;;
g 6;;
let rec f m n =
if m = 0 then
n
else
g (m - 1) (n + 1)
and g m n =
if m = 0 then
n
else
(f (m - 1) n) + 1
f m n
et g m n
renvoient $n + m$. Si $m < 0$, les fonctions ne terminent pas. En revanche $n$ peut être un entier relatif ici.
f 3 4;;
g 23 (-14)