Mail/M'écrire


Chapitre 1  SURVOL DU LAMBDA CALCUL (ASPECT FORMEL)

(André Brouty)
Cet exposé est sous licence libre LLDD.
La première partie de ce chapitre est consacrée à une brève présentation du lambda calcul en terme de système formel. Les interprétations possibles de ce système sont abordées dans la seconde partie.

1.0.1  Définition des termes du lambda calcul.

Les termes du lambda calcul sont décrits par le langage suivant:
Soit Vt={ λ ( ) x0 x1 x2 x3 x4 … } l'alphabet ou le vocabulaire terminal. 1

Soit Va={T V E F} la métalangue ou le vocabulaire auxiliaire, T étant l'axiome.

Soient enfin les règles de production:

V —→ x0|x1|x2|x3|… (les variables)
E —→ V|λ(V)E|λ(V)(F) (les expressions simples)
F —→ EE|FE|E(F)|F(F) (les expressions composées)
T —→ E|F (les termes)
Cette grammaire permet de sélectionner dans l'ensemble des mots sur Vt un sous ensemble dont les éléments sont appelés termes ou expressions bien formées (EBF) du lambda calcul.

1.0.2  Précision sur les variables.

Suivant son usage dans un terme une variable peut être libre ou liée.

variable liée.

On détermine l'ensemble des variables liées dans un terme en appliquant à ce terme la fonction V suivante definie inductivement sur chaque composante du terme :
V(xi)= Ø
V(λ(xi)X)= V(X)∪{xi}
V(X1X2)= V(X1)∪ V(X2)

variable libre.

De même l'ensemble des variables libres d'un terme s'obtient en appliquant la fonction W définie inductivement :
W(xi)={xi}
W(λ(xi)X)= W(X)\{xi}
W(X1X2)= W(X1)∪ W(X2)
Dans les définitions précédentes xi désigne une variable quelconque du lambda calcul et X X1 X2 des termes.

1.0.3  Notion de substitution.

Une opération de substitution de variables dans les termes est introduite de la maniere suivante:
S(M)[x ←— N]
signifie qu'on a remplacé dans le terme M chaque occurrence de la variable libre x par le terme N. Cette opération est bien connue et peut faire l'objet d'une définition formelle que nous ne reproduisons pas.

On peut avoir dans un terme à substituer successivement plusieurs variables; nous le traduirons par :
S(M)[x1 ←— N1,x2 ←— N2,…,xn ←— Nn].

1.0.4  Règles de déduction

La construction d'un systeme formel exige la définition d'un langage qui donne les termes; mais cela est en général insuffisant. Il faut pouvoir en plus "classer" ces termes ou calculer sur eux. Cela se fait par l'adjonction au langage d'axiomes ou/et de règles de déduction.

Le lambda calcul est un système formel caracterisé par le langage défini ci-dessus , les définitions précédentes et les règles de déduction suivantes (qui sont en fait des règles de réécriture) :
λ(xi)M → λ(xj) S(M)[xi ←— xj]   (1.1)
λ(x)MN → S(M)[x ←— N]   (1.2)
M → M   (1.3)
M → N et N → L ⇒ M → L   (1.4)
M → N ⇒ ZM → ZN   (1.5)
M → N ⇒ MZ → NZ   (1.6)
M → N ⇒ λ(x)M → λ(x)N   (1.7)
M → N ⇒ M=N   (1.8)
M=N ⇒ N=M   (1.9)
M=N et N=L ⇒ M=L   (1.10)
M=N ⇒ ZM=ZN   (1.11)
M=N ⇒ MZ=NZ   (1.12)
M=N ⇒ λ(x)M= λ(x)N   (1.13)

Commentaires

1.0.5  Définitions.

Nous noterons L la théorie formelle que nous venons de décrire. Par abus d'écriture L désignera aussi bien la théorie que l'ensemble de ses termes. Un terme de L est aussi appelé une λ-expression. Un terme de la forme λ(x)V où x désigne une variable et V un terme sera appelé une abstraction; et un terme de la forme UV, où U et V sont des termes, sera appelé une application. Nous appellerons L0 la théorie précédente dont les termes sont ceux de L qui ne contiennent pas de variables libres. Les éléments de L0 seront appelés des λ-expressions fermées.

1.0.6  Extensionalité.

On étend la théorie précédente en rajoutant la règle suivante :
λ(x) (M x) → M (1.14)
si x n'est pas libre dans M. Cette règle est nommée η-règle. On peut établir facilement l'équivalence de cette règle et de la suivante :
Mx → Nx ⇒ M → N (1.15)
avec x non libre dans MN (voir [1] pp 31-32).
La nouvelle théorie obtenue sera notée L+ext; on aura de même L0+ext.

