Sur le Lambda calcul
________________________

Avertissement : Ce texte est une compilation des sites : https://sourceforge.net/project/showfiles.php?group_id=31790
http://www.cis.upenn.edu/~hol/lamcr/
http://www.lip6.fr/http://www.lip6.fr/reports/IBP/Litp.1995.html
http://dept-info.labri.u-bordeaux.fr/HBib/AnLex.html
http://www.enseignement.polytechnique.fr/informatique/TC/polycopie-1.6/main002.html
http://www.mactech.com/articles/mactech/Vol.07/07.05/LambdaCalculus/
http://perso-info.enst-bretagne.fr/~brouty/Logique/lambdainv.html
http://www.lsv.ens-cachan.fr/~goubault/lambdaidx.html


Le Lamda calcul prend la notion de calcul à son début.
Il faut en particulier oublier ce qu’est une addition, oublier les notions de vrai ou de faux, oublier ce que sont les nombres ou les fonctions. Tout cela peut être redéfini à partir du Lamda calcul.

Mais pourquoi donc remettre en question ce que l’on sait déjà ?
Est-ce bien utile ?
Ce n’est certainement pas indispensable, puisqu’on peut utiliser dans la pratique des notions très élaborées, sans connaître la structure de leurs axiomes, en s’appuyant sur des théorèmes connus.

Ceci est vrai pour tous les domaines de l' informatique théorique qui fait appel à plusieurs théories imbriquées: logique et calculabilité, algorithmique et analyse d'algorithmes, conception et sémantique des langages de programmation, bases de données, principes des systèmes d'exploitation, architectures des ordinateurs et évaluation de leurs performances, réseaux et protocoles, langages formels et compilation, codes et cryptographie, apprentissage et zero-knowledge algorithms, calcul formel, démonstration automatique, conception et vérification de circuits, vérification et validation de programmes, temps réel et logiques temporelles, traitement d'images et vision, synthèse d'image, robotique, ...

Le Lamda-calcul sert à approfondir l’informatique théorique. Il se situe au niveau des machines de Türing.
On montre d’ailleurs que tout ce qui peut se calculer par ordinateur peut l’être par une machine de Turing ou par Lamda calcul.

***

Voici la syntaxe générative, simple et courte, des expressions de Lamda calcul :

<Expr> := <Ident> | <Constante> | Lambda<Ident>. <Expr> | (Expr) | <Expr><Expr>


Ce que l’on peut exprimer sous la forme suivante :

Une expression peut être un identifiant, une constante, une Lamda expression, une expression entre parenthèses ou deux expressions juxtaposées.
Une Lambda-expression représente une fonction. Elle commence par le symbole Lambda suivi du nom de la variable, d’un point et enfin de l'expression de la fonction formulée avec cette variable.

Le résultat de l'application de la fonction à une expression se note par simple juxtaposition :

Lamda <ident>. Expr Expr2
qui signifie que Expr2 vient remplacer <ident>  dans Expr
Le résultat obtenu en effectuant ce remplacement se note :

Expr[Expr2/ident]

est appelé Beta-Réduction de l'application

Exemple 1 :
(lambda n . n*2+3) 7
-->(n*2 + 3)[7/n] ( 7 doit remplacer n dans ce qui précède "[ ")
-->7*2 + 3 (le remplacement est fait)
-->14 + 3 (en informatique "*" tient lieu de signe de multiplication)
-->17

Le signe --> désigne  une "production" c'est à dire le résultat de l'étape suivante du calcul. Il y a production tant que l'on n'a pas atteint l'expression terminale qui doit être ici un nombre.



