Lambda-calcul et langages fonctionnels

Jean Goubault-Larrecq

Table des matières

1 Introduction au λ-calcul 3
1.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.2 Calculs et réduction . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 Théorèmes principaux, confluence, expressivité 6

2.1 Terminaison . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2.2 Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.3 Pouvoir expressif . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

3 Stratégies de réduction et langages de programmation 17

3.1 Stratégies internes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.2 Stratégies externes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.3 Stratégies internes faibles, appel par valeur . . . . . . . . . . . . . . 18
3.4 Standardisation, appel par nom . . . . . . . . . . . . . . . . . . . . . 20

4 Modèles, sémantique dénotationelle 24

4.1 Quelques remarques liminaires . . . . . . . . . . . . . . . . . . . . . 24
4.2 Les ordres partiels complets (dcpo) . . . . . . . . . . . . . . . . . . . 25
4.3 Le modèle Pω . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4.4 Sémantiques d’un λ-calcul enrichi . . . . . . . . . . . . . . . . . . . . 29

5 Style de passage de continuations 32

5.1 Le concept de continuation . . . . . . . . . . . . . . . . . . . . . . . 33
5.2 Sauts non locaux et captures de continuations . . . . . . . . . . . . . 34
5.3 Ajout d’effets de bord . . . . . . . . . . . . . . . . . . . . . . . . . . 39

A Modèles D∞ 40

Résumé
Ceci est la version 15 de la première partie du cours de lambda-calcul,
datant du 04 mars 2024. (Merci à Loïc Chevalier, qui a trouvé de nombreuses
petites erreurs.) La version 14 datait du 30 mai 2023. (Merci à Jean Abou
Samra.) La version 13 datait du 17 avril 2023. (Il manquait un théorème un
tant soit peu formel concernant le pouvoir expressif du λ-calcul.) La version 12
12 datait du 05 mai 2021. La version 11 datait du 15 février 2021. La version 10
datait du 27 janvier 2021. La version 9 datait du 04 mai 2020. (Merci à Gaïa
Loutchmia, qui m’a signalé un bug dans l’usage de l’α-renommage au sein
de la définition formelle de la β-réduction.) La version 8 datait du 25 février
2019. (Merci à Stéphane Le Roux, qui m’a signalé plusieurs inexactitudes.
J’en ai profité pour mettre à jour la partie sur les modèles.) La version 7
datait du 12 novembre 2018. (Merci à Maxime Bombar.) La version 6 datait
du 04 octobre 2017. (Merci à Lilian Besson.) La version 5 datait du 22 février
2017. La version 4 datait du 02 juin 2014 (et contenait encore une erreur dans
la démonstration du théorème de standardisation). La version 3 datait du 28

1
 janvier 2011 (bizarrement, je n’avais pas remarqué l’erreur présente depuis dix
ans dans la démonstration du théorème de standardisation. Merci à Arthur
Milchior), la version 2 datait du 04 mars 2009. La première version datait du
02 août 1999.
Un langage fonctionnel est juste un langage dans lequel la notion de fonction
(procédure, sous-programme) est centrale. Cette définition vague recouvre les lan-
gages fonctionnels dits purs, dans lesquels tout calcul est effectué au moyen d’appels
de fonctions (Miranda, Haskell, par exemple) ; et les langages fonctionnels impératifs
(Lisp, ML), dans lesquels il est aussi permis d’effectuer des effets de bord (affecta-
tions), comme en Pascal ou en C.
Pour prendre un exemple, en OCaml, on peut définir la factorielle par :
let rec fact n = if n=0 then 1 else n*fact (n-1);;
et calculer la factorielle de 10 en demandant :
fact 10;;
ce à quoi le système répond 3628800. On a donc défini la fonction fact par une
définition proche de la notion mathématique usuelle :

1 si n = 0
n!=
ˆ
n × (n − 1)! sinon

où =ˆ dénote l’égalité par définition.

Les ingrédients de cette définition sont, d’abord, l’absence d’affectation à des
variables, contrairement au programme C typique réalisant la même fonction :
int fact (int n)
{
int res, i;

for (res = 1, i = 1; i<=n; i++)

res *= i;
return res;
}
ensuite, la définition de fact par une expression utilisant fact elle-même — ce
qu’on appelle une définition récursive. On pourrait d’ailleurs faire la même chose
en C :
int fact (int n)
{
if (n==0)
return 1;
return n * fact (n-1);
}
ce qui montre que C est lui-même un langage fonctionnel, selon notre définition.
Le point intéressant dans ces petits exemples, et que nous développerons, est
que la notion de fonction est une notion importante en programmation. En fait,
elle est tellement fondamentale qu’on peut fonder un langage de programmation
universel (au sens où une machine de Turing est universelle) sur la seule notion de
fonction : c’est le λ-calcul pur, que nous allons étudier dans ce chapitre. Le λ-calcul
est aujourd’hui un outil central en informatique et en logique : en fait, la sémantique
des langages de programmation, la formalisation des logiques d’ordre supérieur ou
de la déduction naturelle bénéficient directement des concepts inhérents au λ-calcul.

2
 Nous examinons principalement le λ-calcul pur dans ce chapitre. Nous en don-
nons la définition en section 1, prouvons certaines de ses propriétés les plus im-
portantes en section 2, puis nous dégageons les quelques stratégies de réduction
les plus caractéristiques des langages de programmation actuels en section 3. Nous
définissons ensuite des modèles mathématiques des programmes du λ-calcul (les
λ-termes) en section 4, ce qui nous permettra de raisonner sémantiquement sur
les programmes. Finalement, nous introduirons la notion de continuation en sec-
tion 5, en profiterons pour faire le lien entre sémantiques dénotationnelles en style
de passage de continuations et stratégies de réduction.

1 Introduction au λ-calcul
Le λ-calcul a été inventé par le logicien américain Alonzo Church dans les années
1930, dans l’espoir de fournir un fondement au mathématiques plus simple que la
théorie des ensembles, et fondé sur la notion de fonction. Ce programme a échoué,
car le λ-calcul a un pouvoir d’expression beaucoup plus faible ; en revanche, le λ-
calcul a exactement le même pouvoir d’expression que les machines de Turing par
exemple, ce qui en fait un bon choix pour fonder la notion de fonction calculable.
La bible du λ-calcul est le livre de Barendregt [Bar84].

1.1 Syntaxe
Les trois constructions principales du λ-calcul sont :
— la variable (il faut bien commencer quelque part) : nous les noterons x, y, z,
etc.
— l’application : si u et v sont deux programmes, on peut considérer u comme
une fonction et v comme un argument possible, et former l’application uv.
Ceci correspond à la notation mathématique usuelle u(v) tout en nous écono-
misant quelques parenthèses. On remarquera qu’il n’y a pas de contraintes de
typage ici, et qu’il est donc tout à fait légal de former des auto-applications
xx, par exemple.
— l’abstraction : si u est un programme dépendant (ou non) de la variable x,
alors on peut former un nouveau programme λx·u, qui représente la fonction
qui à x associe u.
Par exemple, λx · x + 1 est intuitivement la fonction qui à x associe x + 1 — sauf
que + et 1 ne font pas partie du vocabulaire décrit ci-dessus, un point sur lequel
nous reviendrons.
Formellement, fixons-nous un ensemble V infini dénombrable dit de variables.
On définit l’ensemble Λ des λ-termes s, t, u, v, . . ., comme étant le plus petit tel
que V ⊆ Λ, si u et v sont dans Λ alors uv est dans Λ, et si x ∈ V et u est dans Λ
alors λx · u est dans Λ. Ou, sous forme de déclaration de grammaire :

Λ ::= V | ΛΛ | λV · Λ

On autorisera l’usage de parenthèses pour désambigüer les expressions. D’autre

part, les abstractions s’étendent aussi loin qu’il leur est permis, ce qui signifie en
particulier que λx·uv dénote λx·(uv) et non (λx·u)v. La notation uu1 . . . un dénotera
u si n = 0, et sinon (. . . ((uu1 )u2 ) . . . un ), quant à la notation λx1 , . . . , xn · u, elle
abrégera λx1 · . . . · λxn · u.
L’intérêt de ces deux dernières notations est que, bien que toutes les fonctions du
λ-calcul soient unaires (ne prennent qu’un argument), on peut simuler les fonctions
d’arité quelconque par currification : la fonction λx · λy · x + y, par exemple, est
la fonction qui prend un x en argument, et retourne une fonction qui prend un y

3
en argument et retourne x + y ; autrement dit, c’est la fonction qui prend x, y et
retourne leur somme.

1.2 Calculs et réduction

Il s’agit maintenant de donner un sens à ces λ-termes. Une première observa-
tion simple est que nous voudrions que λx · x + 1 et λy · y + 1 dénotent la même
fonction : que l’argument s’appelle x ou y, c’est toujours la fonction qui ajoute 1 à
son argument. On va donc vouloir confondre les deux termes. Supposons pour cela
que nous sachions ce que veut dire remplacer une variable x par un terme v dans
un terme u, et notons u[x := v] le résultat. L’égalité entre deux termes dont seuls
les noms des variables d’entrée diffèrent s’exprime alors par la règle suivante, dite
d’α-renommage :
(α) λx · u α λy · (u[x := y])
ce qui définit une relation binaire α. Notons =α la plus petite congruence conte-
nant α, autrement dit la plus petite relation telle que uαv implique u =α v, =α
est réflexive, symétrique, transitive et passe au contexte : u1 =α u2 et v1 =α v2
impliquent u1 v1 =α u2 v2 , et u =α v implique λx · u =α λx · v.
Pour plus de simplicité, nous quotientons implicitement Λ par =α , de sorte que
λx · x + 1 et λy · y + 1 seront en fait vus comme deux termes identiques.
Sémantiquement, la règle importante est la β-réduction :

(β) (λx · u)v β u[x := v]

qui exprime que si on applique la fonction qui à x associe u à l’argument v, on

obtient la même chose que si on calcule directement u avec x remplacé par v. Par
exemple, (λx · x + 1)4 β 4 + 1.
Nous noterons →β , ou plus souvent →, la plus petite relation contenant β qui
passe au contexte. Nous noterons →∗ sa clôture réflexive transitive : u →∗ v si et
seulement s’il existe n ≥ 0, et n + 1 termes u0 , u1 , . . ., un tels que u = u0 →
u1 → . . . → un = v. Nous noterons →+ la clôture transitive de → : la définition est
similaire, mais avec n > 0. Finalement, deux termes u et v sont β-équivalents si et
seulement si u =β v, où =β est la plus petite congruence contenant β.
Mais avant d’aller plus avant, il faut d’abord réaliser que la notion de remplace-
ment, ou substitution u[x := v] n’est pas aussi simple qu’elle y paraît. Par exemple,
si vous utilisez la notion de remplacement textuel, fourni par la commande de re-
cherche et de remplacement de n’importe quel éditeur de texte, vous allez obtenir
une absurdité :
(λx · y)[x := uv] = λuv · y (?)
mais λuv · y n’est pas un terme légal, uv n’étant pas une variable. Le remède est
simple : ne remplaçons pas les variables qui suivent un λ, que l’on considère comme
des variables liées. Mais ça ne résout pas tout :

(λx · x)[x := y] = λx · y (?)

λx · y[y := x] = λx · x (?)

Dans le premier exemple ci-dessus, le fait de remplacer x par y dans la fonction

identité λx · x a produit la fonction constante qui retourne toujours y. Dans le
deuxième exemple, c’est le contraire qui se produit.
Le problème dans le premier exemple, c’est que nous avons remplacé une occur-
rence de la variable x qui était liée par l’en-tête λx : nous devons donc exclure ce cas.
Dans le second, c’est plus subtil : nous avons remplacé une variable non liée y par
un terme qui contient une variable libre x (autrement dit, pas dans la portée d’un

4
en-tête d’abstraction), qui si l’on remplace y par x, va se retrouver subrepticement
liée par le λx au-dessus.
Pour éviter ces problèmes, nous conviendrons que les termes sont toujours préa-
lablement α-renommés de sorte à éviter ces problèmes. Formellement (et nous re-
venons pour cela à la notion de termes hors α-renommage) :

Définition 1 L’ensemble des variables libres fv(u) et celui des variables liées bv(u)
est défini par récurrence sur la structure de u par :

fv(x) =ˆ {x} bv(x) =ˆ ∅

fv(uv) =ˆ fv(u) ∪ fv(v) bv(uv) =ˆ bv(u) ∪ bv(v)
fv(λx · u) =
ˆ fv(u) \ {x} bv(λx · u) =
ˆ bv(u) ∪ {x}

On dit que x est substituable par v dans u si et seulement si x 6∈ bv(u) et fv(v) ∩

bv(u) = ∅. Dans ce cas, on définit u[x := v] par récurrence sur la structure de u :

x[x := v] =ˆ v
y[x := v] =ˆ y (y 6= x)
(u1 u2 )[x := v] =
ˆ (u1 [x := v])(u2 [x := v])
(λy · u)[x := v] =ˆ λy · (u[x := v])

La relation d’α-renommage est alors définie par :

(α) λx · u α λy · (u[x := y])

pour toute variable y telle que x est substituable par y dans u et y n’est pas libre
dans u.

Exercice 1 Montrer que, formellement, λx · λy · xy α λy · λx · yx est faux, mais

que λx · λy · xy =α λy · λx · yx est vrai.

Formellement, on définit en fait →β comme la plus petite relation contenant

=α ◦β◦ =α qui passe au contexte, et de même pour →∗β , →+ β , =β .
L’exercice suivant montre que l’on peut essentiellement faire comme s’il n’y avait
aucun problème dans la définition de la substitution, pourvu que l’on s’arrange tou-
jours pour remplacer u par un α-équivalent avant substitution, et que l’on raisonne
toujours modulo α-équivalence. C’est ce que nous supposerons toujours dans la
suite.

Exercice 2 Montrer que pour tous u, x, v il existe un terme u0 tel que u =α u0 et

x est substituable par v dans u0 . Montrer de plus que si u0 et u00 sont deux termes
vérifiant ces conditions, alors u0 [x := v] =α u00 [x := v].

Nous considérerons aussi de temps en temps la règle d’η-contraction :

(η) λx · ux η u (x 6∈ fv(u))

qui exprime que, lorsque u ne dépend pas de x, la fonction qui à x associe u de x est
exactement u elle-même. Par exemple, la fonction λx · len x, où len est la fonction
longueur sur les listes, est len elle-même. Curieusement, (η) est indépendante des
relations précédentes, et notamment λx · ux 6=β u lorsque x 6∈ fv(u) en général.
On note →βη , →∗βη , =βη la plus petite relation contenant β, η et =α , sa clôture
réflexive transitive, sa clôture transitive et la plus petite congruence la contenant
respectivement.

Exercice 3 Donner un exemple montrant que la condition x 6∈ fv(u) est nécessaire,

intuitivement, dans la règle (η).

5
 Une occurrence d’un sous-terme de la forme (λx · u)v dans un terme t est appelé
un β-rédex dans t. (Ce mot vient de l’anglais “redex”, abréviation de “reduction
expression”.) Dire que t → s signifie que s est obtenu à partir de t (modulo α-
renommage) en remplaçant un rédex (λx · u)v par son contractum u[x := v].
Le but de l’exercice suivant est de montrer qu’un terme peut contenir zéro, un
ou plusieurs rédex.

Exercice 4 Montrer qu’il y a exactement deux termes v tels que (λx·(λy·xy)x)z →

v. Nommons-les v1 et v2 . Montrer que, pour chaque i ∈ {1, 2}, il y a exactement
un terme wi tel que vi → wi . Montrer que w1 = w2 et qu’il n’y a pas de terme t tel
que w1 → t.
On a donc le graphe de réductions :

(λx · (λy · xy)x)z

w '
v1 v2

' w
w1 = w2
où v1 , v2 , w1 et w2 sont à trouver.

Exercice 5 Dessiner le graphe de réductions de (λx · (λy · y)x)z, de (λf, x ·

f (f x))(λg, y · gy), de (λx · xx)(λx · xx).

2 Théorèmes principaux, confluence, expressivité

La relation →β (en abrégé, →) est une règle de calcul, elle permet de simplifier
des termes jusqu’à obtenir un terme qu’on ne peut plus simplifier. Un tel terme, sur
lequel on ne peut pas appliquer la règle (β), est appelé une forme normale. Deux
questions se posent immédiatement : 1. ce processus termine-t-il toujours, autrement
dit aboutit-on toujours à une forme normale ? 2. la forme normale est-elle unique ?
En général, combien a-t-on de formes normales d’un même terme ?

2.1 Terminaison
La première question a en fait une réponse négative :

Lemme 1 La β-réduction ne termine pas en général.

Preuve : Considérons Ω=(λx·xx)(λx·xx)

ˆ (on a le droit d’écrire une chose pareille,
oui). Il ne contient qu’un rédex, lui-même. Le contracter redonne Ω, ce qui signifie
que la seule réduction (maximale) à partir de Ω est la boucle :

Ω → Ω → ... → Ω → ...

qui ne termine pas. ♦

Non seulement elle ne termine pas, mais en fait Ω n’a même pas de forme
normale.
Si cette dernière phrase a l’air curieuse, c’est qu’il faut formaliser nos concepts :

Définition 2 Un terme u est fortement normalisant si et seulement si toutes les

réductions partant de u sont finies.
Un terme u est faiblement normalisant si et seulement si au moins une réduction
partant de u est finie.

6
 Donc Ω n’est non seulement pas fortement normalisant, il n’est même pas fai-
blement normalisant.
Tous les termes fortement normalisants sont faiblement normalisants, mais le
contraire n’est pas vrai :

Exercice 6 Montrer que (λx · y)Ω est faiblement normalisant, mais pas fortement
normalisant.

Tant pis pour la terminaison, et en fait c’est normal : n’importe quel langage
de programmation (sauf quelques rares exceptions) permet d’écrire des programmes
qui bouclent, et ne terminent donc jamais.

2.2 Confluence
La deuxième question est alors : en supposant u faiblement normalisant — autre-
ment dit, u a au moins une forme normale —, cette forme normale est-elle unique ?
Cette question a, elle, une réponse affirmative. C’est une conséquence des résultats
qui suivent : Si u →∗ v1 et u →∗ v2 , alors il existe w tel que v1 →∗ w et v2 →∗ w.
Nous démontrerons ce résultat à la fin de cette section.
On utilisera pour écrire ce théorème la notation diagrammatique plus parlante :
u
∗ ∗

~
v1 v1

∗ ∗
~
w
où les lignes pleines indiquent des réductions universellement quantifiées, et les lignes
pointillées des réductions dont l’existence est affirmée. Les astérisques sur les flèches
dénotent la clôture réflexive transitive.
Une technique de preuve qui marche presque est la suivante. On vérifie par
énumération exhaustive de tous les cas que :
u

~
v1 v1

∗ ∗
~
w
c’est-à-dire que la relation → est localement confluent. Noter que u se réduit ici vers
v1 ou v2 en une étape.
Puis on colle autant de ces petits diagrammes qu’il en faut pour obtenir :
u

~
u1 u2

∗ ∗
 .
. ..  ..

 
v1 v2

7
mais ça ne marche pas : les petits diagrammes à mettre à l’intérieur du cône ci-
dessus ne se recollent pas bien les uns aux autres. En fait, supposons qu’on ait
quatre termes a, b, c, d tels que a → b, b → a, a → c et b → d et c et d sont
normaux et distincts, alors on aurait a → c d’un côté, et a →∗ d (en passant par
b). Mais c et d étant normaux et distincts, il n’existe pas de w tel que c →∗ w
et d →∗ w, et le théorème serait faux. Pourtant, on peut vérifier qu’on a tous les
“petits diagrammes” ci-dessus :
a
&
b
x
a
&
b