1.0.7  Exemples.

λ(x1) (x1 x2)
λ(x1) λ(x2) x1
x0 λ(x0) x0
Dans ce dernier exemple la variable x0 a une occurrence libre ainsi qu'une occurrence liée. Par convention d'écriture le second exemple sera abrégé en:
λ(x1 x2) x1
On aura aussi par application de la β-réduction (règle (1.2)):
λ(x1) (x1 x2)M → Mx2

1.0.8  Notion de forme normale.

Une λ-expression sera dite être en forme normale si on ne peut lui appliquer la règle (1.2) dans le cas des théories L et L0, ou si on ne peut lui appliquer les règles (1.2) et (1.14) dans le cas des théories L+ext et L0+ext.

Une λ-expression M sera dite avoir une forme normale s'il existe une λ-expression N en forme normale telle que M → N.

1.0.9  Un autre système formel: la logique combinatoire.

Bien qu'il soit possible de développer le système suivant dans L , nous le ferons indépendamment et mettrons ensuite en évidence les différences et les similitudes les caractérisant. Les termes de la logique combinatoire sont de même décrits par le langage suivant :
soit Vt={B C S W K I ( ) x0 x1 x2 … xn … } l'alphabet;
Soit Va={T V} la métalangue, T étant l'axiome.
Soient enfin les règles de production:

V —→ B|C|S|W|K|I|x0|x1|x2|… |xn … (les variables)
T —→ V|TT|T(T) (les termes)
L'ensemble des termes obtenus par ce langage sera noté CL. Les termes particuliers B C S W K I seront appelés combinateurs de base. De même nous désignerons également par CL le système formel composée du langage précédent et des règles de déduction suivantes:
BXYZ=X(YZ)   (1.16)
CXYZ=XZY   (1.17)
SXYZ=XZ(YZ)   (1.18)
WXY=XYY   (1.19)
KXY=X   (1.20)
IX=X   (1.21)
X=X   (1.21)
X=Y ⇒ Y=X   (1.21)
X=Y et Y=Z ⇒ X=Z   (1.22)
X=Y ⇒ ZX=ZY   (1.23)
X=Y ⇒ XZ=YZ   (1.24)
X Y et Z désignent ici des termes de CL.

Commentaires et définitions

1.0.10  Remarques et exemples.

Il a la même propriété que B. Cependant aucune règle ne nous permet de dire que
SKK=I ou S(KS)K=B.
Mais du point de vue du calcul l'usage de SKK ne se distingue pas de I, c'est pourquoi cette théorie est souvent presentée avec comme combinateurs de base S et K qui permettent de décrire les autres.

Par analogie on dira qu'un terme de CL ou CL0 est en forme normale si on ne peut pas lui appliquer les règles (1.21) à (1.26) utilisées de gauche à droite.

1.0.11  Rapport entre ces systèmes.

On remarque que dans L la λ-expression
Cλ=λ(x0 x1 x2) (x0 x2 x1)
a le même usage que le terme C de CL:
CλXYZ=XZY
CXYZ=XZY
de même avec B W S K et I où on peut leur associer respectivement les λ-expressions:
Bλ=λ(x0 x1 x2) (x0 (x1 x2))
Wλ=λ(x0 x1) (x0 x1 x1)
Sλ=λ(x0 x1 x2) (x0 x2(x1 x2))
Kλ=λ(x0 x1) x0
Iλ=λ(x0) x0
qui vérifient les règles (1.21) à (1.26) de CL. On peut se demander si les deux systèmes sont équivalents. En réalité tel que nous avons défini CL il n'en est rien. La raison en est que le combinateur
CB
par exemple est en forme normale alors que la λ-expression
CλBλ
ne l'est pas. Elle peut se réduire à
λ(x0 x1) (Bλ x1 x0)
en particulier
SλKλKλ = λ(x0 x1 x2) (x0 x2(x1 x2))KλKλ
  = λ(x2) (Kλ x2(Kλ x2))
  = λ(x2) x2
  = Iλ
On démontre ainsi dans L que
SλKλKλ et Iλ
sont équivalents, alors que dans CL SKK est en forme normale et comme nous l'avons dit SKK et I ne peuvent être montrés équivalents dans ce système.

On voit que pour établir l'équivalence de SKK et de I par exemple dans CL alors qu'on sait que
SKKX=X et IX=X c'est-à-dire SKKX=IX
il faudrait pouvoir en déduire l'équivalence de SKK et de I. On reconnait la la règle d'extensionalité.