L'existence de plusieurs expressions successives est conforme à la syntaxe mais aussi elles doivent s'évaluer en groupant les expression par deux à partir de la gauche. Par exemple:
Expr1  Expr2  Expr3  Expr4
s'évalue :
(((Expr1 Expr2) Expr3) Expr4

Les applications sont donc associatives :  f x y = (f x)y


<Ident> peut ne pas figurer dans Expr ; dans ce cas l’application à Expr2  se réduit à Expr puisque cette dernière ne sera pas modifiée par un remplacement.

Les Lamba expressions  peuvent  s’imbriquer à plusieurs niveaux lorsque Expr comporte elle même des Lambda-expressions.


Les fonctions élémentaires n’ont qu’une variable : la variable spécifiée par ident. Pour définir des fonctions de plusieurs variables il suffit d’imbriquer plusieurs Lambda-expressions . Ainsi la fonctions de deux variables : x + y s'écrit avec la fonction PLUS:

Exemple 2:
La fonction identique, qui retourne un résultat identique à l' argument qui lui est fourni, s’écrit

Lambda x.x


où x est un identifiant.
Si on fournit à cette fonction comme argument l’identifiant “Pierre” on trouve que :

Lambda x.x “Pierre”
-->x["Pierre"/x]
-->“Pierre”

puisqu’il faut remplacer “Pierre” par “Pierre” dans “Pierre” !

L’exemple peut sembler une banale tautologie. Il permet cependant de voir fonctionner un lambda expression.

Exemple 3
Cette fois écrivons une fonction constante qui donne toujours comme résultat l'identificateur “Jacques”:

Lambda x.”Jacques”

car l'identifiant x ne se trouve pas dans l'identifiant "Jacques"

Mais il faut avoir préalablement défini Jacques comme un identifiant qui ne peut avoir comme contenu que lui-même et non une chaine de caractères :

<ident> := “Jacques”| "Pierre" | x


Exemple 4
Cet exemple va commencer à nous montrer d’étranges choses.
L’expression dont l’identifiant habituel est SI (ou IF), couramment utilisée  en programmation est une fonction de trois expressions (ou variables) :

SI Expr1 Expr2 Expr3


telles que si Expr1 est vraie, le résultat est Expr2, sinon Expr3

La fonction SI (ou IF)  s’exprime en Lamda calcul par :

Lambda ident1 . Lambda ident2 . Lambda ident3 ( ident1 ident2 ident3)


Pour le verifier sur un cas en utilisant les expressions :

VRAI = Lambda a . Lambda b . a
FAUX = Lambda a . Lambda b . b

Avec ces définitions de SI, VRAI et FAUX on a par Béta-réductions successives :

SI VRAI A B --> A
et    SI FAUX A B --> B



Exemple 5
Citons enfin le cas de la fonction  habituellement notée par Y en lambda-calcul et appelée aussi fonction paradoxale ou fonction point-fixe. Cette fonction est telle qu'appliquée à une fonction f quelconque : Yf désigne un argument x de f tel que :

f x --> x

son expression est la suivante :

Y =lambda G. G(g g)(lambda g.G(g g))

On peut en effet montrer que pour toute fonction f

Yf = f(Yf)


Y permet de montrer que le Lamda calcul admet le récursivité, ou de retirer la récursivité d'une déclaration de fonction recursive.

________________________________________________________________


Comment évaluer une expression ?

Une expression ne peut avoir que l'un des formes résultant de la syntaxe
(1) evaluer l'expression()
• s'il s'agit d'une expression entre parenthèse retirer les parenthèses puis -->(1)
• s'il s'agit d'un identifiant ou d'une constante retourner ce résultat
• s'il s'agit d'une lambda expression

• suivie d'une ou plusieurs expressions effectuer une Beta- Reduction avec la premiére expression -->(1)
• s'il s'agit d'une suite d'expressions évaluer les deux premières qui donnent un expression en moins --> (1)

• s'il s'agit d'une Lambda expression sans suite aller en (2)


(2) cas difficile d'une lambda expression sans argument
• réduire l'Expr de la lamda expression et retourner la nouvelle lambda expression après réduction
on peut tomber sur une suite irreductible telle que
lambda x.((lamda y.(expr))expr)
irreductible = lambda ident.irreductible

Ainsi :

Règles d'évaluation
Il peut y avoir le choix entre plusieurs applications présentes dans une expression.
La stratégie pour choisir l'ordre de calcul s'appelle une Règle d'évaluation.
Une règle courante est l'évaluation stricte ou appel par valeur.Cette règle impose que les paramètres soient toujours évalués avant d'être fourni à une fonction ou d'y être substitué. Cela revient à passer les paramètres par valeur comme dans les languages tels que le Pascal.
Une autre règle est dite évaluation dans l'ordre normal ou appel par nom. Elle stipule que l'application la plus à gauche et la plus externe soit exécutée à chaque pas. Un paramètre donné n'est pas évalué avant son utilisation : il y a appel par nom.