.y $
c .. d
On peut réparer ce défaut lorsque la relation → termine. . . ce qui ne sera malheu-
resement pas le cas du λ-calcul :
Lemme 2 (Newman) Soit → une relation binaire sur un ensemble A, et suppo-
sons que → est localement confluente et fortement normalisante. (Par fortement
normalisante, nous entendons qu’il n’y a aucune réduction infinite partant d’aucun
élément de A le long de →.)
Alors → est confluente.
Preuve : Comme → termine, on dispose du principe de récurrence le long de → :
pour démontrer une propriété P des éléments u de A, il suffit de la démontrer sous
l’hypothèse (dite de récurrence) que (∗) P (v) est vraie pour tout v tel que u → v.
(Il n’y a pas besoin de cas de base séparé : lorsque u est normal, (∗) est trivialement
vérifiée, et l’on doit donc vérifier que P (u) est vrai pour tout élément normal.)
En effet, supposons le contraire, c’est-à-dire qu’il existe une propriété P telle
que pour tout u, si (∗) P (v) est vraie pour tout v tel que u → v, alors P (u)
est vraie ; mais qu’il existe un élément u0 tel que P (u0 ) soit fausse. On note qu’il
existe nécessairement un u1 tel que u0 → u1 et tel que P (u1 ) soit faux : sinon,
(∗) impliquerait que P (u0 ) soit vrai. De même, il existe un u2 tel que u1 → u2 et
P (u2 ) est faux. Par récurrence sur k, on en déduit l’existence d’une réduction infinie
u0 → u1 → . . . → uk → . . . où P (uk ) est faux : contradiction.
Soit u →∗ v1 et u →∗ v2 . Montrons que v1 et v2 ont un réduit commun, par
récurrence sur u le long de →. Si la longueur de réduction de u à v1 vaut 0, c’est
évident (prendre v2 ), et de même si la longueur de réduction de u à v2 vaut 0. Sinon,
les deux réductions données se décomposent en u → u1 →∗ v1 et u → u2 →∗ v2
respectivement, et l’on a :
u

} !
u1 u2
∗ ∗
∗ ∗
} ! ~ !
v1 v v2
∗
∗
! }
w1 ∗

∗
! }
w

8
où le losange du haut est par l’hypothèse de confluence locale, et les deux plus bas
sont par hypothèse de récurrence, sur u1 et u2 respectivement. ♦
Il y a différentes techniques pour montrer le théorème [Bar84]. Une de celles-ci
est donnée à l’exercice 8.

Exercice 7 (Confluence forte) Supposons que la relation binaire → soit forte-

ment confluente, c’est-à-dire que si u → u1 et u → u2 , alors u1 et u2 se réécrivent
au même terme en au plus une étape. Montrer que → est confluente.


Exercice 8 (Réductions parallèles ) On définit une nouvelle règle de réduc-
tion ⇒ par :
1. u ⇒ u pour tout terme u ;
2. si u ⇒ u0 et v ⇒ v 0 , alors uv ⇒ u0 v 0 ;
3. si u ⇒ u0 , alors λx · u ⇒ λx · u0 ;
4. si u ⇒ u0 et v ⇒ v 0 , alors (λx · u)v ⇒ u0 [x := v 0 ].
Autrement dit, ⇒ est la plus petite relation binaire vérifiant ces conditions et
contenant le α-renommage. Vérifier que :
u

z $
u1 u2

$ z
v
Montrer que →⊆⇒⊆→∗ , et en déduire la confluence du λ-calcul.

Pour démontrer le théorème de confluence du λ-calcul (le théorème 1 plus bas),

nous allons passer par le théorème dit des développements finis. Ceci introduira au
passage une technique de démonstration de la terminaison qui formera la base de
techniques plus avancées que l’on verra en partie 2.
Considérons pour ceci le calcul suivant, qu’on appellera le λ∗ -calcul . Les λ∗ -
termes sont définis par la grammaire :

Λ∗ ::= V | Λ∗ Λ∗ | λV · Λ∗ | (λ∗ V · Λ∗ )Λ∗

de nouveau, à α-équivalence près. Il y a une construction supplémentaire par rap-

port au λ-calcul : la construction (λ∗ x · u)v. Attention : ceci n’est pas l’application
d’un terme de la forme λ∗ x·u à v : il n’y a tout simplement pas de terme de la forme
λ∗ x · t dans le langage. La notation peut prêter à confusion, donc, et il serait peut-
être plus clair de noter la construction (λ∗ x · u)v sous une forme plus proche de la
notation OCaml let x = v in u. Néanmoins, nous conservons la notation (λ∗ x · u)v
par commodité : la technique qui consiste à effacer les étoiles, que nous utilise-
rons ci-dessous, est bien plus simple à expliquer avec cette notation. Formellement,
l’effacement d’étoiles est la fonction E définie par :

E(x) = x E(uv) = E(u)E(v) E(λx·u) = λx·E(u) E((λ∗ x·u)v) = (λx·E(u))E(v)

Le λ∗ -calcul n’a qu’une règle de réduction, la β ∗ -réduction :

(β ∗ ) (λ∗ x · u)v → u[x := v]

On notera que, du coup, (λx · u)v n’est jamais un rédex en λ∗ -calcul.

9
Lemme 3 (Développements finis) La β ∗ -réduction termine.

Preuve : Nous allons tenter de montrer que le λ∗ -terme t est fortement normalisant
par récurrence structurelle sur t. Ceci échoue lorsque t est de la forme (λ∗ x · u)v, il
est possible que t se réduise en (λ∗ x·u0 )v 0 avec u →∗ u0 , v →∗ v 0 , puis en u0 [x := v 0 ],
sur lequel on ne sait plus rien dire.
À la place, nous allons montrer que tσ est fortement normalisant pour toute
substitution σ fortement normalisante. Une substitution est une liste [x1 :=
t1 , . . . , xn := tn ] où les variables x1 , . . ., xn sont deux à deux disjointes. L’applica-
tion de la substitution à t est définie comme pour la substitution ordinaire : xi σ = ti
(1 ≤ i ≤ n), yσ = y pour toute variable hors de {x1 , . . . , xn }, (st)σ = (sσ)(tσ), et
(λx · t)σ = λx · (tσ), où x n’est libre dans aucun ti , et est différent de xi , pour tout i,
1 ≤ i ≤ n. On notera qu’il s’agit d’une substitution parallèle, et qu’en général, par
exemple, t[x1 := t1 , x2 := t2 ] 6= t[x1 := t1 ][x2 := t2 ]. La substitution σ est fortement
normalisante si et seulement si tous les ti le sont, 1 ≤ i ≤ n.
On démontre que tσ est fortement normalisant pour toute substitution fortement
normalisante, par récurrence structurelle sur t.
— Lorsque t est une variable xi , alors tσ = ti est fortement normalisant par
hypothèse.
— Lorsque t est une autre variable y, tσ = y est fortement normalisant.
— Lorsque t est une application uv, toute réduction infinie partant de tσ =
(uσ)(vσ) devrait effectuer une infinité de réductions à partir de uσ ou à partir
de vσ, puisque jamais aucune règle ne s’applique aux applications en λ∗ -calcul
(on se rappellera que la construction (λ∗ x · u)v n’est pas une application).
Mais, par hypothèse de récurrence, on ne peut faire qu’un nombre fini de
réductions depuis uσ et depuis vσ.
— Lorsque t est une abstraction λx·u, tσ = λx·(uσ), à condition d’α-renommer
afin de s’assurer que x ne soit ni parmi les xi ni libre dans aucun ti . Toute
réduction infinie partant de tσ a alors lieu à l’intérieur de uσ, autrement
dit est de la forme tσ = λx · u0 → λx · u1 → · · · où u0 = uσ → u1 → · · ·
est elle-même une réduction infinie, ce qui est impossible par hypothèse de
récurrence.
— Finalement, lorsque t est de la forme (λ∗ x · u)v, toute réduction infinie à
partir de tσ est nécessairement de la forme tσ = (λ∗ x · uσ)(vσ) →∗ (λ∗ x ·
u0 )v 0 → u0 [x := v 0 ] → . . ., où uσ →∗ u0 et vσ →∗ v 0 , et la réduction
(λ∗ x · u0 )v 0 → u0 [x := v 0 ] est la première qui utilise (β ∗ ) au sommet du
terme. Une telle réduction finit nécessairement par arriver, car uσ et vσ sont
fortement normalisants par hypothèse de récurrence. Mais il est facile de
voir que uσ[x := vσ] = uσ 0 où, si σ s’écrit [x1 := t1 , . . . , xn := tn ], σ 0 est
la substitution parallèle [x1 := t1 , . . . , xn := tn , x := vσ]. On démontre en
effet que l’égalité tient dès que x 6∈ {x1 , . . . , xn } et x n’est libre dans aucun
ti , 1 ≤ i ≤ n, par récurrence structurelle sur u. Or, par hypothèse σ, donc
t1 , . . ., tn sont fortement normalisants ; vσ est fortement normalisant par
hypothèse de récurrence ; donc σ 0 est fortement normalisante, ce qui permet
d’affirmer que uσ 0 est fortement normalisant, de nouveau par hypothèse de
récurrence. Or uσ 0 = uσ[x := vσ] →∗ u0 [x := v 0 ], et il existe une réduction
infinie partant de u0 [x := v 0 ] (voir plus haut) : contradiction.
♦
Il est facile, quoique pénible, de vérifier que la β ∗ -réduction est localement
confluente. Par le lemme de Newman (lemma 2), tout λ∗ -terme u a donc une unique
forme normale u ↓. Remarquons que u ↓ ne peut pas contenir d’étoile : les étoiles
apparaissent uniquement sur les β ∗ -rédex. Donc u ↓ est en fait un λ-terme. Défi-
nissons une relation →1 sur les λ-termes par : u →1 v si et seulement s’il existe un
λ∗ -terme u0 tel que u = E(u0 ) et v = u0 ↓. Ceci revient à ajouter des étoiles sur

10
certains rédex de u, puis à les réduire jusqu’à ce que tous aient été éliminés.
La relation →1 est fortement confluente (voir l’exercice 7). En effet, si u →1 u1
et u →1 u2 , c’est qu’on peut rajouter des étoiles à certains rédex de u de sorte
que le λ∗ -terme obtenu se réduise en u1 , et des étoiles à certains rédex (en général
différents) de u de sorte que le λ∗ -terme obtenu se réduise en u2 . Pour fixer les idées,
imaginons que l’on colorie les étoiles : les étoiles ajoutées dans le premier cas sont
bleues, celles du second cas sont rouges. Il est facile de vérifier que, si l’on pose u0
le terme où l’on a rajouté à la fois les étoiles bleues et les étoiles rouges, alors la
réduction u →1 u1 se relève en une réduction de u0 vers un terme u01 qui est u1 , avec
possiblement des étoiles rouges ici ou là ; et que de même u0 se réduit en λ∗ -calcul
à un terme u02 qui est u2 avec des étoiles bleues ici ou là. Comme le λ∗ -calcul est
confluent et terminant, u01 et u02 ont la même forme normale pour (β ∗ ), disons v :
mais alors u1 →1 v et u2 →1 v.

Théorème 1 (Confluence) Si u →∗ v1 et u →∗ v2 , alors il existe w tel que

v1 →∗ w et v2 →∗ w.

Preuve : Comme →1 est fortement confluente, elle est confluente (exercice 7).
Or →⊆→1 ⊆→∗ : si u → v, alors il suffit de poser une étoile sur l’unique rédex
contracté, ce qui montre que u →1 v ; si u →1 v, alors u0 →∗ v en λ∗ -calcul pour un
certain u0 tel que E(u0 ) = u ; mais l’effacement des étoiles s’étend aux réductions,
montrant que u →∗ v.
Donc si u →∗ v1 et u →∗ v2 , on a u →∗1 v1 et u →∗1 v2 . Comme →1 est confluente,
∗
il existe un w tel que v1 →∗1 w et v2 →∗1 w. On en déduit v1 (→∗ ) w, donc v1 →∗ w,
∗
et de même v2 → w. ♦

Corollaire 1 (Unicité des formes normales) Si u1 et u2 sont deux formes nor-

males de u, alors u1 = u2 .

Preuve : Par le théorème 1, il existe w tel que u1 →∗ w et u2 →∗ w. Comme ui

est normal (i ∈ {1, 2}), ui →∗ w implique ui = w. Donc u1 = u2 . ♦
Donc si l’on estime que la valeur d’un programme u est sa forme normale (par
exemple, la valeur de (λx · x + 1)4 serait 5, en supposant que 4 + 1 →∗ 5 et que 5
est normal), alors ce corollaire nous permet d’affirmer qu’en effet cette valeur est
uniquement définie.

Exercice 9 Démontrer que la relation →1 ci-dessus coïncide en fait avec la relation

⇒ de l’exercice 8.

2.3 Pouvoir expressif

La question que nous abordons maintenant est de savoir quelles fonctions on
peut représenter en λ-calcul. Dans nos exemples, nous avons souvent utilisé des
symboles qui ne faisaient pas partie du vocabulaire du λ-calcul pur, comme +, 1, 4
ou 5. Il y a deux façons de les intégrer dans le langage :
1. les ajouter au langage, et se donner quelques règles de réduction supplémen-
taires comme 4 + 1 → 5. Ceci demande à redémontrer la confluence, par
exemple, mais est une façon de faire standard pour définir de vrais langages
de programmation.
2. Ou bien les définir dans le langage, c’est-à-dire trouver des termes dans le
λ-calcul pur qui aient le comportement attendu. Il s’agit de l’approche la
plus simple d’un point de vue logique, et bien que n’étant pas d’une utilité
informatique immédiate, elle apporte de nombreux éléments.

11
 On va commencer par coder les entiers naturels dans le λ-calcul. Il y a plusieurs
façons de le faire, mais la plus simple et la plus connue est d’utiliser les entiers de
Church :
Définition 3 Pour tout n ∈ N, on pose pnq=λf,
ˆ x · f n x, où f n t est défini par :
0 n+1 n
f t=t,
ˆ f t=f
ˆ (f t).
On pose d’autre part :
1. pSq=λn,
ˆ f, x · f (nf x) ;
2. p+q=λm,
ˆ n, f, x · mf (nf x)
3. p×q=λm,
ˆ n, f · m(nf ) ;
4. pexpq=λm,
ˆ n · mn.
L’entier de Church pnq est donc la fonctionnelle qui prend une fonction f et un
argument x, et qui retourne f composée n fois appliquée à x.
On sait donc calculer sommes, produits et exponentielles :
Exercice 10 Montrer que pSqpnq →∗ pn + 1q, autrement dit pSq représente la
fonction successeur, qui à n associe n + 1. De même, montrer que p+q pmq pnq →∗
pm + nq, p×q pmq pnq →∗ pmnq, pexpq pmq pnq →∗ pnm q.
On dispose aussi des booléens. Pour les coder, l’idée c’est qu’un booléen sert à
faire des tests if . . .then . . .else. Si on choisit V=λx,
ˆ y · x pour le vrai et F=λx,
ˆ y · y,
on voit que le test “if b then x else y” se représente juste par l’application bxy. En
effet, “if V then x else y” est Vxy, qui se réduit en x, et “if F then x else y” est
Fxy, qui se réduit en y.
On peut donc presque coder la factorielle, l’exemple du début de ce chapitre.
Pour cela, il nous manque quand même quelques ingrédients, notamment le test
d’égalité entre entiers et le calcul du prédécesseur n − 1 d’un entier n. C’est le sujet
des exercices qui suivent.

Exercice 11 On code les couples hu, vi par la fonction λz · zuv. On définit les
ˆ · sF. Montrer que π1 hu, vi →∗ u et π2 hu, vi →∗ v.
ˆ · sV, π2 =λs
projections π1 =λs
Montrer par contre qu’en général, hπ1 s, π2 si =
6 β s.


Exercice 12 ( ) On veut définir une fonction prédecesseur, c’est-à-dire un λ-
terme pP q tel que pP q(pSqpnq) →∗ pnq pour tout entier n. Par convention, on
posera que pP q(p0q) →∗ p0q.
ˆ · π2 (k(λs · hpSq(π1 s), π1 si)hp0q, p0qi) est une fonction pré-
Montrer que pP q=λk
decesseur acceptable (effectuer une récurrence sur n). Décrire intuitivement com-
ment le prédécesseur est calculé étape par étape. Que pensez-vous de l’efficacité de
l’algorithme ?

Exercice 13 On définit pletq x = u pinq v par (λx · v)u. Montrer que pletq x =
u pinq v → v[x := u]. En déduire que pletq . . . pinq . . . est un mécanisme de nom-
mage (de u par la variable x) correct.

Exercice 14 On veut maintenant fabriquer une construction de pattern-matching

“case n of 0 ⇒ u | pSqm ⇒ f (m)” qui calcule u si n = 0, et sinon calcule f (m),
où m est le prédécesseur de n. On va coder ceci par un terme pintcaseq tel que
pintcaseq pnq uf représente le résultat désiré, autrement dit :

pintcaseq p0q uf →∗ u
pintcaseq pn + 1q uf =β f pnq

Montrer que l’on peut prendre pintcaseq=λk,

ˆ x, f · k(λz · f (pP qk))x.

12
Exercice 15 On va définir une fonction de soustraction partielle −̇ par
m−̇n= ˆ max(m − n, 0). Montrer que p−̇q=λm,
ˆ n · npP qm en est une réalisation cor-
recte.

Exercice 16 Montrer que pzero?q=λn

ˆ · n(λz · F)V est une fonction de test de
nullité, autrement dit :

pzero?q p0q →∗ V
∗
pzero?q pn + 1q → F

En déduire que p≤q=λm,

ˆ n · pzero?q(p−̇qmn) est un terme qui réalise le test ≤
d’inégalité.

Exercice 17 Définir p∧q, un λ-terme prenant deux booléens b et b0 et retournant

leur conjonction b∧b0 (le “et”). Faire la même chose pour le “ou” ∨, pour l’implication
⇒, la négation ¬.

Exercice 18 Sachant que m = n si et seulement si m ≤ n et n ≤ m, déduire des

exercices précédents un terme de test d’égalité entre entiers.


Exercice 19 (B. Maurey ) Étant donnés deux termes a et b dans lesquels x
n’est pas libre, et posant F =λf,
ˆ g ·gf , on définit Ga,b =λn,
ˆ m·nF (λx·a)(mF (λx·b)).
Montrer que :

Ga,b p0q pmq →∗ a

Ga,b pn + 1q pmq =β Gb,a pmq pnq

En déduire que GV,F est une réalisation correcte de ≤, et GF,V une réalisation
correcte de >.

Il nous manque enfin un ingrédient pour pouvoir coder la factorielle (et en fait
n’importe quelle fonction calculable sur les entiers) : la récursion. C’est un point
délicat, et nous allons venir à la solution par étapes.
On veut définir pf actq comme une fonction d’elle-même, autrement dit on veut :

pf actq =β λn · pif q(pzero?qn) p1q (p×qn (pf actq(P n)))

