let a = 2;;
let f x = a * x;;
a vaut $2$ et c'est ceci qui est conservé pour toujours.
let a = 3 in f 1;;
La liaison locale, qui masque la liaison globale, n'est pas utilisée.
let a = 3;;
C'est une nouvelle liaison qui masque l'ancienne, mais ne change rien à f.
f 1;;
En programmation fonctionnelle (pure), le résultat d'une fonction est déterministe et ne peut pas dépendre de son contexte d'application. Nous verrons que ce n'est cependant pas le cas en Caml.
Il faut retenir que c'est bien la valeur de a et non l'identifiant "a" qui est utilisée lors de la définition de la fonction. Ceci est heureux, sinon il faudrait proscrire tous les noms de variables qui peuvent être utilisés dans des fonctions, sous peine de changer le comportement des fonctions sans même s'en rendre compte !
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 = x (x y);;
f4 est la fonction carré (au sens de la composition) : $f \rightarrow f \circ f$
let f5 x y = x (y x);;
let f6 x y z = (x y) z;;
C'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) sur ses deux arguments.
let f7 (x, y, z) = function t -> (t, y, z);;
let f8 f g x = f x + g x;;
f8 est la fonction qui renvoie la somme de deux fonctions à valeurs entières.
let f9 f g x = f (g x);;
f9 est la composition de fonctions que nous avons vue en cours : $(f, g) \rightarrow f \circ g$
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 (en général) les valeurs fonctionnelles, Caml ne sait pas comparer des fonctions (différentes), la fonction max3 est inutilisable sauf éventuellement avec max3 max y z, ce qui ne présente que peu d'intérêt.
Bien entendu, ce que l'on voulait était :
let max3 x y z = max (max x y) z;;
max3 55 0 42;;
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 composition f = function
| 0 -> (function x -> x)
| n -> (function x -> (f ((composition f (n - 1)) x)))
;;
C'est la fonctionnelle qui calcule la composée $n$-ième : $f \rightarrow f^n$.
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;;
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;;