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 :
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 :
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.
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 :
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 :
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.