où pif q b x y abrège bxy, dans un but de lisibilité. Il s’agit d’une équation à résoudre,
et son côté droit est une fonction de l’inconnue pf actq. En fait, on peut même écrire
le côté droit sous la forme F pf actq, où F est le λ-terme :

λf · λn · pif q(pzero?qn) p1q (p×qn (f (P n)))

(On a renommé l’inconnue pf actq par une variable f .)

Notre équation devient alors : pf actq =β F pf actq. Ce genre d’équation est
appelé une équation de point fixe, car si pf actq en est une solution, elle est par
définition un point fixe de la fonction représentée par le λ-terme F .
Le miracle du λ-calcul est que tous les termes ont des points fixes ; encore mieux,
ces points fixes sont définissables dans le λ-calcul lui-même :

Théorème 2 Tout λ-terme F a un point fixe x, autrement dit un λ-terme x tel

que x =β F x.
En fait, il existe un λ-terme Y sans variable libre tel que pour tout F , Y F soit
un point fixe de F . Un tel Y est appelé un combinateur de point fixe.

13
Preuve : Ce théorème est surprenant, mais voyons comment on peut le démontrer,
en utilisant le fait que nous connaissons déjà un terme qui boucle, à savoir Ω=(λx
ˆ ·
xx)(λx · xx).
On veut que Y F =β F (Y F ), pour tout F , donc en particulier lorsque F est
une variable. On peut donc définir Y sous la forme λf · A(f ), où A(f ) est un
terme à trouver de variable libre f . Ce qui faisait boucler Ω, c’était une savante
dose d’auto-application. On va réutiliser l’astuce, et essayer de trouver A(f ) sous
la forme de l’application d’un terme B(f ) à lui-même. Autrement dit, on veut que
B(F )(B(F )) =β F (B(F )(B(F ))). Pour cela, on va supposer que le premier B(F ) à
gauche est une abstraction λx·u, et que u est l’application de F à un terme inconnu,
de sorte à obtenir le F en tête de F (B(F )(B(F ))). En somme, on suppose que
B(F )=F
ˆ (C(F, x)), où C(F, x) est un terme à trouver. En simplifiant juste le rédex
de gauche, ceci se ramène à F (C(F, B(F ))) =β F (B(F )(B(F ))), ce qui sera réalisé
dès que C(F, B(F )) = B(F )(B(F )). On peut par exemple poser C(f, x) = xx. En
résumé, on a trouvé le combinateur de point fixe :

Y =λf
ˆ · (λx · f (xx))(λx · f (xx))

Ce combinateur s’appelle le combinateur de point fixe de Church. ♦

On notera que Y F =β F (Y F ), mais il est faux que Y F →∗ F (Y F ). Il arrive
que l’on souhaite cette dernière réduction. En fait, c’est réalisable : le combinateur
Θ de point fixe de Turing a comme propriété que ΘF →∗ F (ΘF ).
On peut l’obtenir par un raisonnement similaire, c’est-à-dire en utilisant un choix
d’arguments parmi : 1. si on veut ab →∗ c et a est inconnu, alors on peut choisir
a sous forme d’une abstraction ; 2. si on veut a →∗ f (b) et a est inconnu, où f est
une variable, on peut choisir a de la forme f (c), avec c à trouver tel que c →∗ b ; 3.
on peut toujours choisir un terme inconnu a de la forme bb, avec b à trouver.
Voici le raisonnement menant au combinateur de Turing. Ce qui faisait boucler
Ω, c’était une savante dose d’auto-application. On va réutiliser l’astuce, et essayer
de trouver Θ sous la forme de l’application d’un terme A à lui-même. On cherche
donc A tel que AAF →∗ F (AAF ). Pour que AAF se réduise, quel que soit F ,
donc même lorsque F est une variable, il est raisonnable de penser que A va devoir
s’écrire λg · B(g) pour un certain terme B(g) à trouver ayant g pour variable libre.
Alors AAF → B(A)F , qui doit se réduire en F appliqué à quelque chose. On va
donc choisir B(g)=λhˆ · h(C(g, h)), où C(g, h) est à trouver. Ce faisant, AAF →
B(A)F = (λh · h(C(A, h)))F → F (C(A, F )), et une solution est alors de définir
C(A, F )=AAF
ˆ , autrement dit C(g, h)=ggh.
ˆ En résumé, on obtient :

Θ=(λg,
ˆ h · h(ggh))(λg, h · h(ggh))

La découverte de combinateurs de points fixes est un exercice de voltige, et si

vous n’avez pas tout suivi, essayez simplement de vérifier que Y F =β F (Y F ) pour
tout F , et que ΘF →∗ F (ΘF ) pour tout F .
Il est aussi clair que l’on ne codera pas les fonctions récursives dans une réa-
lisation informatique du λ-calcul par l’utilisation de Y ou de Θ tels que définis
ci-dessus. Par contre, on supposera souvent qu’on a un mécanisme permettant de
réécrire Y F en F (Y F ), pour Y un terme sans variable libre fixé à l’avance (typi-
quement une constante que l’on aura rajouté au langage). Ce mécanisme ne change
rien aux propriétés du λ-calcul, car on peut le coder dans le λ-calcul lui-même :
c’est tout l’intérêt des constructions du théorème 2.

Exercice 20 ( ) On code les listes de termes comme suit. La liste u1 , . . . , un est
représentée par [u1 , . . . , un ]=λf,
ˆ x · f u1 (f u2 . . . (f un x) . . .). En particulier, la liste
vide est pnilq=λf, ˆ x · x, et la fonction pconsq qui prend un élément u0 et une liste
[u1 , . . . , un ] et retourne [u0 , u1 , . . . , un ] est pconsq=λa,ˆ `, f, x · f a(`f x).

14
 ˆ · `(λy, z · y)pnilq est telle que :
Montrer que phdq=λ`

phdq(pconsqa`) →∗ a
phdq pnilq →∗ pnilq

et donc calcule le premier élément de la liste en argument, quand elle est non vide.
Montrer que pmapq=λg,
ˆ ` · `(λa, `0 · pconsq(ga)`0 )pnilq est telle que :

pmapq g [u1 , . . . , un ] =β [gu1 , . . . , gun ]

(On pourra utiliser le fait que si ` = [u1 , u2 , . . . , un ], alors `hr =β hu1 (`0 hr), où
`0 = [u2 , . . . , un ], et effectuer une récurrence sur n.)
Montrer que ptlq=λ` ˆ · π2 (`(λs, p · hpconsqs(π1 p), π1 pi)hpnilq, pnilqi) envoie la
liste [u1 , u2 , . . . , un ] vers [u2 , . . . , un ]. (Ceci est analogue au codage du prédécesseur
dans les entiers.)
Que fait pappq=λ`, ˆ `0 · `pconsq`0 ?

On conclut cette section en formalisant ce que nous avons appris. Il s’agit d’une
forme faible d’un théorème dû à Kleene. Nous avons besoin de savoir que la classe
des fonctions récursives est la plus petite classe de fonctions (partielles) de Nk vers
N (pour une arité k qui varie de fonction à fonction) qui contient :
— les fonctions constantes ;
— la fonction successeur m ∈ N 7→ n + 1 ;
— les projections πik : (m1 , · · · , mk ) ∈ Nk 7→ mi (1 ≤ i ≤ k) ;
et qui est close par les opérations de :
— composition : pour toutes fonctions g1 , · · · , gk : N` → N et f : Nk → N,
la composition f ◦ hg1 , · · · , gk i est la fonction qui envoie m ~ ∈ N` vers
~ · · · , gk (m))
f (g1 (m), ~ si cette expression est définie (ce qui requiert que g1 (m),
~
. . ., gk (m)
~ soient tous définis, ainsi que l’application de f à ces k entiers), et
est indéfinie sur m ~ sinon ;
— récurrence primitive : pour toutes fonctions f : Nk → N and g: Nk+1 → N, la
fonction Rf,g : Nk+1 → N est définie par

Rf,g (0, m)
~ = f (m)
~
Rf,g (n + 1, m)
~ = g(n, Rf,g (n, m),
~ m),
~

cette définition étant une récurrence sur n, et la valeur à gauche de l’égalité

étant définie si et seulement celle à droite de l’égalité l’est ;
— minimisation : pour toute fonction f : Nk+1 → N, µf : Nk → N est définie
par : µf (m) ~ . . ., f (n − 1, m)
~ est l’unique entier n tel que f (0, m), ~ sont définis
et non nuls, et f (n, m) ~ est (défini et) nul, si cet entier existe ; sinon, µf (m)
~
est indéfini.
La minimisation est probablement plus facile à comprendre comme l’effet d’une
boucle while : n := 0; whilef (n, m) ~ 6= 0 do n + +; return n. A noter qu’une
boucle peut ne pas terminer, et c’est la raison pour laquelle nous sommes obligés
de considérer des fonctions partielles dans la définition des fonctions récursives.
Disons qu’un λ-terme t code correctement une fonction f : Nk → N si et seulement
si, pour tout k-uplet d’entiers m ~ = (m1 , · · · , mk ) ∈ Nk tel que f (m)
~ est défini, on a
t(pm1 q, · · · , pmk q) =β pf (m)q.
~
Théorème 3 Pour toute fonction récursive f , il existe un λ-terme pf q (pas néces-
sairement unique) qui code correctement f , autrement dit : pour tout k-uplet d’en-
~ = (m1 , · · · , mk ) ∈ Nk tel que f (m)
tiers m ~ est défini, on a pf q(pm1 q, · · · , pmk q) =β
pf (m)q.
~

15
Preuve : Par récurrence sur la formation de f . Si f est une fonction constante
d’arité k et de valeur n, on peut poser pf q = λz1 , · · · , zk .pnq. Pour la projection, on
peut poser pπik q = λz1 , · · · , zk .zi . Le successeur est donné à l’exercice 10. On peut
poser :
pf ◦ hg1 · · · , gk iq = λz1 , · · · , z` .pf q(pg1 qz1 · · · z` ) · · · (pgk qz1 · · · z` )
pour ce qui est de la composition. On peut produire pRf,g q, connaissant pf q et pgq,
par la définition :
pRf,g q = Y (λR, z, z1 , · · · , zk .
(pzero?qz)
(pf qz1 · · · zk )
(pgq(pP qz)(R(pP qz)z1 · · · zk )z1 · · · zk )),
ce qui imite la définition pseudo-ML :
letrec R z z1 · · · zk =
if z = 0
then f z1 · · · zk
else g(z − 1)(R(z − 1)z1 · · · zk )z1 · · · zk .
On vérifie les lois :
pRf,g qp0qu1 · · · uk =β pf qu1 · · · uk
pRf,g qpn + 1qu1 · · · uk =β pgqpnq(pRf,g qpnqu1 · · · uk )u1 · · · uk ).
Finalement, on pose :
pµf q = λz1 , · · · , zk . Y (λsearch, z.
(pzero?q(pf qzz1 · · · zk ))
z
search(pSqz))
p0q,
ce qui imite la définition pseudo-ML :
let µf z1 · · · zk =
letrec search z =
if f zz1 · · · zk = 0
then z
else search(z + 1)
in search 0.
Par une récurrence sur n, on vérifie que si pf qp0qu1 · · · uk = pm0 q, . . .,
pf qpnqu1 · · · uk = pmn q où m0 , . . ., mn−1 sont des entiers non nuls et mn = 0,
alors pµf qu1 · · · uk =β pnq. Les vérifications sont laissées en exercice au lecteur. ♦
Kleene a en réalité démontré que l’on peut même demander, non seulement
que pour tout k-uplet d’entiers m ~ = (m1 , · · · , mk ) ∈ Nk tel que f (m)
~ est défini,
on a pf q(pm1 q, · · · , pmk q) =β pf (m)q,~ mais aussi que si f (m) ~ n’est pas défini,
alors pf q(pm1 q, · · · , pmk q) n’est pas normalisable. On peut démontrer cette dernière
affirmation en utilisant le théorème de standardisation, que nous verrons plus bas.
La preuve la plus simple consiste à démontrer que, si f (m) ~ n’est pas défini, alors
pf q(pm1 q, · · · , pmk q) n’a même pas de forme normale de tête (un concept que nous
allons voir plus bas). Nous ne le démontrerons pas.
Réciproquement, nous verrons en troisième partie que tout λ-terme t est (semi-
)calculable, au sens où il existe un programme qui calcule une (la, par confluence)
forme normale de t s’il en existe une. Ceci permet d’en déduire que les fonctions
(semi-)calculables, les fonctions récursives, et les fonctions définissables en λ-calcul,
forment exactement les mêmes classes de fonctions (à un codage convenu près des
entrées et des sorties).

16
3 Stratégies de réduction et langages de program-
mation
On a vu qu’un λ-terme pouvait contenir plusieurs rédex. Si l’on veut calculer la
forme normale d’un terme u (si elle existe), on va pouvoir l’obtenir en choisissant
un rédex dans u, en le contractant, et en répétant le processus jusqu’à ce qu’il n’y
ait plus de rédex. Ce choix du rédex à chaque étape de réduction est appelé une
stratégie de réduction.

3.1 Stratégies internes

Prenons le cas d’un langage de programmation usuel, comme OCaml ou Pascal
ou C. Dans ces langages, un terme de la forme uv (noté u(v) en Pascal ou en
C) s’évalue typiquement en calculant d’abord la valeur f de u, qui doit être une
fonction, puis en calculant la valeur a de v, puis en appliquant f à a. (En général,
u est un identificateur qui dénote déjà une fonction, sans qu’on ait à calculer quelle
fonction c’est exactement.) Remis dans un cadre λ-calculatoire, on peut dire qu’on
a d’abord réduit les rédex de u, puis quand il n’y en a plus eu, on a réduit les rédex
de v, enfin on regarde ce qu’est devenu u, et s’il est devenu un terme de la forme
λx · t, on applique cette dernière fonction à v pour donner t[x := v], et on continue.
Ce genre de stratégie est appelée une stratégie interne (innermost en anglais),
parce qu’elle réduit d’abord les rédex les plus à l’intérieur des termes d’abord. La
stratégie particulière présentée préfère de plus les rédex de gauche à ceux de droite :
elle ne réduit les rédex de droite que quand il n’y en a plus à gauche. Il s’agit d’une
stratégie interne gauche. Une stratégie interne droite est évidemment envisageable,
et se rapprocherait de la sémantique de OCaml. Un petit test qui le montre est de
taper :
let a = ref 0;;
let f x y = ();;
f (a:=1) (a:=2);;
a;;
qui crée une référence (une cellule de valeur modifiable par effet de bord), puis une
fonction bidon f qui ignore ses deux arguments. Ensuite on calcule f appliquée à
deux arguments qui affectent 1, resp. 2 à a. Le langage étant séquentiel, la valeur
finale de a permettra de savoir lequel des arguments a été évalué en dernier. En
OCaml, la réponse est 1, montrant que c’est l’argument de gauche qui a été évalué
en dernier.
Évidemment, en λ-calcul on n’a pas d’affectations, et le fait qu’une stratégie
interne soit gauche ou droite ne change rien au résultat final.

3.2 Stratégies externes

On peut aussi décider d’utiliser une stratégie externe, qui réduit les rédex les plus
externes d’abord. Autrement dit, alors qu’une stratégie interne réduit (λx · u)v en
normalisant λx · u vers λx · u0 , en normalisant v vers v 0 , puis en réduisant u0 [x := v 0 ],
une stratégie externe commence par contracter (λx · u)v en u[x := v], qu’il réduit à
son tour.
Vu au travers du filtre des langages de programmation usuels, voici ce que ces
stratégies donnent pour l’évaluation de f act(1 + 2), en supposant la définition de
f act donnée au début de ce chapitre, et les règles de réduction typiques de +, ×,
etc. Pour se fixer les idées, on utilisera celles de pf actq, p+q, p×q.
On commence par regarder la stratégie externe gauche. (Nous supposons ici, par
commodité, que Y est un combinateur de point fixe tel que Y M →∗ M (Y M ) pour

17
tout M par la stratégie externe gauche, par exemple celui de Turing. Le cas du
combinateur de point fixe de Church nécessiterait de petites adaptations.) Comme
pf actq = Y (λf ·λn·pif q(pzero?qn) p1q (p×qn (f (P n)))), par une stratégie externe
on aura pf actq →∗ λn · pif q(pzero?qn) p1q (p×qn (pf actq(P n)))). On obtient
alors :
pf actq(p+q p1q p2q)
→∗ (λn · pif q(pzero?qn) p1q (p×qn (pf actq(P n))))(p+q p1q p2q)
→ pif q(pzero?q(p+q p1q p2q)) p1q (p×q(p+q p1q p2q) (pf actq(P (p+q p1q p2q))))

mais ici on voit que l’argument (p+q p1q p2q) a été copié en trois endroits. Chaque
occurrence devra être réduite en p3q indépendamment des autres ; autrement dit,
on va devoir calculer 1 + 2 = 3 trois fois !
Pour voir ça plus clairement, reprenons une notation plus proche de la notation
OCaml, et en particulier plus agréable. Nous réécrivons la réduction ci-dessus et la
complétons :

fact (1 + 2)
→∗ (λn · if n = 0 then 1 else n × fact (n − 1))(1 + 2)
→ if (1 + 2) = 0 then 1 else (1 + 2) × fact ((1 + 2) − 1)
. . .où l’on passe quelques temps à réduire (1 + 2) = 0 en F . . .
→∗ if F then 1 else (1 + 2) × fact ((1 + 2) − 1)
→ (1 + 2) × fact ((1 + 2) − 1)
→∗ . . .où 1 + 2 n’est toujours pas évalué à 3 . . .
. . .on réduit comme ça jusqu’à la fin de la récursion . . .
→∗ (1 + 2) × (((1 + 2) − 1) × ((((1 + 2) − 1) − 1) × 1))
→∗ . . .et après un temps certain, on obtient le résultat final,
→∗ 6

3.3 Stratégies internes faibles, appel par valeur

Maintenant, examinons ce qui se passe avec une stratégie interne. Nous allons
commencer par supposer que la factorielle pf actq s’évalue par la stratégie interne
en λn · pif q(pzero?qn) p1q (p×qn (pf actq(P n)), et que ceci est normal. (Il y a un
problème avec cette hypothèse, que nous résoudrons par la suite.) Alors le même
calcul, par la stratégie interne, est beaucoup plus direct. Dans un souci de lisibilité,
nous l’écrivons en notation pseudo-OCaml :

fact (1 + 2)
→∗ (λn · if n = 0 then 1 else n × fact (n − 1))(1 + 2)
→∗ (λn · if n = 0 then 1 else n × fact (n − 1))(3)
→ if 3 = 0 then 1 else 3 × fact (3 − 1))
→∗ if F then 1 else 3 × fact (3 − 1))
→ 3 × fact (3 − 1)
→∗ 3 × (λn · if n = 0 then 1 else n × fact (n − 1))(2)
→∗ . . .par le même procédé . . .
3 × (2 × fact (2 − 1))
→∗ 3 × (2 × (1 × 1))
→∗ 6

ce qui correspond beaucoup plus à ce à quoi on s’attend de la part d’un langage

