1.1 Définition et a-conversion
Commençons par donner une intuition. Le l-calcul est le calcul de
la fonctionnalité pure. Il n'y a donc que deux opérations :
la formation d'une fonction à partir d'un terme et l'application d'une
fonction à un argument. En mathématiques, on dit couramment
``considérons la fonction qui à x associe x+3'', ce que Bourbaki note
x|® x+3. Le l-calcul introduit la notation
l x.x+3 pour cette opération. Dans la suite, le calcul considéré sera
pur et ne contiendra donc aucune constante (comme ici 3
et +).
On se donne un ensemble V infini dénombrable de variables. On définit les
termes inductivement comme suit :
-
Si xÎ V alors x est un terme
- Si xÎ V et M est un terme, alors l x.M est un terme ;
c'est la fonction qui, à x, associe M (qui, en général,
dépend de x).
On dit que la variable x est abstraite dans M.
- Si M et N sont des termes, alors M N est un terme.
C'est l'application de M (à considérer comme une fonction) à N (à
considérer comme son argument).
Tout de suite quelques exemples :
-
L'identité : l x.x, ou bien l y.y ou bien...
- On peut l'appliquer à elle-même : (l x.x) l x.x.
- K=l x.l y.x
Pour alléger les notations, on écrira souvent
l x1 x2 ··· xn.M au lieu de
l x1.l x2.···l xn.M, et
M1M2··· Mk au lieu de
(···((M1M2)M3)···)Mk. On remarquera que ce sont les
conventions habituelles de CAML.
La substitution aux occurrences libres d'une variable x d'un terme M par un terme N
sera notée M[N/x] (où N écrase s).
Définition 1 Pour tout terme N,M et pour n'importe quelle variable x, le résultat (M[N/x]) de la substitution de toutes les occurrences libres de x dans M par N est définie de la manière suivante :
-
x[N/x] º N
- y [N/x] º y pour tout y ¬ ºx
- (M1 M2)[N/x] º (M1[N/x])(M2[N/x])
- (l x.Y)[N/x] º l x.Y
- (l y.Y)[N/x] º (l y.Y[N/x]) si y¬ ºx, et y ÏN ou xÏY
- (l y.Y)[N/x] º (l z.Y[z/y][N/x]) si y¬ ºx et yÎ N et x Î Y où z est une nouvelle variable.
On remarque dans ces exemples que le nom des variables liées dans un terme
n'a aucune importance. Cela se traduit par la règle
d'a-conversion :
l x.M º l y.M[y/x]
si x n'est pas liée dans M et y ne figure pas libre ou liée dans M.
L'importance de cette règle apparaîtra avec la b-conversion.
Exemples :
-
l x.x y º l z.z y mais l x.x y ¬ ºl y.y y.
- l x.yx º l z.yz mais l x.yx ¬ ºl y.yy