Complétons donc le système CL par la règle suivante : XZ=YZ ⇒ X=Y où Z n'est pas libre dans XY, et notons CL+ext le nouveau système obtenu. (De même pour CL0+ext).

Il est maintenant possible de montrer l'équivalence entre
L+ext et CL+ext
L0+ext et CL0+ext
Voir par exemple [1] pp 152-159.

1.0.12  Quelques définitions.

ordre d'un combinateur en forme normale

C'est le nombre minimal de termes qu'il faut concaténer au combinateur pour qu'il ne soit plus en forme normale. Par exemple B est d'ordre 3 car BXY est en forme normale mais pas BXYZ. I est d'ordre 1 et B(B(B(B(BI)))) est d'ordre 6. D'après cette définition il n'y a pas de terme d'ordre zéro; on peut alors poser par convention qu'un terme est d'ordre zéro s'il n'admet pas de forme normale.

combinateur régulier

Un combinateur U en forme normale d'ordre n est dit régulier si
UX1X2… Xn=X1X'2… X'p
ou Xi et X'i sont des termes. Par exemple B C S W K et I sont réguliers mais CI et SI ne le sont pas.

combinateur propre

Un combinateur U d'ordre n en forme normale est dit propre si
UX1X2… Xn=X'0X'1X'2… X'p
où Xi est un terme et X'i un terme composé uniquement des termes
X1,X2,... ,Xn.

forme normale de tête

Une λ-expression est dite avoir une forme normale de tête si elle s'écrit:
λ(x1 x2… xn) (y M1 M2… Mp)
ou si elle peut s'écrire sous cette forme en appliquant les règles relatives au système où elle est définie. Le cas n=0 exprime qu'une λ-expression en forme normale de tête est
yM1M2… Mp
xi et y désignent des variables et Mi des termes.

On peut en gros classer les λ-expressions en deux catégories: celle qui ont une forme normale et celle qui n'en ont pas. Ces deux catégories comportent une infinité de termes non équivalents. Présentons quelques exemples:

exemples

λ(x) λ(y) x z u (1.28)
Y=λ(f) (λ(x) (f(x x))λ(x) (f(x x))) (1.29)
O=λ(x) (x x)λ(x) (x x) (1.30)
(1.28) admet une forme normale qui est z. (1.29) et (1.30) n'admettent pas de forme normale. On remarque que (1.29) et (1.30) ne sont pas en forme normale de tête. On peut cependant s'y ramener pour (1.29) en faisant une réduction interne. On obtient:
Y=λ(f) (f(λ(x) (f(x x)) λ(x) (f(x x))))
qui admet la variable f comme variable de tête. Par contre pour (1.30) il n'est pas possible d'obtenir une telle forme normale de tête puisque l'application de la β-réduction redonne éternellement la même expression (1.30).

On peut aussi classer les λ-expressions sans forme normale en deux catégories: celle admettant une forme normale de tête et celle n'en admettant pas. Il est également possible de présenter cette situation autrement.

λ-expressions résolubles

Une λ-expression U de L0 est dite résoluble s'il existe n λ-expressions
M1,M2,… ,Mn telles que UM1M2… Mn=I.

Une λ-expression U de L est dite résoluble si la λ-expression de L0
λ(x0 x1… xn)U est résoluble sachant que {x0 x1 … xn} désigne l'ensemble des variables libres de U.

On peut encore dire qu'une λ-expression U est résoluble si pour tout terme P il existe N1,N2,…,Nq termes tels que UN1N2… Nq=P.

Par exemple S est résoluble ainsi que W ou K puisque
SIII=I
WKI=KII=I
et même Y défini plus haut:
Y(KI)=KI(Y(KI))=I
Par contre O n'est pas résoluble.

Intuitivement les expressions résolubles sont celles avec lesquelles il est possible d'appliquer les règles et d'obtenir un résultat en forme normale. Bref, sur de telles expressions il est possible de calculer.

Un résultat connu du λ-calcul est l'équivalence entre avoir une forme normale de tête et être résoluble (voir par exemple [1] p 171).

1.0.13  Approximations directes.

On vient de voir que parmi les λ-expressions celles qui ne sont pas résolubles ne permettent aucun calcul. L'idée est donc de les éliminer ou tout au moins de les mettre de coté.

C'est pourquoi on définit une application Φ de L dans L ∪ {Ω } de la manière suivante:
si une λ-expression X peut se réduire à
λ(x1 x2… xn)(y X1 X2… Xp)
alors
Φ(X)=λ(x1 x2… xn)(y Φ(X1)Φ(X2)… Φ(Xp))
Φ(x)=x si x est une variable et
Φ(X)=Ω si X n'est pas résoluble.
Ici Ω désigne une constante extérieure au langage. Nous noterons
Φ(L) l'ensemble {Φ(X)|X est un terme de L}.
Nous voyons que Φ(L) contient les λ-expressions sur lesquelles il est possible de calculer. Φ(X) est appelé approximation directe de X.