de programmation.
Cependant, dans l’exemple ci-dessus, nous avons triché deux fois.
Première tricherie : Nous avons supposé que pf actq s’évaluait par la stratégie
interne en λn · pif q(pzero?qn) p1q (p×qn (pf actq(P n)), et que ceci était normal.

18
Mais c’est faux ! En fait, pf actq est de la forme Y F , pour un certain F , et on a :

YF → (λx · F (xx))(λx · F (xx))

→ F ((λx · F (xx))(λx · F (xx)))
→ F (F ((λx · F (xx))(λx · F (xx)))) → . . .

qui ne termine jamais !

Le remède est que dans les langages de programmation usuels, on ne réduit pas
sous les λ. Autrement dit, on considère que λx · u est déjà suffisamment évalué.
De telles stratégies s’appellent des stratégies de réduction faible. Elles ne sont évi-
demment pas suffisantes pour obtenir une forme normale — par exemple, aucune
règle de réduction faible ne s’applique pour réduire λx · (λy · y)x. Mais ça n’est
pas très important dans un langage de programmation ; en un sens, par programme
on veut calculer des entiers, des listes, des structures de données en somme. Si un
programme retourne une fonction, c’est qu’il attend encore au moins un argument
pour pouvoir continuer le calcul.
La stratégie de réduction interne faible peut maintenant se formaliser par les
règles suivantes, où u . v signifie “u se réduit en une étape en v” par cette stratégie :

(β.) u . u0 v . v0
(λx · u)V . u[x := V ] (App1 .) (App2 .)
uv . u0 v uv . uv 0
L’argument V de l’abstraction dans la règle (β.) est contraint à être une valeur.
On définit ici les valeurs V par récurrence sur la structure de V comme étant les
variables, les applications V1 V2 d’une valeur V1 qui n’est pas une abstraction à une
valeur V2 , et les abstractions quelconques λx · u. De façon équivalente :

V ::= VV . . . V | λx · Λ

Ces règles sont une façon commode de dire que . est la plus petite relation
binaire telle que (λx · u)V . u[x := V ] pour tout terme u et toute valeur V , et
passant aux contextes applicatifs (règles (App1 .) et (App2 .)), mais ne passant pas
nécessairement aux contextes d’abstraction. Formellement, les formules (ici, de la
forme u . v) au-dessus des barres sont des prémisses, qu’il faut vérifier avant de
pouvoir appliquer la règle et d’en déduire la conclusion qui est en-dessous de la
barre.
Pour corriger le problème de non-terminaison de la définition de pf actq en tant
que point fixe, on va définir pf actq=Y
ˆ v [F ] au lieu de Y F , où F est la fonctionnelle
définissant pf actq, soit :

F =λf
ˆ · λn · pif q(pzero?qn) p1q (p×qn (f (P n)))

et Yv [F ] est définie de sorte d’une part que Yv [F ]V .∗ F (Yv [F ])V pour toute valeur V ,
et d’autre part que Yv [F ] soit une valeur. On peut y arriver en effectuant quelques η-
expansions dans Y F , comme le montre l’exercice 21. Selon la stratégie interne faible,
´
pf actq = Yv [F ] Ãľtant une valeur, termine immédiatement, et donc, en particulier,
ne boucle plus.

Exercice 21 Définissons Yv [F ]=λy ˆ · (λx · F (λz · xxz))(λx · F (λz · xxz))y. Montrer

que Yv [F ]V .∗ F (Yv [F ])V pour toute valeur V .

Deuxième tricherie : Le calcul que l’on a fait de la factorielle de 3 par straté-

gie interne, maintenant modifiée en une stratégie interne faible, n’est toujours pas
correct, même si on remplace → par .. En effet, la réduction :

19
 if F then 1 else 3 × fact (3 − 1)
. 3 × fact (3 − 1)
est incorrecte : ce n’est pas une réduction par stratégie interne. En ef-
fet, revenons à une écriture plus formelle, alors la ligne du dessus est
Fp1q(p×q p3q (pf actq(P p3q))), mais la réduction par stratégie interne demande
que l’on calcule d’abord la valeur p6q de p×q p3q (pf actq(P p3q)) avant de conclure
que l’on peut normaliser Fp1qp6q en p6q. Or ce que nous avons fait ici, c’est utiliser
une étape de stratégie externe, pour éviter de garder l’argument p1q en attente,
puisque son destin est d’être éliminé de toute façon.
Une conclusion provisoire est que les langages de programmation utilisent en
fait une stratégie interne faible pour les appels de fonction normaux, mais une
stratégie externe (faible elle aussi) pour les tests. La raison est pragmatique : il
est plus avantageux de calculer de façon interne les appels de fonctions normaux,
parce que leurs arguments devront en général être utilisés par la fonction, et que
s’ils sont utilisés plusieurs fois, on n’aura pas à recalculer leur valeur plusieurs fois ;
mais d’autre part, les arguments en position “then” et “else” d’un if ne sont jamais
utilisés plus d’une fois, et en fait l’un des deux ne sera pas utilisé, il est donc plus
intéressant d’utiliser une stratégie externe dans ce cas, ce qui économise l’évaluation
de l’argument qui ne sera jamais évalué.

3.4 Standardisation, appel par nom

Il est bon de remarquer, cependant, que changer de stratégie n’est pas innocent :
certains termes ont une réduction externe qui termine mais aucune réduction in-
terne finie. (Prendre l’exemple de l’exercice 6.) En revanche, et aussi bizarre que ça
paraisse, la réduction externe gauche, aussi inefficace qu’elle puisse être en pratique,
est optimale dans le sens suivant :
Théorème 4 (Standardisation) Si u est faiblement normalisant, alors la straté-
gie externe gauche calcule la forme normale de u par une réduction finie.
Autrement dit, la stratégie externe est peut-être lente, mais elle est sûre : elle
ne se laisse pas embarquer dans des bouclages inutiles.
Preuve :
Avant de commencer, faisons quelques remarques sur les stratégies externes :
— D’abord, on peut écrire tout λ-terme u de façon unique sous la forme
λx1 , . . . , xn · hu1 . . . um , où hu1 . . . um n’est pas une abstraction, h n’est pas
une application, et n et m valent possiblement 0. Le sous-terme h est appelé
la tête de u, et la notation λx1 , . . . , xn · hu1 . . . um est la forme de tête de u.
En effet, si u est une abstraction λx · u0 , on prend x1 = x et on continue le
processus sur u0 ; après un nombre fini détapes, on aboutit ainsi à écrire u
sous la forme λx1 , . . . , xn · v, où v n’est pas une abstraction. Dans ce cas,
soit v est directement la tête h, soit v s’écrit v 0 um , et on recommence le
processus avec v 0 à la place de v. Ce processus s’arrête lorsque v 0 devient
un terme qui n’est pas une application, et on obtient ainsi v sous la forme
désirée hu1 . . . um . (Exercice : formaliser cet argument.)
— Si la tête h de u est une abstraction λx · v, alors nécessairement m ≥ 1 (sinon
hu1 . . . um serait une abstraction), et le sous-terme (λx · v)u1 de u est un
rédex. En fait, dans ce cas (λx · v)u1 est un rédex le plus externe possible, et
c’est le plus à gauche dans u de tous les rédex externes.
Dans ce cas spécial, on dit que (λx · v)u1 est le rédex de tête de u, et l’étape
de réduction :
u = λx1 , . . . , xn · (λx · v)u1 . . . um → λx1 , . . . , xn · v[x := u1 ]u2 . . . um

20
 est appelée réduction de tête.
Notons →t la réduction de tête en une étape, et →∗t sa clôture réflexive
transitive.
— Si par contre la tête h de u n’est pas une abstraction, auquel cas il n’y a
pas de rédex de tête et le terme u est dit normal de tête (car il n’y a pas
de réduction de tête), alors h est une variable. Cette variable est appelée la
variable de tête de u.
La propriété importante est que dans une forme normale de tête u =
λx1 , . . . , xn · hu1 . . . um , les seules réductions possibles prennent place dans
les ui , et en fait sans aucune interférence entre les différents ui . L’en-tête
λx1 , . . . , xn · h . . . ne bougera plus jamais dans la réduction.
Nous donnons maintenant une preuve du théorème due à René David. On peut
définir de façon astucieuse la notion de réduction standard ⇒s de u vers v, comme
étant la relation binaire définie par récurrence sur la taille de v, par u ⇒s v si et
seulement si :
1. v s’écrit sous forme de tête λx1 , . . . , xn · v0 v1 . . . vm ,
2. u se réduit par réduction de tête en une forme de tête λx1 , . . . , xn ·u0 u1 . . . um ,
3. si v0 est une variable x, alors u0 = x, et si v0 est une abstraction λx · v 0 alors
u0 est de la forme λx · u0 et u0 ⇒s v 0 ;
4. u1 ⇒s v1 , . . ., um ⇒s vm .
Il est clair que la stratégie externe gauche réalise une réduction standard. En
effet, la stratégie externe gauche commence par calculer la forme normale de tête
(par →∗t ) λx1 , . . . , xn ·u0 u1 . . . um , puis normalise u1 par la stratégie externe gauche,
puis u2 , . . ., enfin um ; u0 étant une variable, sa normalisation est immédiate. La
notion de réduction standard est plus souple en ce sens qu’on ne demande pas
que u0 soit une variable, et que l’on peut alterner des réductions dans u1 avec des
réductions dans u2 , . . ., um , et même dans u0 .
On va démontrer que : (*) si u →∗ v, alors u ⇒s v, pour tous termes u, v. Ceci
impliquera le théorème : si u a une forme normale v, alors u ⇒s v par (*), et il
ne reste plus qu’à démontrer par récurrence sur la taille de v que cette réduction
standard induit une réduction externe gauche de u vers v. Si v est une variable, alors
cette réduction standard est une réduction de tête, qui est bien une réduction externe
gauche. Sinon, écrivons v sous la forme λx1 , . . . , xn ·v0 v1 . . . vm . Alors nécessairement
la réduction standard de u vers v commence par effectuer une réduction de tête de
u vers une forme de tête λx1 , . . . , xn · u0 u1 . . . um suivie de réductions standard
u0 ⇒s v0 , u1 ⇒s v1 , . . ., um ⇒s vm . Ces réductions standard induisent des réductions
externes gauches par hypothèse de récurrence, donc la réduction :

u →∗t λx1 , . . . , xn · u0 u1 u2 . . . um
→∗ λx1 , . . . , xn · v0 u1 u2 . . . um
→∗ λx1 , . . . , xn · v0 v1 u2 . . . um
→∗ λx1 , . . . , xn · v0 v1 v2 . . . um
→∗ ...
→∗ λx1 , . . . , xn · v0 v1 v2 . . . vm = v

est une réduction externe gauche.

Montrons maintenant (*). En première lecture, il est conseillé de sauter la dé-
monstration, qui est assez technique. L’idée est de permuter les applications de la
 (β), et la difficulté est de le faire dans le bon ordre.
règle

On va démontrer (*) par étapes. Le point important est le numéro 10
ci-dessous, les précédents sont des points techniques :

21
1. D’abord, on remarque que si u = v, alors u ⇒s v ; autrement dit, ⇒s est
réflexive. Ceci se démontre par une récurrence facile sur la taille de v, où les
réductions de tête impliquées sont toutes de longueur nulle ;
2. Ensuite, si u →∗t v, alors u ⇒s v. Écrivons v sous forme de tête λx1 , . . . , xn ·
v0 v1 . . . vm . Par hypothèse, u →∗t λx1 , . . . , xn · u0 u1 . . . um où ui = vi pour
tout i. En particulier, par le point 1, ui ⇒s vi pour tout i ≥ 1. De plus, si
u0 = v0 est une abstraction λx · u0 , alors u0 ⇒s u0 par le point 1.
3. Si u →∗t v et v ⇒s w, alors u ⇒s w : analyse de cas facile.
4. Si λx·u0 ⇒s v, alors v est de la forme λx·v 0 et u0 ⇒s v 0 . Pour ceci, on applique
la définition de nouveau, en observant d’abord que si λx · u0 →t w, alors w
s’écrit λx · w0 avec u0 →t w0 .
5. Si u se réduit par réduction de tête en une forme de tête λx1 , . . . , xn ·
u0 u1 . . . um où n = 0, alors il s’y réduit par une réduction de tête faible,
c’est-à-dire opérant sous un nombre nul de λ (ceci permet de réécrire
λx1 , . . . , xn · (λx · t)s1 . . . sm → λx1 , . . . , xn · t[x := s1 ]s2 . . . sm uniquement si
n = 0). En effet, tout réduction de tête qui n’est pas faible ne peut se réduire
qu’en des termes qui ont au moins un λ en tête.
6. Si u ⇒s v et u0 ⇒s v 0 , alors uu0 ⇒s vv 0 . Par définition, v s’écrit sous forme
de tête λx1 , . . . , xn · v0 v1 . . . vm , u se réduit par réduction de tête en une
forme de tête λx1 , . . . , xn · u0 u1 . . . um , de sorte que les conditions 3 et 4 de
la définition de ⇒s soient vérifiées.
Si n = 0, par le point 5, u se réécrit par réduction de tête faible en u0 u1 . . . um .
L’intérêt de la réduction de tête faible est qu’alors uu0 se réduit par réduc-
tion de tête (faible de nouveau) en u0 u1 . . . um u0 . Ce genre de propriété de
stabilité n’est pas vraie pour les réductions de tête générales. On en conclut
immédiatement uu0 ⇒s vv 0 .
Si n 6= 0, considérons le plus grand préfixe de la réduction de tête de u à
λx1 , . . . , xn · u0 u1 . . . um qui forme une réduction de tête faible. On a donc un
terme t, et une suite de réductions de tête u →∗t t →∗t λx1 , . . . , xn ·u0 u1 . . . um
où les réductions de tête de u à t sont faibles, et les suivantes non. Comme
n 6= 0, on note que t s’écrit lui-même comme une abstraction λx1 · t0 , soit
parce que t = λx1 , . . . , xn · u0 u1 . . . um , soit parce qu’il y a au moins une
étape de réduction de tête de t vers λx1 , . . . , xn · u0 u1 . . . um , et qu’elle n’est
pas faible. On note alors que t0 →∗t λx2 , . . . , xn · u0 u1 . . . um .
On en déduit que uu0 →∗t (λx1 · t0 )u0 (par la propriété de stabilité des réduc-
tions de tête faibles remarquée plus haut), t0 ⇒s λx2 , . . . , xn · v0 v1 . . . vm (par
définition de ⇒s ), u0 ⇒s v 0 , donc uu0 ⇒s (λx1 · (λx2 , . . . , xn · v0 v1 . . . vm ))v 0 =
vv 0 par définition.
7. Si u ⇒s v alors λx · u ⇒s λx · v. C’est immédiat, en notant que si u →∗t u0
implique λx · u →∗t λx · u0 (propriété vraie de la réduction de tête, mais pas
de la réduction de tête faible cette fois-ci !).
8. Si u0 ⇒s w0 , u1 ⇒s w1 , . . ., um ⇒s wm , alors λx1 , . . . , xn · u0 u1 . . . um ⇒s
λx1 , . . . , xn · w0 w1 . . . wm . Ceci peut sembler être juste une reformulation
de la définition, mais la définition requiert que λx1 , . . . , xn · u0 u1 . . . um et
λx1 , . . . , xn · w0 w1 . . . wm soient des formes de tête, ce que l’on ne demande
pas ici. La propriété se démontre par application itérée des points 6, puis 7.
9. Si u0 ⇒s w0 et u1 ⇒s w1 , alors u0 [x := u1 ] ⇒s w0 [x := w1 ]. Ceci se démontre
par récurrence sur la taille de w0 . Écrivons w0 sous forme de tête λy1 , . . . , yn ·
w00 w10 . . . wm0
. Par hypothèse u0 →∗t λy1 , . . . , yn · u00 u01 . . . u0m , où u01 ⇒s w10 , . . .,
um ⇒s wm , et soit u00 et w00 sont des variables identiques, soit u00 = λx · s,
0 0

w00 = λx·t et s⇒s t. Par hypothèse de récurrence, u01 [x := u1 ]⇒s w10 [x := w1 ],

22
 . . ., u0m [x := u1 ] ⇒s wm 0
[x := w1 ]. De plus, u00 [x := u1 ] ⇒s w00 [x := w1 ], par
l’argument suivant : si u00 = w00 = x, ceci provient de u1 ⇒s w1 , si u00 et w00
sont égaux à la même variable y et y 6= x, alors y ⇒s y par le point 1, et si
u00 = λx · s, w00 = λx · t et s ⇒s t, alors ceci vient de s[x := u1 ] ⇒s t[x := w1 ]
(hypothèse de récurrence) et du point 7.
Comme u0i [x := u1 ]⇒s wi0 [x := w1 ] pour tout i, 0 ≤ i ≤ m, le point 8 entraîne
que (λy1 , . . . , yn · u00 u01 . . . u0m )[x := u1 ] = λy1 , . . . , yn · u00 [x := u1 ]u01 [x :=
u1 ] . . . u0m [x := u1 ] ⇒s λy1 , . . . , yn · w00 [x := w1 ]w10 [x := w1 ] . . . wm
0
[x := w1 ] =
w [x := w1 ]. Puisque u →t λy1 , . . . , yn · u0 u1 . . . um , on a aussi u0 [x :=
0 0 ∗ 0 0 0

u1 ] →∗t (λy1 , . . . , yn ·u00 u01 . . . u0m )[x := u1 ], et le point 3 implique donc u0 [x :=

u1 ] ⇒s w0 [x := w1 ].
10. Si u ⇒s w → v, alors u ⇒s v. La démonstration est par récurrence sur la taille
de w.
Par définition, u se réduit par réduction de tête en une forme de tête
λx1 , . . . , xn · u0 u1 u2 . . . um , w a la forme de tête λx1 , . . . , xn · w0 w1 w2 . . . wm
et ui ⇒s wi pour tout i ≥ 1, et soit u0 et w0 sont la même variable, soit
u0 = λx · u0 , w0 = λx · w0 pour certains terms u0 et w0 tels que u0 ⇒s w0 .
La réduction de w vers v peut maintenant se produire en deux types d’en-
droits.
Cas 1 : elle se produit dans l’un des wj (et si j = 0, dans w0 ). Alors v =
λx1 , . . . , xn · v0 v1 v2 . . . vn , avec vi = wi pour tout i 6= j, et wj → vj sinon.
Noter que uj ⇒s wj → vj , et que la taille de wj est plus petite que celle de w,
donc on peut appliquer l’hypothèse de récurrence et conclure que uj ⇒s vj .
D’autre part, pour i 6= j on a ui ⇒s wi = vi . Donc dans tous les cas, pour
tout i, ui ⇒s vi . Il s’ensuit que u ⇒s v, en utilisant le point 8.
Cas 2 : la réduction de w vers v est une réduction de tête. C’est l’unique cas
intéressant de la démonstration. Noter qu’alors on a nécessairement u0 =
λx · u0 , w0 = λx · w0 pour certains terms u0 et w0 tels que u0 ⇒s w0 . De plus,
v = λx1 , . . . , xn · w0 [x := w1 ]w2 . . . wm .
L’idée est qu’au lieu de contracter le rédex (λx · w0 )w1 dans w (donc tard
dans la réduction) on va contracter le rédex qui lui fait pendant beaucoup
plus tôt dans la réduction, (λx · u0 )u1 . Formellement, on étend la réduction
de tête partant de u en :

u →∗t λx1 , . . . , xn · (λx · u0 )u1 u2 . . . um

→t λx1 , . . . , xn · u0 [x := u1 ]u2 . . . um .

Puis l’on note que u0 [x := u1 ]⇒s w0 [x := w1 ] par le point 9, ui ⇒s wi pour tout

i ≥ 2 par hypothèse, donc λx1 , . . . , xn · u0 [x := u1 ]u2 . . . um ⇒s λx1 , . . . , xn ·
w0 [x := w1 ]w2 . . . wm = v par le point 8.
Nous démontrons maintenant (*), à savoir que u →∗ v implique u ⇒s v, par récur-
rence sur la longueur k de la réduction donnée de u vers v. Si cette longueur est
0, alors u = v et on conclut par le point 1. Sinon, c’est que cette réduction s’écrit
u →∗ w → v, où la réduction de u à w est de longueur k − 1. Par hypothèse de
récurrence, u ⇒s w, et par le point 4 ci-dessus, u ⇒s v. ♦
La stratégie externe gauche (leftmost outermost strategy en anglais) est souvent
appelée réduction gauche, ou stratégie d’appel par nom. Cette dernière dénomination
vient du langage Algol, et caractérise le fait que dans (λx · u)v, on remplace d’abord
x par v dans u avant de réduire v — le terme non réduit v étant pris comme nom
de sa valeur.

Exercice 22 Montrer que si u →∗ x, où x est une variable, alors il existe une

réduction de tête de u à x. (Regarder la preuve du théorème 4.)

23
 
Exercice 23 ( ) Utiliser la notion de réduction standard, et en particulier le
point (*) de la démonstration du théorème 4 pour montrer directement que le λ-
calcul est confluent.

D’un point de vue pratique, sachant que ni les stratégies externes (appel par
valeur) ni les stratégies internes (appel par nom) ne sont des panacées, pourquoi ne
pas utiliser d’autres stratégies ? Une qui semble intéressante est la stratégie d’appel
par nécessité, utilisée dans les langages comme Miranda ou Haskell. L’idée, c’est de
partager tous les sous-termes d’un λ-terme, et de considérer les λ-termes comme des
graphes. On verra comment faire cela dans la troisième partie de ce cours, intitulée
“Machines, Interprètes”. Disons tout de suite que ce n’est pas, en fait, une panacée.

4 Modèles, sémantique dénotationelle

La sémantique qu’on a donnée du λ-calcul est par réduction. Que ce soit la
sémantique générale de la β-réduction ou la sémantique de la stratégie interne faible,
cette sémantique est donnée par un ensemble de règles, plus la condition que la
réduction est la plus petite relation binaire obéissant aux règles. On dit qu’il s’agit
d’une sémantique opérationnelle.
Il arrive que l’on ait envie d’un autre style de sémantique, plus synthétique.
Intuitivement, on aimerait pouvoir définir la sémantique du λ-calcul par une fonction
u 7→ [[u]] qui à tout terme u associe un vrai objet mathématique, dans un domaine
D de valeurs. Par exemple, si u = λx · x, on aimerait dire que [[u]] est la fonction
identité (sur un sous-ensemble de D).
[[_]] sera alors un modèle s’il fournit une interprétation saine de la β-conversion,
autrement dit si :
u =β v ⇒ [[u]] = [[v]]
L’intérêt d’une telle approche, c’est qu’elle va simplifier les preuves, dans la
plupart des cas. Par exemple, on pourra montrer que deux termes u et v ne sont
pas convertibles en exhibant un modèle du λ-calcul suffisamment simple dans lequel
[[u]] 6= [[v]]. De façon plus subtile, on utilisera des modèles dans lesquels une valeur
spéciale ⊥ sera réservée pour représenter la valeur des programmes qui ne terminent
pas, et on pourra alors assurer qu’un λ-terme u termine rien qu’en calculant [[u]]
et en vérifiant que le résultat est différent de ⊥, c’est-à-dire sans avoir à réduire u
pendant un temps indéterminé.
L’autre intérêt d’exhiber des modèles, c’est que souvent ils seront trop riches,
et contiendront des valeurs qui ne sont des valeurs d’aucun λ-terme. Ceci permet
par exemple de montrer que certaines constructions sémantiquement saines ne sont
pas réalisables par programme dans le λ-calcul. Par contrecoup, ceci permettra
de suggérer des extensions du λ-calcul, permettant de réaliser ces constructions,
tout en garantissant à la fois que ces extensions sont cohérentes avec le λ-calcul et
nécessaires pour réaliser la construction visée.

4.1 Quelques remarques liminaires

Avant de passer à plus compliqué, observons qu’il y a au moins deux modèles
très simples du λ-calcul :
— le modèle trivial : D est un singleton {∗}, et [[u]] = ∗ pour tout u. Un
tel modèle n’apportant pas grand-chose à notre compréhension, nous nous
efforcerons de trouver des modèles non triviaux.
— Le modèle de termes Λ/=β : ses éléments sont les classes d’équivalence de
λ-termes modulo β-équivalence. Celui-ci est exactement celui qui nous inté-
resse, mais il n’apporte aucune facilité de calcul : pour raisonner dessus, on

24
 est obligé de passer par l’analyse des propriétés de → (confluence, standar-
disation, etc., sont les outils de base).
Nous allons donc essayer de trouver des modèles intermédiaires, qui soient non
triviaux et sur lesquels on peut calculer.
Une première idée est la suivante : on prend un ensemble D de valeurs (séman-
tiques, à ne pas confondre avec la notion de valeurs de la section 3), et on essaie
d’interpréter les termes dans D.
Commençons par les variables : que doit valoir [[x]] ? Tout choix étant arbitraire,
on va supposer qu’on se donne toujours en paramètre une valuation ρ qui à toute
variable associe sa valeur. On définira donc non pas [[u]] pour tout terme u, mais
[[u]]ρ comme une fonction de u et de ρ. Clairement, on posera [[x]]ρ=ρ(x).
ˆ
Grâce aux valuations, on va pouvoir définir facilement la valeur des abstractions.
Pour toute valuation ρ, pour toute variable x et toute valeur v ∈ D, définissons
ρ[x := v] comme étant la valuation qui à x associe v, et à toute autre variable y
associe la valeur qu’elle avait par ρ, soit ρ(y). En somme, ρ[x := v] c’est “ρ, sauf
que x vaut maintenant v”. Le valeur [[λx · u]]ρ est alors juste la fonction 1 qui prend
une valeur v ∈ D et retourne [[u]](ρ[x := v]).
Il y a juste un problème ici, c’est que la valeur de λx · u est une fonction de D
vers D. Mais comme c’est censé être aussi une valeur, elle doit être dans D aussi.
En clair, on veut trouver un domaine D suffisamment gros pour que :
(D → D) ⊆ D
où D → D dénote l’ensemble des fonctions de D vers D. Malheureusement :
Lemme 4 Si (D → D) ⊆ D, alors D est trivial.
Preuve : D ne peut pas être vide, car sinon D → D contiendrait un élément (la
fonction vide) qui n’est pas dans D. Si D n’était pas trivial, alors son cardinal α
serait donc au moins 2. Mais alors le cardinal de D → D serait αα ≥ 2α > α par le
théorème de Cantor, ce qui entraîne que D → D ne peut pas être contenu dans D.
♦
En fait, on veut aussi que D ⊆ (D → D), mais c’est plus facile à obtenir. La
raison est que l’on veut pouvoir interpréter [[uv]]ρ comme l’application de [[u]]ρ à
[[v]]ρ, mais pour cela il faut que toute valeur possible pour [[u]]ρ (dans D) puisse être
vue comme une fonction de D dans D.
Il faut donc trouver d’autres solutions. Une idée due à Dana Scott est de se
restreindre à des domaines D munie d’une structure supplémentaire, et à demander
à ce que l’espace de fonctions de D vers D préserve la structure. Ceci permet de
court-circuiter l’argument de circularité. Par exemple, si on prend D = R avec sa
structure d’espace topologique, et qu’on ne garde que les fonctions continues de
R vers R, alors il n’y a pas plus de fonctions continues que de réels. (La raison
est que le cardinal des réels est 2ℵ0 , et que les fonctions continues de R vers R
sont déterminées de façon unique comme les prolongements par continuité de leurs
restriction à Q. Il n’y en a donc pas plus que de fonctions de Q vers R, soit pas plus
ℵ0
que (2ℵ0 ) = 2ℵ0 .) Malheureusement, même si le problème de cardinalité est ainsi
vaincu, ça ne suffit pas pour résoudre le problème entièrement.

4.2 Les ordres partiels complets (dcpo)

La solution de Scott est de considérer des domaines D qui sont des dcpo, ou
ordres partiels complets (dcpo signifie “directed-complete partial order”) :
1. En français, on devrait dire une application, qui est une fonction définie sur tout son ensemble
de départ. Comme le mot “application” est déjà pris par ailleurs, nous utiliserons les anglicismes
“fonction partielle” pour fonction et “fonction totale” pour application, et conviendrons que “fonc-
tion” signifie “fonction totale”.

25
Définition 4 Un ordre partiel est un couple (D, ≤), où ≤ est une relation d’ordre
sur D.
Un majorant d’une partie E de D est un élément x de D tel que F y ≤ x pour
tout y dans E. Une borne supérieure de E est un majorant minimum E ; si elle
existe, elle est unique.
Une famille dirigée dans (D, ≤) est une famille C = (xi )i∈I non vide et telle que
pour tous i, j ∈ I il existe un k ∈ I tel que xi ≤ xk et xj ≤ xk (de façon équivalente,
toute partie finie de C a un majorant dans C).
On dira qu’un ordre partiel (D, ≤) est complet, ou bien est un dcpo, si et seule-
ment si toute famille dirigée a une borne supérieure. Il est pointé si et seulement
s’il a un élément minimum ⊥.
Une fonction f de (D, ≤) vers (D0 , ≤0 ) est dite monotone si et seulement si
x ≤ y implique f (x) ≤0 f (y). Elle est continue si et seulement si elle est monotone
et préserve les bornes supérieures de familles dirigées :
G G
f ( C) = {f (c) | c ∈ C}

pour toute famille dirigée C dans D.

Parmi les familles dirigées, on trouve les chaînes : les familles de la forme (xn )n∈N
avec x0 ≤ x1 ≤ · · · ≤ xn ≤. Il y en a d’autres. Par exemple, dans l’ensemble des
parties PA d’un ensemble quelconque A, muni de l’ordre d’inclusion ⊆, l’ensemble
des parties finies d’une partie quelconque B ⊆ A est toujours une famille dirigée,
mais n’est pas une chaîne, à moins que B ne soit de cardinal au plus 1.
Les familles dirigées généralisent donc les chaînes, et cette généralisation est utile
dans le traitement mathématique, à partir d’un certain niveau de sophistication. Ce
qu’il est important de comprendre, c’est l’idée qui sous-tend la notion de chaîne :
une chaîne est une suite d’approximations de la valeur que l’on souhaite calculer, et
l’ordre ≤ est l’ordre “est moins précis que”. L’élément ⊥ représente alors l’absence
totale d’information, et la borne supérieure d’une chaîne représente la valeur finale
d’un calcul.
Précisément, on peut voir les chaînes émerger à partir de l’analyse de la réduction
d’un terme. Par exemple, si on prend le terme J =ΘG,ˆ avec G=λx,
ˆ y, z · y(xz), on a
les réductions suivantes, avec à chaque étape ce qu’on peut conclure sur le résultat
final R du calcul, s’il existe :

J= ΘG R =?
→∗ G(ΘG) R =?
→ λy, z · y(ΘGz) R = λy, z · y?
→∗ λy, z · y(G(ΘG)z) R = λy, z · y?
→∗ λy, z · y(λz 0 · z(ΘGz 0 )) R = λy, z · y(λz 0 · z?)
→∗ λy, z · y(λz 0 · z(λz 00 · z 0 (ΘGz 00 ))) R = λy, z · y(λz 0 · z(λz 00 · z 0 ?))
...

où les points d’interrogation dénotent des termes encore inconnus. (Noter qu’il s’agit
d’isoler la partie du terme à chaque ligne qui est en forme normale de tête, cf. théo-
rème 4). On peut ordonner les “termes partiels” contenant des points d’interrogation
par une relation ≤ telle que u ≤ v si et seulement si v résulte de u par le remplace-
ment de points d’interrogations par des termes partiels. La colonne de droite définit
alors bien une chaîne dans l’espace des termes partiels , où ? = ⊥. Pour que de telles
chaînes aient des bornes supérieures, on est obligé d’enrichir l’espace des termes par-
tiels par des termes infinis. Par exemple, la borne supérieure de la chaîne ci-dessus
est :
λz0 , z1 · z0 (λz2 · z1 (λz3 · z2 (. . . (λzk+1 · zk (λzk+2 · zk+1 (. . .

26
après un α-renommage adéquat. On note en général plutôt Ω le point d’interroga-
tion, et l’espace des arbres finis ou infinis ainsi obtenus s’appelle l’espace des arbres
de Böhm.

Exercice 24 Construire la suite d’arbres de Böhm associée à la réduction standard

de λx · x. Quelle est sa borne supérieure ?

Exercice 25 Construire la suite d’arbres de Böhm associée à la réduction standard

de (λx · xx)(λx · xx). Quelle est sa borne supérieure ? Justifier pourquoi on appelle
ce terme Ω.

Le modèle des arbres de Böhm — pour vérifier qu’il s’agit effectivement d’un
modèle, on consultera [Bar84] — est relativement peu informatif encore : il code
essentiellement la syntaxe et la réduction, modulo le théorème de standardisation.
On va maintenant construire quelques modèles (D, ≤), donc quelques dcpo tels
que [D → D] = D, où [D → D] est l’espace des fonctions continues de D dans D.
(En général, pour deux dcpo X et Y , [X → Y ] est le dcpo des fonctions continues
de X vers Y , ordonné point à point : f ≤ g si et seulement si f (x) ≤ g(x) pour
tout x ∈ X. [X → Y ] est non seulement un dcpo, mais les sups dirigés F y sont
calculés point à point aussi : si (fi )i∈I est dirigée dans [X → Y ],Falors i∈I fi est
la fonction, nécessairement continue, qui à tout x ∈ X associe i∈I (fi (x)).) Une
première observation, c’est que nous avons juste besoin que [D → D] et D soient
isomorphes, en fait même seulement qu’il existe deux fonctions continues :

r: D → [D → D] i: [D → D] → D

telles que r ◦ i soit l’identité sur [D → D]. Un tel domaine D est appelé un domaine
réflexif.
En effet, on définira alors :

[[x]]ρ = ρ(x)
[[uv]]ρ = r([[u]]ρ)([[v]]ρ)
[[λx · u]]ρ = i(v 7→ [[u]](ρ[x := v]))

où v 7→ e dénote la fonction qui à la valeur v associe la valeur e (pour ne pas

provoquer de confusions avec la notation des λ-termes, nous ne l’écrivons pas λv · e).
On a alors :

Lemme 5 (Correction) Si u =β v, alors [[u]]ρ = [[v]]ρ pour tout ρ.

Preuve : Il suffit de montrer le résultat lorsque u → v. On le montre alors par

récurrence sur la profondeur du rédex contracté dans u pour obtenir v. Le cas
inductif, où cette profondeur est non nulle, est trivial. Dans le cas de base, on doit
démontrer que [[(λx · s)t]]ρ = [[s[x := t]]]ρ. Mais [[(λx · s)t]]ρ = r([[λx · s]]ρ)([[t]]ρ) =
r(i(v 7→ [[s]](ρ[x := v]))([[t]]ρ) = (v 7→ [[s]](ρ[x := v])([[t]]ρ) (puisque r ◦ i est l’identité)
= [[s]](ρ[x := [[t]]ρ]), et il ne reste plus qu’à montrer que ce dernier vaut [[s[x := t]]]ρ.
Ceci se fait par une récurrence structurelle facile sur s. ♦

4.3 Le modèle Pω
Une première construction d’un modèle, due à Plotkin et Scott, et qui est très
concrète, est le modèle Pω des parties de l’ensemble N des entiers naturels (on note
aussi
F N = ω, d’où le nom), avec l’ordre ⊆. C’est un dcpo, et la borne
S supérieure
i∈I Ai d’une famille (dirigée) d’éléments Ai de Pω est son union i∈I Ai .

27
 m+n=5
15

m+n=4
10 16

m+n=3
6 11 17

m+n=2
3 7 12 18

m+n=1
1 4 8 13 19

m+n=0
0 2 5 9 14 20

Figure 1 – Codage des couples d’entiers

La construction du modèle Pω est fondée sur quelques remarques. D’abord, on

peut représenter tout couple hm, ni d’entiers par un entier, par exemple par la
formule :
(m + n)(m + n + 1)
hm, ni=ˆ +m
2
La valeur de hm, ni en fonction de m en abscisse, et de n en ordonnée, est donnée
en figure 1.
Ensuite, on peut représenter tout ensemble fini e={n ˆ 1 , . . . , nk } d’entiers par
Pk
le nombre binaire [e]= ˆ i=1 2ni . Réciproquement, tout entier m peut être écrit
en binaire, et représente l’ensemble fini em de tous les entiers n tels que le bit
numéro n de m est à 1 : cf. figure 2, où l’on a écrit l’ensemble {1, 3, 4, 7, 9, 10} sous
la forme du nombre binaire 11010011010, soit 1690 en décimal — autrement dit,
[{1, 3, 4, 7, 9, 10}] = 1690 et e1690 = {1, 3, 4, 7, 9, 10}.

10 9 8 7 6 5 4 3 2 1 0

{1, 3, 4, 7, 9, 10} = 1 1 0 1 0 0 1 1 0 1 0 = 1690

Figure 2 – Codage des ensembles finis

Exercice 26 Trouver une formule pour π1 : hm, ni 7→ m et pour π2 : hm, ni 7→ n.

L’astuce principale dans la construction de Pω est que la continuité des fonctions

de Pω dans Pω permet de les représenter comme limites d’objets finis :

Lemme 6 Pour toute fonction f de Pω dans Pω, f est continue si et seulement si

pour tout x ∈ Pω, f (x) est l’union de tous les f (y), y partie finie de x.

Preuve : Seulement si : pour tout x ∈ Pω, la famille des parties finies y de x est
dirigée, et de borne supérieure égale à x. La continuité de f impose que f (x) soit
la borne supérieure des f (y), ySpartie finie de x.
Si : supposons que f (x) = y finie ⊆x f (y). Il est
S facile de voir que f est mono-
tone. Soit (xi )i∈I une famille dirigée de Pω, etSx = i∈I xi sa borne supérieure. Par
monotonie, f (xi ) ⊆ f (x) pour tout i, donc i∈I f (xi ) ⊆ f (x). Réciproquement,

28
 S
pour tout S n ∈ f (x), on montre que n est dans i∈I f (xi ) comme suit. Puisque
f (x) = y finie ⊆x f (y), il existe une partie finie y = {m S 1 , · · · , mk } de x telle que
n ∈ f (y). Pour chaque j, 1 ≤ j ≤ k, mj est dans x = i∈I xi , donc dans xij pour
un certain ij ∈ I. La famille des xi étant dirigée, il existe un xi qui contient tous
les xij , 1 ≤ j ≤ k,Sdonc aussi y. Alors f (y) ⊆ f (xi ) par monotonie.
S Donc n est dans
f (xi ), donc dans i∈I f (xi ). Comme n est arbitraire, f (x) ⊆ i∈I f (xi ). ♦
L’idée est alors que toute fonction continue est définie par ses valeurs sur les
ensembles finis, et que les ensembles finis sont codables par des entiers. On définit
donc :
i: [Pω → Pω] → Pω f 7→ {hm, ni | n ∈ f (em )}
et son inverse à gauche :

r: Pω → [Pω → Pω] e 7→ (x 7→ {n ∈ N | ∃y fini ⊆ x · h[y], ni ∈ e}

Théorème 5 La fonction r ◦ i est l’identité sur [Pω → Pω], r et i sont continues.

De plus, la fonction (u, ρ) 7→ [[u]]ρ est bien définie.

Autrement dit, on a bien défini un modèle. Le fait que la fonction (u, ρ) 7→ [[u]]ρ
soit bien définie signifie notamment que, dans la définition de [[λx · u]]ρ, la fonction
v 7→ [[u]](ρ[x := v]) est bien continue — ce qui n’est pas totalement immédiat.
Finalement, il est clair que Pω est non trivial.

Exercice 27 Démontrer le théorème 5. (En cas de panne, se référer à [Bar84],

pp.469–476.)

Exercice 28 Calculer [[λx · x]]ρ dans Pω, et montrer qu’il est non vide.

Exercice 29 Calculer [[λx, y · xy]]ρ dans Pω, et montrer qu’il est différent de [[λx ·
x]]ρ. En déduire que la règle (η) n’est pas déductible de la (β)-équivalence, autrement
dit λx · ux 6=β u en général.

On peut aussi montrer ce dernier résultat syntaxiquement : λx, y·xy et λx·x sont
η-équivalents mais normaux et différents, donc pas β-équivalents, par la confluence
du λ-calcul. La preuve sémantique via Pω remplace la démonstration combinatoire
de la confluence du λ-calcul par la démonstration sémantique que Pω est un modèle.

4.4 Sémantiques d’un λ-calcul enrichi

Une famille plus générale de modèles, due à Scott, est présentée en annexe A.
Elle permet de montrer le résultat suivant :

Théorème 6 (Scott) Soit (D0 , ≤0 ) un dcpo pointé quelconque. Alors il existe un

dcpo pointé (D∞ , ≤∞ ) contenant (D0 , ≤0 ) et tel que D∞ = [D∞ → D∞ ] à isomor-
phisme près.

Un intérêt que l’on peut avoir dans les dcpo pointés ne tient pas tant au fait
qu’on puisse fabriquer des domaines D réflexifs, mais au fait que finalement ils
modélisent une notion de calcul par approximations successives.
On peut alors fabriquer des dcpo pointés non nécessairement réflexifs pour mo-
déliser des concepts informatiques intéressants. Par exemple, le dcpo pointé des
booléens est B⊥ ={F,
ˆ V, ⊥}, avec l’ordre ⊥ ≤ F, ⊥ ≤ V, mais F et V incom-
parables. En clair, et pour paraphraser l’exemple des arbres de Böhm plus haut,
un programme qui doit calculer un booléen soit n’a pas encore répondu (sa valeur
courante est ⊥) soit a répondu F (et on sait tout sur la valeur retournée, donc
F doit être un élément maximal), soit a répondu V (de même). Comme F et V

29
sont deux valeurs différentes, et maximales en termes de précision, elles doivent être
incomparables.
Le dcpo pointé des entiers, de même, est N⊥ =N ˆ ∪ {⊥}, avec l’ordre dont les
seules instances non triviales sont ⊥ ≤ n, n ∈ N. Les entiers sont incomparables
entre eux pour les mêmes raisons que les booléens, et son diagramme de Hasse est
donné en figure 3. Un tel dcpo pointé, dont la hauteur est inférieure ou égale à 1,
est dit plat.
0 1 2 3 4 5 ...

Figure 3 – Le dcpo plat des entiers naturels

Exercice 30 Si D1 et D2 sont deux dcpo plats, montrer que [D1 → D2 ] n’est jamais
plat, sauf si D1 = {⊥} et D2 est plat, ou bien si D2 = {⊥}.
On peut alors construire sémantiquement un langage plus riche que le λ-calcul
pur, mais qui contienne toujours le λ-calcul. Par exemple, on peut décider d’ajouter
à la syntaxe des termes du λ-calcul des constantes F et V, la constante 0 et un
symbole S représentant le successeur.
Sémantiquement, on a besoin d’un domaine réflexif (pour avoir les fonctions
r et i) contenant l’union de B⊥ et N⊥ . C’est facile : appliquer le théorème 6 à
ˆ ⊥ ∪ N⊥ (un dcpo plat encore). On peut alors définir :
D0 =B

[[T]]ρ =
ˆ V
[[F]]ρ =
ˆ F
[[0]]ρ =
ˆ 0
[[S]]ρ =
ˆ i(v 7→ v + 1)
Il y a quand même un problème dans cette définition, à savoir que v + 1 n’est
défini que quand v est un entier, et donc la fonction v 7→ v + 1 n’est pas définie.
Si v = ⊥, c’est-à-dire que typiquement v est le “résultat” d’un programme qui ne
termine pas, intuitivement on va prendre v + 1 = ⊥, autrement dit le calcul de v + 1
ne terminera pas non plus : une telle fonction, qui envoie ⊥ sur ⊥, est dite stricte.
Si v n’est pas dans N⊥ , alors une convention possible est de considérer que
v + 1 est un programme absurde, qui ne termine pas, autrement dit v + 1 = ⊥.
En pratique, un tel programme absurde plante, ou s’interrompt sur un message
d’erreur, et c’est en ce sens qu’il ne termine pas : il n’arrive jamais au bout du
calcul.
Regardons maintenant les fonctions que l’on peut définir sur les booléens. Le
“ou” ∨ doit avoir la propriété que F ∨ F = F et V ∨ x = x ∨ V = V pour tout x ∈ B,
mais qu’en est-il si x = ⊥ ?
En Pascal, le ou est strict en ses deux arguments. Autrement dit, x∨y est calculé
en calculant x, y, puis en en prenant la disjonction. En C, le ou est strict en son
premier argument mais pas en son second : x||y est calculé en calculant x ; si x vaut
V, alors V est retourné comme valeur, sinon c’est celle de y qui est calculée. En
particulier, V ∨ ⊥ = V. La table de vérité complète est :
|| V F ⊥
V V V V
F V F ⊥
⊥ ⊥ ⊥ ⊥

30
 Il y a encore d’autres possibilités. Une qui maximise le nombre de cas où x ∨ y
termine est donnée par la table de vérité :

| V F ⊥
V V V V
F V F ⊥
⊥ V ⊥ ⊥

Cette fonction | est en effet continue, donc sémantiquement acceptable. Elle est
connue sous le nom de “ou parallèle”, car on peut la réaliser en évaluant x sur un
processeur 1, y sur un processeur 2. Le premier des deux qui répond V interrompt
l’autre, et V est retourné. Si les deux répondent F, alors F est retourné. Sinon, rien
n’est retourné, autrement dit la valeur finale est ⊥.
Il est remarquable que, alors que le ou de Pascal et le || de C étaient simu-
lables en λ-calcul, le ou parallèle ne l’est pas. La raison est que le λ-calcul est
intrinsèquement séquentiel. Ceci ce manifeste mathématiquement par le fait que les
valeurs sémantiques des fonctions définissables par des λ-termes sont non seulement
continues, mais stables :

Définition 5 Deux éléments x et y d’un dcpo sont dits compatibles si et seulement

s’il existe z dans le dcpo tel que x ≤ z et y ≤ z.
Supposons que le dcpo D ait la propriété que pour tous éléments compatibles x
et y, il existe une borne inférieure x u y. Une fonction f : D → D0 est stable si
et seulement si elle est continue, et pour tous x, y compatibles dans D la borne
inférieure f (x) u f (y) existe et est égale à f (x u y).
On munit l’espace des fonctions stables de D vers D0 de l’ordre de Berry : f ≤s g
si et seulement si x ≤ y implique que f (y) u g(x) existe et égale f (x).

Exercice 31 Montrer que le ou parallèle n’est pas stable. En déduire qu’on ne peut
pas le coder en λ-calcul enrichi avec T, F, 0, S.

On peut coder le test “if . . .then . . .else . . .”. Sémantiquement, c’est la fonction
if (x, y, z) telle que if (V, y, z) = y, if (F, y, z) = z, et si x n’est pas un booléen alors
if (x, y, z) = ⊥. Noter que cette fonction est stricte en son premier argument, mais
pas en son deuxième et en son troisième.
Par contre, des fonctions comme + et × seront strictes en tous les arguments.
Même × est en général choisie stricte, ce qui signifie que 0 × ⊥ = ⊥ et non 0. On
remarquera qu’une fonction appelée par valeur (+, ×) est nécessairement stricte, car
cette fonction attend que ses arguments soient évalués avant de continuer le calcul ;
alors qu’une fonction en appel par nom peut être non stricte. (Le dcpo que nous
choisissons pour comprendre ces notions dans un cadre d’analyse des réductions est
celui dont les valeurs sont les arbres de Böhm.) Le cadre sémantique est plus souple
et accomode les deux notions dans une seule définition. De plus, les détails réels des
réductions importent peu, finalement, du moment que les équations sémantiques
sont respectées.
Par exemple, un λ-calcul avec booléens et entiers, en appel par valeur sauf sur
le “if . . .then . . .else . . .”, serait défini comme suit. On prend un dcpo D tel que :

D = (N ⊕ B ⊕ [D → D])⊥

modulo un isomorphisme i qui sera laissé implicite dans la suite, où ⊕ dénote l’union
disjointe d’ensembles ordonnés, et D⊥ dénote l’ensemble ordonné obtenu à partir
de D en ajoutant un élément ⊥ plus bas que tous les éléments de D, et on définit
[[_]] comme en figure 4.

31
 [[x]]ρ =
ˆ ρ(x)

⊥ si v = ⊥
[[λx · u]]ρ =
ˆ i(v →
7 )
[[u]](ρ[x := v]) sinon

f ([[v]]ρ) si f =[[u]]ρ
ˆ ∈ [D → D]
[[uv]]ρ =
ˆ
⊥ sinon
[[T]]ρ =
ˆ V
[[F]]ρ =
ˆ F
[[0]]ρ =
ˆ 0

v+1 si v ∈ N
[[S]]ρ =
ˆ i(v 7→ )
⊥ sinon

 [[v]]ρ si [[u]]ρ = V
[[if (u, v, w)]]ρ =
ˆ [[w]]ρ si [[u]]ρ = F
⊥ sinon


Figure 4 – Sémantique dénotationnelle de l’appel par valeur

Dans les langages dits paresseux, comme Miranda ou Haskell, qui simule un
appel par nom d’une façon un peu plus efficace (voir partie 3), la seule différence
serait qu’il n’attend pas d’évaluer l’argument, et donc on aurait juste :

[[λx · u]]ρ =
ˆ i(v 7→ [[u]](ρ[x := v]))

On voit alors qu’on peut réaliser une fonction λx · u qui est normalement en
appel par nom par une stratégie d’appel par valeur exactement quand les deux
définitions de sa sémantique coïncident, autrement dit quand cette fonction est
stricte. L’appel par valeur étant dans ce cas moins coûteux en temps et en espace,
un bon compilateur pourra compiler les fonctions détectées comme strictes par une
stratégie d’appel par valeur. Cette détection de fonctions strictes est appelée en
anglais la “strictness analysis”.

5 Style de passage de continuations

Les modèles sémantiques dénotationnels que l’on a vus jusqu’ici — dits en style
direct — ont l’avantage d’oublier tous les détails liés à l’ordre d’évaluation, excepté
les points importants comme la terminaison (valoir ⊥ ou pas). C’est parfois aussi
un inconvénient, et on aimerait parfois pouvoir exprimer une partie de la stratégie
d’évaluation. Par exemple, dans la sémantique proposée en figure 4, rien ne dit que
pour évaluer uv, on doive évaluer u avant v.
C’est gênant notamment si l’on enrichit notre λ-calcul avec des constructions
telles que les affectations (setq en Lisp, := ou <- en Caml, := en Pascal, = en C),
ou les sauts non locaux (try et raise en Caml, goto en Pascal, setjmp et longjmp
en C). Prenons le cas des affectations tout d’abord, parce qu’il est plus simple à
expliquer. Supposons qu’on veuille calculer la valeur de uv, et que l’évaluation de u
affecte une référence x à 1, et l’évaluation de v affecte x à 2. Si u est évalué avant v,
alors x vaudra 2 à la fin du calcul, et si c’est v, alors x vaudra 1 à la fin du calcul :
la sémantique des deux cas n’est donc pas la même.

32
5.1 Le concept de continuation
Une façon de spécifier l’ordre d’évaluation en sémantique dénotationnelle est de
faire prendre à la fonction d’évaluation un deuxième argument, la continuation κ,
qui est une fonction de D vers D, et de convenir que :

[[u]]ρκ

est la valeur non pas de u mais d’un programme tout entier dont un sous-terme est
u : κ dénote la suite du calcul une fois qu’on aura évalué u, et si la valeur de u
est d, alors la valeur du programme tout entier sera κ(d). Graphiquement, on peut
imaginer que l’on a un programme π, dont l’exécution va consister en une suite
d’instructions, et qu’au milieu de cette suite on trouve une sous-suite d’instructions
pour évaluer u :
π

1 2 3

u κ

Lorsque l’exécution se trouve au début de u (au point 1), ce graphique dit que
ce qu’il reste à faire pour trouver la valeur de π au point 3, c’est calculer la valeur
de u, et une fois qu’on l’aura (au point 2), il suffira d’appliquer κ, la suite du calcul.
Formellement, examinons déjà comme on peut modéliser une stratégie (faible)
d’appel par valeur gauche sur les λ-termes purs par ce moyen (le codage des boo-
léens, des entiers, etc., est laissé en exercice), et nous verrons ensuite comment ce
style de sémantique permet de modéliser les constructions de style setjmp/longjmp,
puis les affectations.
Tout d’abord, [[x]]ρκ, lorsque x est une variable, doit évaluer x, et passer sa
valeur ρ(x) à κ. On va donc définir [[x]]ρκ=κ(ρ(x)).
ˆ
Dans le cas des applications, [[uv]]ρκ doit d’abord évaluer u, puisque nous avons
décidé d’une stratégie gauche. [[uv]]ρκ vaudra donc [[u]]ρκ0 pour une continuation
κ0 à trouver. Cette continuation κ0 est une fonction qui prend la valeur f de u,
et va ensuite calculer v. Donc κ0 doit être de la forme (f 7→ [[v]]ρ0 κ00 ) pour un
environnement ρ0 et une continuation κ00 à trouver. Mais v s’évalue dans le même
environnement que uv, donc ρ0 = ρ. D’autre part, κ00 doit être une fonction qui
prend la valeur d de v, applique la valeur f de u (que l’on supposera être une
fonction) à d, et continue le reste du calcul (κ) avec la valeur f (d). En résumé :

[[uv]]ρκ=[[u]]ρ(f
ˆ 7→ [[v]]ρ(d 7→ κ(f (d))))

Cette formule peut avoir l’air illisible, mais voici un truc pour déchiffrer ce genre
de notations intuitivement : [[u]]ρ(f 7→ . . . se lit “évaluer u dans l’environnement ρ,
ceci donne une valeur f ; ensuite . . .”. D’autre part, appliquer κ à une valeur d se
lit : “retourner d”. La formule ci-dessus se lit donc :
Évaluer u dans l’environnement ρ, ceci donne une valeur f ; ensuite,
évaluer v dans l’environnement ρ, ceci donne une valeur d ; ensuite,
retourner f (d).

Pour évaluer une λ-abstraction λx · u dans l’environnement ρ et la continuation

κ, on va d’abord calculer la valeur de λx · u, et ensuite la retourner par κ. Cette
valeur est une fonction qui prend une valeur d pour x, et ensuite évalue u . . .mais
avec quelle continuation ? L’idée, c’est qu’une fois que le calcul de u sera terminé,

33
la continuation devra juste retourner cette valeur : la continuation cherchée est
l’identité id. En somme :

[[λx · u]]ρκ=κ(d
ˆ 7→ [[u]](ρ[x := d])id)

Cette sémantique, qui est notre premier exemple d’une sémantique par passage
de continuations, est résumée en figure 5. Nous avons affiné la définition dans le cas
de l’application uv, pour tenir compte de ce qui se passe lorsque f n’est pas une
fonction dans le domaine sémantique D considéré. Noter qu’on ne retourne pas ⊥
(on n’a pas écrit κ(⊥)), mais on interrompt l’exécution complète du programme,
qui retourne immédiatement ⊥. (C’est un plantage.)

[[x]]ρκ =
ˆ κ(ρ(x))
   
κ(f (d)) si f est une fonction
[[uv]]ρκ =
ˆ [[u]]ρ f 7→ [[v]]ρ d 7→
⊥ sinon
[[λx · u]]ρκ =
ˆ κ(d 7→ [[u]](ρ[x := d])id)

Figure 5 – Une sémantique de l’appel par valeur en style de passage de continua-

tions

On notera que l’on aurait pu définir l’application autrement, par exemple :

  
[[v]]ρ(d 7→ κ(f (d))) si f est une fonction
[[u]]ρ f 7→
⊥ sinon

Avec cette autre définition, si f n’est pas une fonction, la machine plante avant
même d’évaluer v.

5.2 Sauts non locaux et captures de continuations

Voyons maintenant comment on peut coder un mécanisme à la setjmp/longjmp
de C. Rappelons que setjmp capture une copie du contexte d’évaluation courant
(le compteur de programme, le pointeur de pile, les registres) et la met dans une
structure k, que nous représenterons par une variable du λ-calcul, puis retourne 0 ;
longjmp appliqué à k et à une valeur d réinstalle k comme contexte d’évaluation
courant, ce qui à pour effet de faire un saut non local à l’endroit du programme où
se trouve le setjmp qui à défini k, et de faire retourner la valeur d par ce dernier.
Ceci permet de gérer des conditions d’erreur, par ex :
x = setjmp (k);
if (x==0) /* retour normal */
{
/* faire un certain nombre de calculs, eventuellement imbriques,
qui arrivent a la ligne suivante : */
if (errno)
longjmp (k, errno); /* longjmp ne retourne pas,
et saute a l’endroit du setjmp ci-dessus */
/* si pas d’erreur, continuer... */
}
else
{ /* ici, on est revenu sur erreur, avec x==errno */
printf ("Erreur no. %d.\n", x);
}

34
Comme beaucoup de constructions en C, celle-ci manque de l’élégance des construc-
tions similaires de langages fonctionnels, et la plus proche est une construction, ap-
pelée call-with-current-continuation ou call/cc, et qui a été introduite dans
le langage Scheme, un dialecte Lisp. (Le manque d’élégance de la construction C
est due à deux choses. D’une part, si errno vaut 0, on ne peut pas distinguer un
retour normal de setjmp d’un retour sur erreur dans l’exemple ci-dessus. D’autre
part, longjmp a une sémantique indéfinie s’il est appelé après que la fonction dans
laquelle setjmp a été appelé a retourné.)
L’idée est simple : le concept concret de contexte d’évaluation courant n’est
rien d’autre que la continuation κ ! On peut donc définir en première approche
une construction callcc k in u qui capture à la façon de setjmp le contexte (la
continuation) courante, la met dans k et évalue u ; et une construction throw k v
qui évalue k et v, et réinstalle la continuation k pour faire retourner la valeur de v
par l’instruction callcc qui a défini k. Sémantiquement :

[[callcc k in u]]ρκ =
ˆ [[u]](ρ[k := κ])κ
[[throw k v]]ρκ =
ˆ [[k]]ρ(κ0 7→ [[v]]ρκ0 )

Remarquer que dans la définition de throw, la continuation κ n’intervient pas

dans le côté droit de l’égalité : elle est tout simplement ignorée, car c’est la conti-
nuation κ0 , valeur de k, qui va être utilisée pour continuer le calcul. Le fait que κ
n’intervienne pas signifie que throw k v ne retourne jamais.
On peut tester sur quelques exemples que le comportement est bien le compor-
tement attendu :

Exercice 32 Montrer que callcc k in 3 retourne 3 ; autrement dit, en supposant

que l’on a une constante 3 telle que [[3]]ρκ = κ(3), montrer que [[callcc k in 3]]ρκ =
κ(3).

Exercice 33 Selon cette sémantique, que valent

callcc k in throw k 3, callcc k in (throw k 3) 2,
callcc k in + 1 (callcc k’ in throw k’ (throw k 3)) ? (On supposera
que 1 et l’addition ont leurs sémantiques naturelles, que l’on précisera.)

Mais en fait, non, le comportement des continuations n’est pas le com-

portement attendu en général. Considérons le programme callcc k in (λx ·
throw k (λy · y))3. On s’attend à ce qu’il ait la même sémantique que le β-réduit
callcc k in throw k (λy · y), autrement dit qu’il retourne la fonction identité, mais
ce n’est pas le cas. En effet, formellement :

[[callcc k in (λx · throw k (λy · y))3]]ρκ

= [[(λx · throw k (λy · y))3]](ρ[k := κ])κ
= [[λx · throw k (λy · y)]](ρ[k := κ])(f 7→ [[3]](ρ[k := κ])(d 7→ κ(f (d)))
= [[λx · throw k (λy · y)]](ρ[k := κ])(f 7→ κ(f (3)))
= (f 7→ κ(f (3)))(d 7→ [[throw k (λy · y)]](ρ[k := κ, x := d])id)
= κ([[throw k (λy · y)]](ρ[k := κ, x := 3])id)
= κ([[k]](ρ[k := κ, x := 3])(κ0 7→ [[λy · y]](ρ[k := κ, x := 3])κ0 ))
= κ((κ0 7→ [[λy · y]](ρ[k := κ, x := 3])κ0 )κ)
= κ([[λy · y]](ρ[k := κ, x := 3])κ)
= κ(κ(d 7→ [[y]](ρ[k := κ, x := 3, y := d])id))
= κ(κ(d 7→ d))

35
alors que :
[[callcc k in throw k (λy · y)]]ρκ
= [[throw k (λy · y)]](ρ[k := κ])κ
= [[k]](ρ[k := κ])(κ0 7→ [[λy · y]](ρ[k := κ])κ0 )
= (κ0 7→ [[λy · y]](ρ[k := κ])κ0 )κ
= [[λy · y]](ρ[k := κ])κ
= κ(d 7→ [[y]](ρ[k := κ, y := d])id)
= κ(d 7→ d)
Non seulement les deux valeurs sémantiques ne sont pas identiques — donc nous
n’avons plus un modèle correct de la β-réduction —, mais celle de callcc k in (λx ·
throw k (λy · y))3 est en fait parfaitement absurde : κ(κ(d 7→ d)) signifie que si κ est
la suite du programme, au lieu de retourner simplement la fonction d 7→ d, on va
retourner d 7→ d, effectuer la suite du programme, et une fois que le programme aura
terminé et retourné une valeur d0 , on réexécutera la même suite κ du programme
cette fois-ci sur la valeur d0 !
Le problème est dans la façon dont nous avons défini la sémantique de l’abstrac-
tion en figure 5, bien que cela ne soit pas facile à voir sur l’exemple. Raisonnons
donc par analogie, en identifiant continuation et pile courante (plus compteur de
programme). La sémantique de la figure 5 demande à évaluer λx · u dans la pile κ
en retournant une fonction qui doit exécuter u dans la pile id, mais c’est absurde :
si jamais la fonction doit être appelée un jour dans le contexte d’une autre pile κ0 ,
alors u doit être évalué dans la pile κ0 . Il est donc nécessaire de modifier la définition
de sorte qu’elle prenne en paramètre la pile κ0 de l’appelant en plus de la valeur d
de l’argument x :
0
[[λx · u]]ρκ=κ((κ
ˆ , d) 7→ [[u]](ρ[x := d])κ0 )

et la sémantique de l’application uv doit tenir compte de ce changement : la valeur

f de u est maintenant une fonction qui prend non seulement la valeur d de v en
argument, mais aussi la pile courante κ ; f (κ, d) calcule alors la valeur u avec x valant
d dans la continuation κ. En particulier, comme κ est passée à f , c’est f (κ, d) qui
sera chargée de calculer tout le reste du programme, et on n’a donc pas besoin de
calculer κ(f (κ, d)). On pose alors :

[[uv]]ρκ=[[u]]ρ(f
ˆ 7→ [[v]]ρ(d 7→ f (κ, d)))

En résumé, on a obtenu la sémantique de la figure 6.

[[x]]ρκ =
ˆ κ(ρ(x))
   
f (κ, d) si f est une fonction binaire
[[uv]]ρκ =
ˆ [[u]]ρ f 7→ [[v]]ρ d 7→
⊥ sinon
[[λx · u]]ρκ =
ˆ κ((κ0 , d) 7→ [[u]](ρ[x := d])κ0 )
[[callcc k in u]]ρκ =
ˆ [[u]](ρ[k := κ])κ
[[throw k v]]ρκ =
ˆ [[k]]ρ(κ0 7→ [[v]]ρκ0 )

Figure 6 – Une sémantique en passage par valeur avec des sauts non locaux

Exercice 34 On pose let x = u in v =(λx

ˆ · v)u. Calculer [[let x = u in v]]ρκ.

Exercice 35 On appelle valeur au sens de Plotkin, ou P-valeur, les λ-termes qui

sont soit des variables soit des abstractions. Montrer que si V est une P-valeur,

36
[[(λx · u)V ]]ρκ = [[u[x := V ]]]ρκ. (On dit que la règle (βv ) : (λx · u)V → u[x := V ]
est valide.) Montrer que ce résultat ne se généralise pas au cas où V n’est pas une
P-valeur.

En Scheme, les constructions callcc. . .in et throw ne sont pas présentes telles
quelles. Comme k est une variable liée dans callcc k in u, on peut en effet s’arranger
pour la lier via un λ, et définir callcc k in u = call/cc(λk · u), où call/cc est
un opérateur primitif du langage. La sémantique (provisoire) de call/cc est :
0
[[call/cc]]ρκ=κ((κ
ˆ , f ) 7→ f (κ0 , κ0 ))

En fait, il est traditionnel lorsqu’on étudie les opérateurs de capture de conti-

nuation de faire de la valeur de la variable k de continuation directement une valeur
de fonction. En effet, la seule utilisation possible d’une continuation stockée dans k
est d’appeler throw k v. Posons k 0 =throw
ˆ k =λx
ˆ · throw k x : la valeur de k 0 est la
seule chose que call/cc a besoin de stocker. On définit donc (définitivement) :
0
[[call/cc]]ρκ=κ((κ
ˆ , f ) 7→ f (κ0 , (_, d0 ) 7→ κ0 (d0 )))

où (_, d0 ) 7→ κ0 (d0 ) est la fonction qui prend une continuation κ00 , une valeur d0 et
retourne κ0 (d0 ) après avoir jeté κ00 .

Exercice 36 Montrer que, si k est une variable telle que ρ(k) = f , alors [[λx ·
throw k x]]ρκ = κ((_, d) 7→ f (d)).

Exercice 37 Vérifier que, si k n’est pas libre dans u, alors [[call/cc(λk 0 · u)]]ρκ =
[[callcc k in u[k 0 := λx · throw k x]]]ρκ. (Pour faciliter le calcul, on remarquera
que λx · throw k x est une P-valeur, donc par l’exercice 35, il suffit de montrer que
[[call/cc(λk 0 · u)]]ρκ = [[callcc k in (λk 0 · u)(λx · throw k x)]]ρκ.)

Exercice 38 L’opérateur call/cc connaît de nombreuses variantes, notamment

l’opérateur C de Felleisen, dont la sémantique est :
0
[[C]]ρκ=κ((κ
ˆ , f ) 7→ f (_ 7→ ⊥, (_, d0 ) 7→ κ0 (d0 )))

où _ 7→ ⊥ est la fonction qui retourne toujours ⊥. Montrer que, pour tout t :

[[Ct]]ρκ = [[t]]ρ(f 7→ f (_ 7→ ⊥, (_, d0 ) 7→ κ(d0 )))

Exercice 39 Disons que u retourne normalement dans l’environnement ρ si et

seulement s’il existe une valeur d telle que pour toute continuation κ, [[u]]ρκ = κ(d) ;
si c’est le cas, d est appelée la valeur de u.
Montrer que si u retourne normalement dans ρ[k := (_, d0 ) 7→ κ(d0 )], alors
[[C(λk · u)]]ρκ = ⊥. (Autrement dit, si u retourne normalement, alors C(λk · u)
plante.)

Exercice 40 Montrer que l’on peut réaliser call/cc à l’aide de C. Plus précisé-
ment, on montrera que call/cc(λk · u) et C(λk · ku) ont la même sémantique.

L’opérateur C est souvent plus pratique pour les manipulations formelles que
call/cc. Faisons quelques calculs, dans l’espoir de découvrir quelques égalités sé-
mantiques entre termes. Notamment, que vaut C(λk · t) appliqué à v ? Intuitive-
ment, on va récupérer dans k la continuation consistant à appliquer la valeur f
de t à la valeur d de v, et ensuite appliquer la continuation courante κ à f (d).
Mais on peut récupérer la continuation courante dans une variable k 0 en écrivant
C(λk 0 ·. . .), et alors le calcul consistant à calculer t avec comme continuation la fonc-
tion qui prend la valeur f de t, l’applique à v et continue le calcul (par k 0 ) est donc

37
t[k := λf · k 0 (f v)] — ceci du moins tant que v est une P-valeur. Ceci suggère que
C(λk · t)v = C(λk 0 · t[k := λf · k 0 (f v)], au moins si v est une P-valeur. Plus générale-
ment, posons u=λk ˆ ·t, et comparons les deux quantités Cuv et C(λk 0 ·u(λf ·k 0 (f v))) :

[[Cuv]]ρκ = [[Cu]]ρ(g 7→ [[v]]ρ(d 7→ g(κ, d)))

= [[u]]ρ(f 7→ f (_ 7→ ⊥, (_, d0 ) 7→ (g 7→ [[v]]ρ(d 7→ g(κ, d)))(d0 )))
par l’exercice 38
= [[u]]ρ(f 7→ f (_ 7→ ⊥, (_, d0 ) 7→ [[v]]ρ(d 7→ d0 (κ, d))))

Tandis que :

[[C(λk 0 · u(λf · k 0 (f v)))]]ρκ

= [[λk 0 · u(λf · k 0 (f v))]]ρ(f 7→ f (_ 7→ ⊥, (_, d0 ) 7→ κ(d0 )))
= (f 7→ f (_ 7→ ⊥, (_, d0 ) 7→ κ(d0 )))((κ0 , d00 ) 7→ [[u(λf · k 0 (f v))]](ρ[k 0 := d00 ])κ0 )
= [[u(λf · k 0 (f v))]](ρ[k 0 := (_, d0 ) 7→ κ(d0 )])(_ 7→ ⊥)
= [[u]](ρ[k 0 := (_, d0 ) 7→ κ(d0 )])(g 7→ [[λf · k 0 (f v)]](ρ[k 0 := (_, d0 ) 7→ κ(d0 )])(d00 7→ g(_ 7→ ⊥, d00 )))
= [[u]]ρ(g 7→ [[λf · k 0 (f v)]](ρ[k 0 := (_, d0 ) 7→ κ(d0 )])(d00 7→ g(_ 7→ ⊥, d00 )))
à condition que k 0 ne soit pas libre dans u
= [[u]]ρ(g 7→ (d00 7→ g(_ 7→ ⊥, d00 ))((κ0 , g 0 ) 7→ [[k 0 (f v)]](ρ[k 0 := (_, d0 ) 7→ κ(d0 ), f := g 0 ])κ0 ))
= [[u]]ρ(g 7→ g(_ 7→ ⊥, (κ0 , g 0 ) 7→ [[k 0 (f v)]](ρ[k 0 := (_, d0 ) 7→ κ(d0 ), f := g 0 ])κ0 ))
= [[u]]ρ(g 7→ g(_ 7→ ⊥, (κ0 , g 0 ) 7→ [[k 0 ]](ρ[k 0 := (_, d0 ) 7→ κ(d0 ), f := g 0 ])
(f 0 7→ [[f v]](ρ[k 0 := (_, d0 ) 7→ κ(d0 ), f := g 0 ])(d 7→ f 0 (κ0 , d)))))
0 0
= [[u]]ρ(g 7→ g(_ 7→ ⊥, (κ , g ) 7→
(f 0 7→ [[f v]](ρ[k 0 := (_, d0 ) 7→ κ(d0 ), f := g 0 ])(d 7→ f 0 (κ0 , d)))((_, d0 ) 7→ κ(d0 ))))
= [[u]]ρ(g 7→ g(_ 7→ ⊥, (κ , g ) 7→ [[f v]](ρ[k 0 := (_, d0 ) 7→ κ(d0 ), f := g 0 ])(d 7→ κ(d))))
0 0

= [[u]]ρ(g 7→ g(_ 7→ ⊥, (κ0 , g 0 ) 7→ [[f ]](ρ[k 0 := (_, d0 ) 7→ κ(d0 ), f := g 0 ])

(f 0 7→ [[v]](ρ[k 0 := (_, d0 ) 7→ κ(d0 ), f := g 0 ])(d00 7→ f 0 (d 7→ κ(d), d00 )))))
= [[u]]ρ(g 7→ g(_ 7→ ⊥, (κ , g ) 7→ (f 0 7→ [[v]](ρ[k 0 := (_, d0 ) 7→ κ(d0 ), f := g 0 ])(d00 7→ f 0 (d 7→ κ(d), d00 )))(g 0 )))
0 0

= [[u]]ρ(g 7→ g(_ 7→ ⊥, (κ0 , g 0 ) 7→ [[v]](ρ[k 0 := (_, d0 ) 7→ κ(d0 ), f := g 0 ])(d00 7→ g 0 (d 7→ κ(d), d00 ))))
= [[u]]ρ(g 7→ g(_ 7→ ⊥, (κ0 , g 0 ) 7→ [[v]]ρ(d00 7→ g 0 (d 7→ κ(d), d00 ))))
à condition que k 0 et f ne soient pas libres dans v
= [[u]]ρ(g 7→ g(_ 7→ ⊥, (κ0 , g 0 ) 7→ [[v]]ρ(d00 7→ g 0 (κ, d00 ))))
car (d 7→ κ(d)) = κ

On a donc démontré :

Lemme 7 [[Cuv]]ρκ = [[C(λk 0 · u(λf · k 0 (f v)))]]ρκ, où k 0 et f sont deux variables

nouvelles.

Notons que ceci est correct même quand v n’est pas une P-valeur. On peut
directement formaliser le comportement de l’opérateur C par des règles de réécriture
inspirées de la sémantique :

(CL ) Cuv → C(λk 0 · u(λf · k 0 (f v)))

(CR ) V (Cu) → C(λk 0 · u(λx · k 0 (V x)))

où dans la seconde, V est une P-valeur.


Exercice 41 ( ) Montrer que la règle (CR ) est valide. (On utilisera le fait que
toute P -valeur V retourne normalement, cf. exercice 39, et en fait que [[V ]]ρκ = κ(d)
pour une valeur d qui ne dépend que de V et de ρ.) Montrer que l’hypothèse selon
laquelle V est une P-valeur est essentielle.

Nous avons ignoré les problèmes de définition de domaine de valeurs. Mais ceci
se règle aisément. Nous avons besoin d’un domaine D, les continuations κ seront

38
des éléments de [D → D], et les valeurs des fonctions seront des éléments de [[D →
D] × D → D]. Il suffit donc de prendre un domaine D tel que :
D = (N ∪ [[D → D] × D → D])⊥
à isomorphisme près, et où N peut être remplacé par n’importe quel autre ensemble
de valeurs de base. (Noter que les continuations ne sont pas incluses dans le domaine
des valeurs, car les continuations capturées par C sont codées comme des fonctions
dans [[D → D] × D → D].)

5.3 Ajout d’effets de bord

 


Nous allons maintenant voir quelques conséquences intéressantes de cette façon

de voir la sémantique des langages en appel par valeur.
La première est qu’il est maintenant facile de donner une sémantique à un lan-
gage enrichi d’effets de bord, sous la forme d’affectations. Voici, dans le style de
ML, les constructions que nous voulons ajouter : certains termes dénoteront des ré-
férences, c’est-à-dire des adresses en mémoire pointant vers des valeurs ; la construc-
tion !u retourne la valeur stockée à l’adresse u, la construction u := v stocke la valeur
de v à l’adresse u, et enfin ref u alloue une adresse l, y stocke la valeur de u, et
retourne l. Tant qu’à imiter les langages impératifs comme Pascal ou C, nous allons
aussi introduire une construction de séquencement u; v qui évalue u, puis évalue et
retourne la valeur de v.
Pour donner une sémantique formelle à ces constructions, on peut modifier notre
fonction [[_]] de sorte qu’elle prenne maintenant non seulement un environnement
ρ, une continuation κ, mais aussi une mémoire σ ∈ [L⊥ → D], où L est un ensemble
d’adresses (“locations” en anglais).
Noter que les continuations doivent maintenant non seulement prendre en argu-
ment la valeur calculée par un terme u, mais aussi le nouvel état de la mémoire. En
résumé, on aura les conventions de typage :

ρ ∈ V→D
σ ∈ [L⊥ → D]
κ ∈ [[L⊥ → D] × D → A]
où A est un domaine de réponses. Auparavant, A était juste le domaine D des
valeurs, mais il est aussi envisageable de vouloir prendre pour A le produit du
domaine D des valeurs avec celui, [L⊥ → D], des mémoires, par exemple, selon ce
que l’on souhaite observer à la fin du calcul.
Les valeurs de fonctions devront maintenant prendre une continuation, une va-
leur pour son argument, et une mémoire courante, et retourner une réponse. Notre
domaine sémantique doit aussi être enrichi par des adresses, et c’est pourquoi nous
posons :

D =
ˆ (N ⊕ L ⊕ [Cont × M em × D → A])⊥
Cont =
ˆ [M em × D → A]
M em =
ˆ [L⊥ → D]
où N pourrait être remplacé par n’importe quel autre ensemble de valeurs de
base. On peut alors définir notre sémantique comme en figure 7. (Exercice : vérifier
que la définition est cohérente avec le typage donné par les équations de domaine
pour D, Cont et M em.)

39
 [[x]]ρσκ =
ˆ κ(σ, ρ(x))
f (κ, σ 00 , d) si f est une fonction
   
[[uv]]ρσκ =
ˆ [[u]]ρσ (σ 0 , f ) 7→ [[v]]ρσ 0 (σ 00 , d) 7→
⊥ sinon
[[λx · u]]ρσκ =
ˆ κ(σ, (κ0 , σ 0 , d) 7→ [[u]](ρ[x := d])σ 0 κ0 )
κ(σ 0 , σ 0 (l)) si l est dans le domaine de σ 0
  
[[!u]]ρσκ =
ˆ [[u]]ρσ (σ 0 , l) 7→
⊥ sinon
κ(σ 00 [l := d], d) si l ∈ L
   
0 0 00
[[u := v]]ρσκ =
ˆ [[u]]ρσ (σ , l) 7→ [[v]]ρσ (σ , d) 7→
⊥ sinon
[[ref u]]ρσκ =
ˆ [[u]]ρσ((σ 0 , d) 7→ κ(σ 0 [l := d], l)) (l hors du domaine de σ 0 )
[[u; v]]ρσκ =
ˆ [[u]]ρσ((σ 0 , _) 7→ [[v]]ρσ 0 κ)

Figure 7 – Une sémantique en passage par valeur avec affectations

Exercice 42 Commenter la sémantique de la figure 6 en langage courant. En par-

ticulier, dire dans quel ordre cette sémantique spécifie que doivent être évaluées les
expressions, dans quelles continuations et quelles mémoires elles sont évaluées.

On peut bien sûr encore donner une sémantique à l’opérateur C dans ce contexte :

[[C]]ρσκ=κ(σ,
ˆ (κ0 , σ 0 , f ) 7→ f (_ 7→ ⊥, σ 0 , (_, σ 00 , d0 ) 7→ κ0 (σ 00 , d0 )))

Exercice 43 Soit ∗ un identificateur distingué (le handler d’exception courant).

On définit les constructions suivantes :

try u with x ⇒ v =
ˆ let k0 =! ∗ in
C(λk · ∗ := (λx · ∗ := k0 ; kv);
k(let y = u in ∗ := k0 ; y))
raise v =
ˆ !∗v

(Voir l’exercice 34 pour la construction let.) Justifier intuitivement pourquoi il

s’agit bien d’une gestion d’exceptions à la OCaml — et sous quelles conditions.

Alors qu’il était possible, quoique difficile, de trouver une sémantique par réduc-
tion pour C (les règles CL et CR ), il est pratiquement infaisable d’en trouver une
satisfaisante pour les affectations.

Références
[Bar84] Henk Barendregt. The Lambda Calculus, Its Syntax and Semantics, volume
103 of Studies in Logic and the Foundations of Mathematics. North-Holland
Publishing Company, Amsterdam, 1984.

A Modèles D∞
 


Fixons un dcpo pointé (D0 , ≤0 ), et construisons une suite de dcpo pointés

(Dk , ≤k ) par :
ˆ k → Dk ]
Dk+1 =[D

40
avec ≤k+1 l’ordre point à point, soit : pour tous f, g ∈ [Dk → Dk ], f ≤k+1 g si et
seulement si f (x) ≤k g(x) pour tout x ∈ Dk .
On peut construire une fonction i0 : [D0 → D0 ] → D0 par : i0 (f ) = f (⊥0 ) ; et
on peut construire une fonction r0 : D0 → [D0 → D0 ] par : r0 (x) = (v 7→ x) (une
fonction constante). Par récurrence, on définit ik+1 : [Dk+1 → Dk+1 ] → Dk+1 par :
ˆ k ◦ f ◦ rk ; et rk+1 : Dk+1 → [Dk+1 → Dk+1 ] par : rk+1 (x)=r
ik+1 (f )=i ˆ k ◦ x ◦ ik . On
a donc un diagramme infini :
r0
/ r1
/ r2
/ rk
/ rk +1
/
D0 o D1 o D2 o ... o Dk+1 o ...
i0 i1 i2 ik ik+1

avec ik ◦ rk l’identité sur Dk . (On remarquera que cette composition est dans le
mauvais sens, vu qu’on veut obtenir r ◦ i = id au final. On verra plus tard comment
ceci se résout.)

Exercice 44 Montrer par récurrence sur k que ik et rk sont continues.

Posons, pour k ≤ l, ikl : Dl → Dk =i ˆ k ◦ ik+1 ◦ . . . ◦ il−1 . Le système formé par les

Dk et les ikl , k ≤ l, est appelé un système projectif de dcpo pointés. Intuitivement,
ceci revient à voir les Dl se projeter via ikl dans Dk . On peut alors calculer la limite
projective de ce système, qui est un ensemble le plus petit possible D∞ se projetant
sur tous les Dk via des fonctions ik∞ :

Définition 6 On pose :

D∞ =
ˆ {(dk )k∈N | ∀k ≤ l · dk = ikl (dl )}
ik∞ (d0 , d1 , . . . , dk , . . .) =
ˆ dk
(dk )k∈N ≤∞ (d0k )k∈N ⇔ ∀k ∈ N · dk ≤k d0k

Une caractérisation équivalente est :

D∞ = {(dk )k∈N | ∀k · dk = ik (dk+1 )}

Lemme 8 (D∞ , ≤∞ ) est un dcpo, ik∞ : D∞ → Dk est continue pour tout k, et

ikl ◦ il∞ = ik∞ pour tout k ≤ l.

Preuve : (D∞ , ≤∞ ) est clairement un ordre partiel, etFsi (di )i∈I est une fa-
mille dirigée, avec di = (dij )j∈I , alors sa borne supérieure i di ne peut être que
ˆ F i di0 , iFdi1 , . . .) ; il ne reste qu’à montrer que d ∈ D∞ , autrement
F F
d=( ditFque
ikl ( i dil ) = i dik pour tout k ≤ l. Ceci revient à montrer que ik ( i dik+1 ) = i dik
F
pour tout k, sachant que dik = ik (dik+1 ) ; mais ik est continue, par l’exercice 44.
IlFest pratiquement évident que ik∞
F est continue : outre la monotonie, on a
ik∞ ( i di ) = ik∞ ( i di0 , i di1 , . . .) = i dik = i ik∞ (di ). Finalement, ikl ◦ il∞ =
F F F
ik∞ pour tout k ≤ l par les propriétés générales des limites projectives (mais vous
pouvez le vérifier directement). ♦
Donc D∞ se projette sur chaque Dk via les ik∞ . Ceci prend en compte la struc-
ture formée à partir des projections ik . On peut aussi tenir compte des rk , et définir
la construction duale : posons, pour k ≤ l, rkl : Dk → Dl =r ˆ l−1 ◦ . . . ◦ rk+1 ◦ rk .
(Noter que rkl va de Dk dans Dl , alors que ikl va de Dl dans Dk !) Le système formé
par les Dk et les rkl , k ≤ l, est appelé un système inductif de dcpo pointés. Ceci
revient à voir non pas Dl se projeter dans Dk , mais Dk s’injecter dans Dl via rkl .
On pourrait calculer la limite inductive de ce système, qui est en un sens le
plus grand ensemble s’injectant dans tous les Dk , et qui est construit comme le
quotient de la somme directe des Dk (dont les éléments sont des couples (k, dk )
avec dk ∈ Dk ) par la relation d’équivalence ∼ engendrée par (k, dk ) ∼ (l, dl ) si k ≤ l

41
et rkl (dk ) = dl . Il se trouve que dans ce cas précis, la limite inductive des Dk est
exactement la même que la limite projective D∞ (ce n’est en général pas le cas des
limites injectives et projectives) ; c’est pourquoi nous n’étudierons pas cette limite
inductive en tant que telle.
Lemme 9 Soit rk∞ : Dk → D∞ définie par :
rk∞ (d)=(i
ˆ 0k (d), i1k (d), . . . , i(k−1)k (d), d, rk(k+1) (d), rk(k+2) (d), . . .)
pour tout d ∈ Dk . Alors rk∞ est continue, et rl∞ ◦ rkl = rk∞ pour tout k ≤ l. De
plus, ik∞ ◦ rk∞ est l’identité sur Dk .
Preuve : La fonction rk∞ est bien définie, au sens où rk∞ (d) est bien dans D∞ ,
c’est-à-dire que ij (i(j+1)k (d)) = ijk (d) pour tout j ≤ k − 2 (par définition de ijk ),
i(k−1)k (d) = ik−1 (d) (par définition), d = ik (rk(k+1) (d)) (car rk(k+1) = rk et ik ◦rk =
id), et rkl (d) = il (rk(l+1) (d)) pour tout l ≥ k + 1 (car il ◦ rl = id).
La continuité de rk∞ provient du fait que tous les ijk , j ≤ k et tous les rkl ,
k ≤ l, sont continus, par l’exercice 44.
Pour vérifier que rl∞ ◦ rkl = rk∞ pour tout k ≤ l, on remarque d’abord que pour
tous j ≤ k ≤ l :
ijk ◦ ikl = ijl ijl ◦ rkl = ijk ijj = id
rkl ◦ rjk = rjl ikl ◦ rjl = rjk rjj = id
Les deux équations du milieu se démontrent en utilisant que im ◦ rm = id pour
tout m. Alors si k ≤ l, pour tout d ∈ Dk on a :
(rl∞ ◦ rkl )(d) = (i0l (rkl (d)), i1l (rkl (d)), . . . , i(l−1)l (rkl (d)),
rkl (d), rl(l+1) (rkl (d)), rl(l+2) (rkl (d)), . . .)
= (i0l (rkl (d)), . . . , i(k−1)l (rkl (d)), ikl (rkl (d)), i(k+1)l (rkl (d)), . . . , i(l−1)l (rkl (d)),
rkl (d), rl(l+1) (rkl (d)), rl(l+2) (rkl (d)), . . .)
= (i0k (d), i1k (d), . . . , i(k−1)k (d), d, rk(k+1) (d), . . . , rk(l−1) (d),
rkl (d), rk(l+1) (d), rk(l+2) (d), . . .)
= rk∞ (d)
Finalement, (ik∞ ◦ rk∞ )(d) = d par construction. ♦
Il s’ensuit que l’on peut considérer que Dk est inclus dans D∞ à isomorphisme
près : l’isomorphisme est rk∞ de Dk vers son image, et son inverse est la restriction
de ik∞ à l’image de rk∞ . En somme, D∞ est une sorte d’union de tous les Dk ; pour
être précis, de complété de cette union : un élément d=(d ˆ 0 , d1 , . . . , dk , . . .) est en
effet la limite (la borne supérieure) des dk , k ∈ I. C’est ce que dit le lemme suivant :
F
Lemme 10 Pour tout d ∈ D∞ , d = k (rk∞ ◦ ik∞ )(d), et (rk∞ ◦ ik∞ )k∈N est une
chaîne.
Preuve : Notons d’abord que : (a) pour tout k, pour tout f ∈ Dk+1 , rk (ik (f )) ≤k+1
f . En effet, ceci signifie que pour tout x ∈ Dk , rk (ik (f ))(x) ≤k f (x). Montrons-
le par récurrence sur k. Pour k = 0, r0 (i0 (f ))(x) = r0 (f (⊥0 ))(x) = f (⊥0 ) ≤0
f (x) puisque f est monotone. Sinon, rk+1 (ik+1 (f ))(x) = rk (ik+1 (f )(ik (x)) =
rk (ik (f (rk (ik (x))))) ≤k f (rk (ik (x))) (par récurrence) ≤k f (x) (par récurrence et
monotonie de f ).
Soit d = (d0 , d1 , . . . , dk , . . .) ∈ D∞ . On observe que : (b) rk (dk ) ≤k+1 dk+1 pour
tout k. En effet, dk = ik (dk+1 ) puisque d ∈ D∞ et on applique (a). Donc : (c)
rkl (dk ) ≤l dl pour tout k ≤ l. Alors :
F F
k (rk∞ ◦ ik∞ )(d) = Fk (rk∞ (dk ))
= Fk (i0k (dk ), i1k (dk ), . . . , i(k−1)k (dk ), dk , rk(k+1) (dk ), rk(k+2) (dk ), . . .)
= Fk (d0 , dF 1 , . . . , dk−1 , dk , rk(k+1)
F (dk ), rk(k+2) (dk ), . . .)
= ( (d0 ), (r01 (d0 ), d1 ), . . . , (r0k (d0 ), r1k (d1 ), . . . , r(k−1)k (dk−1 ), dk ), . . .)
= (d0 , d1 , . . . , dk , . . .) = d

42
par la remarque (c).
Finalement, (rk∞ ◦ ik∞ )k∈I est une chaîne car k ≤ l implique rk∞ ◦ ik∞ ≤
rl∞ ◦ il∞ . En effet :

(rk∞ ◦ ik∞ )(d) = (d0 , d1 , . . . , dk−1 , dk , rk(k+1) (dk ), rk(k+2) (dk ), . . . , rkl (dk ), rk(l+1) (dk ), . . .)
≤ (d0 , d1 , . . . , dk−1 , dk , dk+1 , dk+2 , . . . , dl , rk(l+1) (dk ), . . .)
= (rl∞ ◦ il∞ )(d)

par (a). ♦
On peut maintenant définir r et i sur D∞ :

Définition 7 Soit r la fonction de D∞ vers [D∞ → D∞ ] qui à

(y0 , y1 , . . . , yk , . . .) associe la fonction qui à (x0 , x1 , . . . , xk , . . .) ∈ D∞ associe
(y1 (x0 ), y2 (x1 ), . . . , yk+1 (xk ), . . .) ∈ D∞ .
Soit i la fonction de [D∞ → D∞ ] vers D∞ qui à f associe (d0 , d1 , . . . , dk , . . .)
défini par : d0 = i0∞ (f (r0∞ (⊥0 ))), dk+1 ∈ Dk+1 = [Dk → Dk ] est la fonction
ik∞ ◦ f ◦ rk∞ .

Lemme 11 Les fonctions r et i de la définition 7 sont bien définies, et continues.

De plus, r ◦ i est l’identité sur [D∞ → D∞ ] et i ◦ r est l’identité sur D∞ . En
particulier, D∞ et [D∞ → D∞ ] sont isomorphes.

Preuve : Pour montrer que r est bien définie, il faut montrer que pour tout
y =(y
ˆ 0 , y1 , . . . , yk , . . .) de D∞ , r(y) en tant que fonction qui à x = (x0 , . . . , xk , . . .)
associe (y1 (x0 ), y2 (x1 ), . . . , yk+1 (xk ), . . .) est bien continue. Ceci est ne présente pas
de difficulté, car les bornes supérieures sont prises composante par F composante
j
et chaque yk est continue. De même, r est continue parce que ( j yk+1 )(xk ) =
F j
j (yk+1 (xk )) par définition. De même, i est bien définie car i0 (d1 ) = d1 (⊥0 ) =
i0∞ (f (r0∞ (⊥0 ))) = d0 , et ik+1 (dk+2 ) = ik ◦ dk+2 ◦ rk (par définition de ik+1 )
= ik ◦ i(k+1)∞ ◦ f ◦ r(k+1)∞ ◦ rk = ik∞ ◦ f ◦ rk∞ = dk+1 , donc i(d) est bien dans
D∞ . De plus, i est continue parce que toutes les ik∞ et les rk∞ sont continues, et
que la composition ◦ est continue.
Avant de continuer, remarquons que dans un dcpo : (a) si on a une famille
0
dirigéeFd’élémentsFajj 0 telle que pour F tous j, Fj , il existe un k tel que ajj 0 ≤ akk ,
alors j,j 0 ajj 0 = k akk . En F effet k akk F ≤ j,j 0 ajj 0 parce que tous les akk sont
des ajj 0 , et réciproquement j,j 0 ajj 0 ≤ kjj0 akjj0 kjj0 (où kjj 0 est un k tel que
ajj 0 ≤ akk , pour tous j, j 0 ) ≤ k akk .
F
Soit f une fonction continue f de D∞ dans D∞ , d ∈ D∞ et posons ajj 0 =(r ˆ j∞ ◦
ij∞ )(f ((rj 0 ∞ ◦ ij 0 ∞ )(d))). Alors comme rj∞ ◦ ij∞ forme une chaîne (lemme 10) et
que f est monotone, ajj 0 ≤ akk pour k = max(j, j 0 ). Donc par (a), on a :
F F
k rk∞ (ik∞ (f (rk∞ (ik∞ (d)))) = Fj,j 0 (rj∞ ◦ ij∞ )(fF ((rj 0 ∞ ◦ ij 0 ∞ )(d)))
= j (r j∞ ◦ i j∞ )(f ( j 0 (rj ∞ ◦ ij ∞ )(d)))
0 0

par
F continuité de r j∞ ◦ i j∞ et de f
= (r
j j∞ ◦ i j∞ )(f (d)) = f (d) par le lemme 10
F
En résumé : (b) f (d) = k rk∞ (ik∞ (f (rk∞ (ik∞ (d)))).
Calculons maintenant r ◦ i. Pour toute f ∈ [D∞ → D∞ ], montrons que
F r(i(f ))(d) = f (d) pour tout d ∈ D∞ .
r(i(f )) = f . Pour ceci, il suffit de montrer que
Remarquons d’abord que : (c) r(i(f ))(d) = k rk∞ (ik∞ (r(i(f ))(d)) par le lemme 10.
Calculons donc ik∞ (r(i(f ))(d)). Posons i(f )=(y
ˆ 0 , . . . , yk , . . .) ; et d=(d
ˆ 0 , . . . , dk , . . .),
autrement dit dk = ik∞ (d) (puisque ik∞ ne fait que récupérer la composant numéro
k). Alors ik∞ (r(i(f ))(d)) = yk+1 (dk ) (par définition de r) = yk+1 (ik∞ (d)). Or par

43
définition yk+1 = ik∞ ◦ f ◦ rk∞ , donc ik∞ (r(i(f ))(d)) = ik∞ (f (rk∞ (ik∞ (d)))). Par
(c) : F
r(i(f ))(d) = Fk rk∞ (ik∞ (r(i(f ))(d))
= k rk∞ (ik∞ (f (rk∞ (ik∞ (d))))
= f (d)
en utilisant la remarque (b). C’était la partie la plus compliquée à montrer.
Calculons maintenant i ◦ r. Fixons y =(y ˆ 0 , y1 , . . . , yk , . . .) dans D∞ . La fonction
f =r(y)
ˆ envoie tout x=(x
ˆ 0 , x1 , . . . , xk , . . .) vers (y1 (x0 ), y2 (x1 ), . . . , yk+1 (xk ), . . .).
Et i(r(y)) = i(f ) est alors un élément (d0 , d1 , . . . , dk , . . .) tel que, d’une part,
d0 = i0∞ (f (r0∞ (⊥0 ))) = y1 (x0 ) avec x0 la composante 0 de r0∞ (⊥0 ), soit
x0 = i0∞ (r0∞ (⊥0 )) = ⊥0 , donc d0 = y1 (⊥0 ) = y0 ; d’autre part, dk+1 est la
fonction qui à xk associe ik∞ (f (rk∞ (xk ))) = yk+1 (ik∞ (rk∞ (xk ))) = yk+1 (xk ), donc
dk+1 = yk+1 . Donc (i ◦ r)(y) = y, pour tout y. ♦

Exercice 45 Montrer que la règle (η) est valide dans D∞ , autrement dit que [[λx ·
ux]]ρ = [[u]]ρ dès que x n’est pas libre dans u. (On pourra commencer par le prouver
dans le cas où u est une variable y 6= x, et remarquer ensuite que (λx · yx)[y :=
u] = λx · ux.)

Exercice 46 Supposons que D0 n’est pas trivial, montrer alors que dans D∞ ,
[[Ω]]ρ = ⊥ et que [[λx · x]] = i(id) 6= ⊥. Déduire de l’exercice précédent que le λ-
calcul avec βη-réduction est cohérent, au sens où il existe deux termes u et v tels
que u 6=βη v (ici, Ω et λx · x).

Ce dernier résultat peut aussi se montrer en prouvant que la βη-réduction est

confluente, et en remarquant ensuite qu’Ω et λx · x n’ont aucun rédex commun.

44