1.0.14  Ordre sur les λ-expressions.

Il est possible de munir Φ(L) d'une relation d'ordre partielle notée ≼ et définie par:
M ≼ N si M=Ω ou bien si
M=λ(x1 x2… xn)(y M1 M2… Mk)
N=λ(x1 x2… xn)(y N1 N2… Nk) et Mi≼ Ni
Ici xi et y désignent des variables, M N Mi Ni désignent des termes.

Cette relation d'ordre peut être transportée sur L via l'application Φ par:
X ≼ Y si Φ(X) ≼ Φ(Y)
avec X et Y termes de L.

1.0.15  Les arbres de Bohm.

Il est possible de représenter les termes de L au moyen d'un arbre particulier. Mais avant il nous faut d'abord définir ce que nous entendons par arbre, car ici le contexte classique de la théorie des graphes où un arbre est défini comme un graphe connexe sans circuit, ne convient pas car dans un tel contexte les sommets du graphe sont marqués par des éléments tous distincts. Or ici nous avons besoin d'associer à chaque sommet de l'arbre une λ-expression et celle-ci peut fort bien figurer sur plusieurs sommets distincts.

notion d'arbre

Soit donc la suite d'ensembles de uplets:
V0={< >}
Vn={<a1 a2 … an> | ai entier naturel}
on pose
V =
∞
∪
n=0
Vn
Définissons sur V une relation d'ordre partielle, notée ∝, par:
< > ∝ v pour tout v élément de V et
<a1 a2 ... an> ∝ <b1 b2 ... bp> si n≤ p et ai=bi pour 1≤ i≤ n.
Définissons sur V une opération • de concaténation de uplets par:
<a1 a2… an> • <b1 b2… bp> = <a1 a2… an b1 b2… bp>
De plus la relation ∝ est compatible avec l'opération •.
( V • ∝) devient ainsi un demi treillis inférieur.

définition

Un sous ensemble A de V sera appelé arbre s'il est un sous demi treillis de V. La représentation en terme de graphe de A n'est rien d'autre que le diagramme de Hasse du demi treillis.

Exemples


Par convention on prendra toujours le sous arbre commençant à la racine de V et on utilisera une numérotation croissante des sommets de haut en bas et de gauche à droite.
Avec cette convention les arbres


sont distincts. Seul le premier nous intéressera.

arbres étiquetés.

Nous voulons pouvoir à chaque sommet de l'arbre associer une λ-expression qui peut éventuellement se retrouver sur plusieurs sommets.

Soit donc E un ensemble fini ou non de symboles. Un arbre étiqueté sera la donnée de ( V E f) où V est le demi treillis défini ci-dessus, E un ensemble non vide de symboles et f une fonction de V dans E telle que f−1( E) est un arbre. Par exemple si E={a b c d} et f définie par son graphe:
{(< > a)(<0> b)(<1> b)(<2> c)(<1 0> a)(<1 1> b)
(<2 0> d)(<1 0 0> d)(<1 0 1> a)(<1 1 0> b)}
alors l'arbre ci-dessus devient

arbres de Bohm.

Soit une lambda expression élément de L; on peut lui associer un arbre étiqueté de la manière suivante:
L'ensemble d'étiquettes est:
E={Ω}∪ {y | y variable}
∞
∪
n=1
{λ(x1 x2 … xn) y | xi,y variables}
L'arbre de Bohm de la λ-expression M, noté AB(M), est défini par:
si M est résoluble et a été mise sous forme normale de tête
M=λ(x1 x2 … xn)(y M1 … Mk).
Comme exemples voyons les expressions classiques:
Bλ=λ(x0 x1 x2)(x0 (x1 x2))
Sλ=λ(x0 x1 x2)(x0 x2 (x1 x2))
Cλ=λ(x0 x1 x2)(x0 x2 x1)
I3λ=λ(x0 x1 x2)(x0 x1 x2)


Ces deux derniers arbres sont distincts d'où l'importance de l'ordre des branches dans l'écriture. Voyons pour terminer l'arbre de Bohm de l'expression Y ci-dessus qui est résoluble mais sans forme normale.


Les arbres de Bohm des expressions résolubles sans forme normale sont infinis.
1
Contrairement à ce que suggère la notation, Vt n'est pas nécessairement dénombrable.

Caractérisation des termes inversibles en logique combinatoire