14

Chapitre 2

Sémantique à réduction et correction du typage

Dans le premier chapitre, nous avons introduit le langage ML et nous l’avons défini en donnant une sémantique à grands pas ; nous en avons déduit un évaluateur pour ML. Nous avons constaté que la sémantique à grands pas ne permet pas de parler des programmes qui bouclent.

Dans ce chapitre, nous présentons une autre sémantique opérationnelle, la sémantique à réduction (ou encore à petits pas) qui est une alternative à la sémantique à grands pas. Elle est plus simple, plus précise, plus modulaire, mais elle est moins concrète, c’est-à-dire qu’elle modélise le calcul de façon plus éloignée d’un interprète.

2.1 Sémantique à petits pas

Dans le λ-calcul, une étape d’évaluation correspond à une β-réduction. À partir d’un terme, il existe en général plusieurs chemins de réduction possibles. Le λ-calcul possède la propriété Church-Rosser qui énonce qu’il est toujours possible de rejoindre deux chemins. Ainsi si un terme est fortement normalisable, c’est-à-dire si tous les calculs terminent, alors ils terminent sur une même forme normale. Le calcul est déterministe.

La réduction dans le λ-calcul est une très bonne modélisation de l’évaluation. Il n’est pas nécessaire que la réduction soit Church-Rosser pour modéliser le calcul. D’une part, il est en général possible de limiter le nombre de chemins autorisés en limitant les contextes dans lesquels la réduction peut se faire (on choisira par exemple une stratégie d’évaluation en appel par valeur), ce qui suffit bien souvent à rendre le calcul déterministe. D’autre part, dans une langage typé, il est souvent possible de modéliser un calcul non-déterministe et de montrer la conservation du typage le long de tous les chemins de réduction possibles ; cela permet non seulement de partager les preuves de correction de plusieurs stratégies, mais également d’énoncer un résultat de correction plus fort.

Dans une sémantique à réduction, les résultats de l’évaluation sont les valeurs. Dans le λ-calcul, ce sont donc les fonctions. En ML, il existe d’autres valeurs que les fonctions, par exemple les constantes, ou plus généralement les valeurs construites.

Donner une sémantique à réduction à petits pas pour le langage ML, c’est donc définir, comme pour le λ-calcul, une relation de réduction des programmes sur euxmêmes. Lorsque c’est possible, il est commode de définir cette relation de la façon modulaire suivante.

1. Définir les valeurs

Tout d’abord nous devons définir le sous-ensemble des expressions qui sont des valeurs :

v ::= c^{k} v_{1} … v_{q}  (q < k)  constantes partiellement appliquées
| C^{k} v_{1} … v_{q}  (q ≤ k)  valeurs construites
| fun (x) a

Nous précisons ainsi la distinction entre constructeurs et primitives. Lorsqu’ils sont totalement appliqués à des valeurs, les constructeurs forment des valeurs, mais pas les primitives. Partiellement appliquées, les constantes sont toujours des valeurs. Par exemple, une paire ( , ) 1 2, notée (1, 2) est une valeur, mais une addition ( + ), notée 1 + 2 n’est pas une valeur.

Nous dirons que les valeurs de la forme C^{k} v_{1} … v_{k} sont des valeurs construites et que les autres valeurs sont des valeurs fonctionnelles.

2. Définir les radicaux et leurs réduits

Les réductions sont d’abord définies pour chaque radical. Pour simplifier la lecture, nous écrirons a_{1} ⟶^{ϵ} a_{2} pour les réductions en tête, i.e. les réductions de radicaux, et plus généralement a_{1} ⟶ a_{2} pour une réduction à une position quelconque dans le terme. Le noyau ML sans constantes n’est qu’un sous-ensemble du λ-calcul non typé, et la seule réduction de radical est la β-réduction, qui prend toutefois deux formes syntaxiques différentes (la construction Let est une façon de marquer certains radicaux présents dans le programme initial) :

(fun (x) a) v ⟶^{ϵ} a[v/x]  (β_{v})
let x = v in a ⟶^{ϵ} a[v/x]  (β_{let})

Dans l’écriture de la β-reduction, a et v sont quelconques, donc les règles s’appliquent pour toute expression a et toute valeur v. Bien entendu, le renomage [v/x] ne doit substituer que les occurences de la variable x qui sont libres dans a.

Nous ajoutons également un ensemble de δ-règles qui décrivent la façon de réduire les primitives. Elles sont de la forme :

f^{k} v_{1} … v_{k} ⟶^{ϵ} a  (δ_{f})

On note aussi parfois a_{1} ⟶^{δ} a_{2} pour dire que a_{1} ⟶^{ϵ} a_{2} par une δ-règle. Attention ! ici les v_{i} et a ne sont pas des paramètres formels universellement quantifiés, mais des valeurs précises qui dépendent de la δ-règle. Une δ-règle associée à une primitive f d’arité k est donc définie par une paire (v̄, a) où v̄ est un k-tuple de valeurs. Une primitive peut avoir plusieurs δ-règles associées, voir même une infinité (dénombrable). Par exemple, nous verrons ci-dessous que les paires peut être modélisées par un constructeur ( , ) et deux primitives fst et snd. Nous avons alors pour toutes valeurs v_{1} et v_{2} deux δ-règles

fst (v_{1}, v_{2}) ⟶^{δ} v_{1} snd (v_{1}, v_{2}) ⟶^{δ} (v_{1}, v_{2})

Il existe donc une infinité de δ-règles associées à la primitive fst. Cependant, dans certains cas comme ci-dessus pour fst, il existe toutes les règles ont un même forme, et on peut les voir comme une seule règle où v_{1} et v_{2} ne sont plus des valeurs mais des méta-variables de valeurs universellement quantifiés (comme pour la β-règle). Ceci n’est pas toujours possible. Par exemple, la fonction successeur peut être modélisée par une infinité de réductions succ 0 ⟶^{δ} 1, succ 1 ⟶^{δ} 2, etc. Cependant on ne peut plus regrouper ces règles en une seule règle avec des méta-variables de valeurs comme pour

fst.

A l’inverse, les constructeurs n’ont jamais de règles de réduction associées, puisque ce sont des valeurs.

Décrire les contextes d’évaluation

Il faut maintenant décrire les endroits où il est possible de réduire un radical. Pour cela, on définit un ensemble de contextes d’évaluation. Dans le λ-calcul, les contextes d’évaluation sont tous les contextes à un trou. En ML, la stratégie d’évaluation est l’appel par valeur et les contextes d’évaluation par valeur sont :

E ::= [] | E a | v E | let x = E in a

Permettre de réduire dans un contexte d’évaluation

Pour cela, on ajoute la règle d’évaluation suivante qui exprime que la réduction peut se produire également à l’intérieur d’un terme :

si a_{1} ⟶^{ϵ} a_{2}, alors E[a_{1}] ⟶ E[a_{2}]  (Contexte)

Formellement la relation de réduction ⟶ est définie comme la plus petite relation satisfaisant les règles β, β_{Let} et Contexte et contenant l’ensemble de toute les δ-règles données en hypothèses.

La plupart des langages de programmation ont une sémantique déterministe, c’està-dire qu’il n’y a qu’une seule évaluation possible. Toutefois, certains langages ont une sémantique non déterministe. Soit parce que la sémantique n’est pas entièrement spécifiée, par exemple l’ordre d’évaluation des arguments, soit parce que cela est essentiel, par exemple dans un langage parallèle.

Lorsque la sémantique d’un langage est déterministe, c’est souvent parce qu’il n’existe qu’un chemin de réduction possible, ce qui découle en général immédiatement de la définition des contextes d’évaluation. Il se peut aussi qu’il existe plusieurs chemins de réduction qui mènent à la même valeur, ou divergent tous simultanément. Mais ceci n’est même pas vrai pour le λ-calcul, car selon l’ordre d’évaluation des arguments, un programme peut diverger ou terminer.

Exercice 1 (*) Dans le λ-calcul réduire le terme let f = fun (y) y in (fun (z) z) f de deux façons différentes, et vérifier que les deux calculs aboutissent au même résultat. Vérifier que le programme ci-dessus ne peut plus être réduit que d’une seule façon en appel par valeur.

Exercice 2 (*) Plus généralement, vérifier que les contextes d’appel par valeur cidessus ne permettent qu’un seul chemin de réduction. Le calcul est donc trivialement déterministe.

Exercice 3 (*) Quelles modifications faut-il apporter à la définition de la sémantique à petits pas pour modéliser l’appel par nom (on ignorera les constantes) ?

Les évaluations possibles d’un programme sont :

a ⟶ a_{1} ⟶ … \{ \begin{matrix}v & le programme s’évalue en la valeur v \\ a_{n}(≠ v∧ −̸→ a_{n+1}) & l’évaluation est bloquée \\ a_{n} ⟶ … & l’évaluation se poursuit indéfiniment \end{matrix}

L’erreur est simplement modélisée par une évaluation bloquée. Pour montrer qu’un programme ne produit pas d’erreur à l’exécution, il faut montrer qu’une réduction quelconque issue de ce programme ne peut jamais être bloquée.

S’il n’y pas de constante, cela est immédiat, même pour les programmes non typables. Dès que le langage contient des constantes, il est possible que des programmes soient bloqués. Par exemple, le programme c a si c est une constante d’ordre 0 qui ne possède pas de δ-règle.

Exercice 4 (*) Vérifiez que pour qui ne contiennent pas de constantes, l’évaluation ne peut jamais être bloquée, que ces termes soit ou non bien typés.

Exercice 5 (programmation) On se propose d’écrire un programme qui évalue les expressions du noyau ML en suivant les définitions de ce chapitre. Écrire un type concret expr représentant les expressions a du langage noyau. Les valeurs seront représentées par un prédicat est une valeur sur les expressions. Un contexte E pourra être représenté par l’expression fun (x) E[x]. Écrire une fonction qui retourne les décompositions possibles d’un terme a en paires (E, a′) telles que E[a′] est égal à a et a′ n’est pas une valeur. Définir les règles de réduction (c’est une fonction prenant un terme a et

Écrire une fonction qui calcule la substitution de x par v dans a. Une règle de réduction est une fonction qui associe un programme a_{2} à un programme a_{1} où échoue si a_{1} n’est pas le radical correspondant. Définir les règles de réduction de radicaux indépendemment les unes des autres. Définir une étape de réduction (en prenant en paramètre une liste de règle de réduction). Enfin définir la réduction comme une succession d’étapes de réductions.

Une constante sera représentée par un identificateur, une arité, et une information dépendant du type primitive ou constructeur. En particulier, les primitives seront données avec leurs delta-règles. (i.e. représentés par une fonction).

On se donnera les entiers et les booléens comme constantes initiales. Évaluer quelques exemples, en traçant les différentes étapes de la réduction (on pourra aussi marquer les expressions réduites).

2.2 Correction du typage vis à vis de la sémantique

La correction du typage revient à montrer que les programmes bien typés ne sont jamais bloqués. Ceci est garanti par les deux propriétés suivantes :

1. Si A ⊢ a_{1} : τ et a_{1} ⟶ a_{2} alors A ⊢ a_{2} : τ.

2. Si A_{0} ⊢ a : τ et a −̸→ alors a_{1} est une valeur.

où A_{0} est l’environnement composé uniquement de déclarations de constantes.

La première propriété énonce que le typage est conservé par réduction. Cette propriété est en général indépendante de la stratégie d’évaluation. La seconde dit simplement que les programmes bien typés ne sont pas immédiatement erronés. Nous pouvons souligner ici l’avantage d’une sémantique à petits pas. La première propriété garantit la correction de l’évaluation, même pour les programmes qui ne terminent pas. En particulier, elle assure que l’évaluation infinie d’un programme bien typé qui diverge se déroule aussi normalement.

Pour simplifier, il est commode de définir une relation de typabilité entre les expressions : nous dirons que l’expression a_{2} est au moins aussi typable que l’expression a_{1}, et nous noterons a_{1} ⊑ a_{2}, si

∀A, ∀τ, (A ⊢ a_{1} : τ) ⟹ (A ⊢ a_{2} : τ)

On peut voir ici la relation de typabilité comme induite par l’inclusion des ensembles de typage d’une expression, c’est-à-dire l’ensemble des paires (A, τ) telles que A ⊢ a : τ.

Nous avons vu que la présence de primitives s’accompagne, en général, de δ-règles. Il est clair que ces règles ne peuvent pas être arbitraires sans invalider la correction du typage.

Hypothèse Étant donné un environnement de typage initial A_{0}, nous faisons les hypothèses suivantes.

H0 On suppose que le domaine de A_{0} est restreint à des constantes, que A_{0}(C^{n}) est de la forme ∀ ᾱ. τ_{1} → … τ_{n} → τ_{0} et τ_{0} n’est pas une flèche.

H1 si a_{1} ⟶_{δ} a, alors a_{1} ⊑ a_{2} et

H2 si A_{0} ⊢ f^{k} v_{1} … v_{k} : τ, alors il existe une expression a telle que f^{k} v_{1} … v_{k} ⟶_{δ} a.

La première affirme que les δ-règles préservent le typage. C’est clairement nécessaire, puisque nous voulons montrer que cette propriété s’étend à une réduction quelconque. La seconde hypothèse assure qu’une application complète et bien typée d’une primitive à des valeurs peut toujours se réduire. C’est-à-dire, plus informellement, qu’il existe assez de δ-règles pour réduire les primitives.

Les deux théorèmes 1 et 2 ci-dessous expriment la sécurité du typage :

Théorème 1 (Auto-réduction) La réduction conserve les typages (i.e. ⟶ est une sous relation de ⊑ ).

En utilisation la notation mathématique (une relation est un graphe) il s’agit donc de montrer (⟶) ⊂ (⊑). Comme la relation ⟶ est la plus petite relation satisfaisant les règles β, δ et Contexte, il suffit en fait de montrer que

Le théorème d’auto-réduction (subject reduction) découle donc de immédiatement de la croissance de ⊑ (lemme 4) et du lemme de contraction des radicaux (lemme 5) qui suivent.

Par construction, la relation ⊑ est réflexive et transitive ; le lemme de remplacement énonce qu’elle est aussi croissante (avec la structure de termes).

Lemme 4 (Croissance de ⊑) Pour tout contexte E, si a_{1} ⊑ a_{2} alors E[a_{1}] ⊑ E[a_{2}].

\underline{Preuve} : Par récurrence structurelle sur le contexte E. Soit A un environnement de typage et τ un type tels que A ⊢ E[a_{1}] : τ (1). Nous montrons que A ⊢ E[a_{2}] : τ.

Cas E est [ ] : trivial.

Cas E est let x = E′ in a: Une dérivation de (1) se termine par :

A ⊢ E′[a_{1}] : τ_{1} (2) A ⊕ (x : Gen(τ_{1}, A)) ⊢ a : τ (Let)

A ⊢ let x = E′[a_{1}] in a : τ

Par l’hypothèse de récurrence appliquée à (2), nous savons que A ⊢ E′a_{2} : τ_{1}, et la conclusion suit en remplaçant a_{1} par a_{2} dans la dérivation ci-dessus.

Cas E est E′ a_{1} ou v E′: Ces deux cas sont aussi simples que celui du Let.

Lemme 5 (Contraction de radicaux) Si a_{1} ⟶_{ϵ} a_{2} alors a_{1} ⊑ a_{2}.

Chaque cas de radical peut être traité indépendamment. Pour les radicaux δ, il suffit d’appliquer l’hypothèse (H1). Pour les radicaux β, on utilise le lemme de remplacement dans un contexte.

2.2. CORRECTION DU TYPAGE VIS À VIS DE LA SÉMANTIQUE 21

Lemme 6 (Remplacement dans un terme) Si les formules A ⊢ v : τ_{0} (1) et A ⊕ (x : ∀ ᾱ_{0}. τ_{0}) ⊢ a : τ (2) sont prouvables et si les variables ᾱ_{0} ne sont pas libres dans A, alors A ⊢ a[v/x] : τ (3) est prouvable.

En fait, on pourrait montrer ce lemme dans le cas plus général où v est remplacé par une expression b dont les variables libres ne sont pas liées dans a.

\underline{Preuve} : La preuve se fait par récurrence sur la structure de a. Nous écrivons A_{x} pour A ⊕ (x : ∀ ᾱ_{0}. τ_{0}).

Cas a est x: Les termes a[v/x] et v sont égaux. De (2), nous savons que τ est τ_{0} où toutes les variables ᾱ_{0} ont été substituées. La stabilité par substitution du typage appliquée à (1) montre (3).

Cas a est x_{1} et x_{1} ≠ x: Les termes a[v/x] et a sont identiques et x_{1} n’y figure pas libre. Il suffit d’appliquer le lemme d’extension de contexte à (2).

Cas a est let x_{1} = a_{1} in a_{2} : Une dérivation de (2) se termine par :

(4) A_{x} ⊢ a_{1} : τ_{1} (5) A_{x} ⊕ (x_{1} : Gen(τ_{1}, A_{x})) ⊢ a_{2} : τ (Let)

A_{x} ⊢ let x_{1} = a_{1} in a_{2} : τ

Par l’hypothèse de récurrence appliquée à (4), nous savons que A ⊢ a_{1}[v/x] : τ_{1} (6).

Si x_{1} est égal à x, alors a[v/x] est égal à let x = a_{1}[v/x] in a_{2}. La premisse (5) s’écrit alors A ⊕ (x : Gen(τ_{1}, A_{x})) ⊢ a_{2} : τ. Par généralisation de contexte (propriété ? ?, page ) nous avons A ⊕ (x : Gen(τ_{1}, A)) ⊢ a_{2} : τ (70), puisque A est une sous-séquence de A_{x}. On conlut par l’application d’une règle Let avec les prémisses (6) et (70).

Sinon, par généralisation du contexte (propriété 3, page 13) appliqué à (5), nous déduisons A_{x} ⊕(x_{1} : Gen(τ_{1}, A)) ⊢ a_{2} : τ, puisque A est une sous-séquence de A_{x}. Notons A_{1} le contexte A ⊕ (x_{1} : Gen(τ_{1}, A)). Par réarrangement du contextes (propriété 2, page 12), on obtient A_{1} ⊕ (x : ∀ ᾱ_{0}. τ_{0}) ⊢ a_{2} : τ (8). Comme v est une valeur, x_{1} n’est pas libre dans v. Donc, par extension de contexte (propriété 2, page 12) appliqué à (7), nous avons A_{1} ⊢ v : τ_{0} (9). Les variables ᾱ_{0} ne sont pas libre dans A_{1}, car les variables libres dans A_{1} sont aussi libres dans A. En appliquant l’hypothèse de récurrence à (9) et (8), nous obtenons :

A_{1} ⊢ a_{2}[v/x] : τ (10)

Nous concluons par l’application de la règle Let à (10) et (6).

Cas a est fun (x_{1}) a_{1} : Si les variables de τ̄_{0} apparaissent dans τ, nous pouvons les renommer en des variables prisent en dehors des variables libres de A par une substitution θ. Sinon, nous prenons θ égale à l’identité. Par application de la substitution θ (propriété 1, page 12) au jugement2, nous avons A ⊢ a : θ(τ).

Nécessairement, θτ est de la forme τ_{1} → τ_{2}, et il existe une dérivation de (2) qui se termine par :

1\begin{aligned}(11) 1A_{x} ⊕ (x_{1} : τ_{1}) ⊢ a_{1} : τ_{2} \\ & (Let) \\ A_{x} ⊢ fun (x_{1}) a_{1} : τ_{1} → τ_{2} \end{aligned}

Si x_{1} est égal à x, alors a[v/x] est égal à a, et il n’y a rien à montrer.

22 CHAPITRE 2. SÉMANTIQUE À PETITS PAS

Sinon, notons A_{1} le contexte A ⊕ x_{1} : τ_{1}. Par réarrangement du contexte (propriété 2), appliquée à (111), nous avons A_{1} ⊕ (x : ∀ α_{0}. τ_{0}) ⊢ a_{1}[v/x] : τ (122).

Comme ci-dessus pour le cas Let, nous avons A_{1} ⊢ v : τ_{0} (13). Comme nous avons supposé les variables τ̄_{0} ne sont pas libres dans τ, donc en particulier τ_{1}, elles ne sont pas non plus libres dans A_{1}. En appliquant l’hypothèse de récurrence à (13) et (122), nous obtenons :

A_{1} ⊢ a_{1}[v/x] : τ.

Par application de la règle Fun, nous obtenons A ⊢ a[v/x] : θτ. Nous concluons par application de la substitution θ^{−1} (propriété 1, page 12).

Cas a est a_{1} a_{2} ou fun (x) a_{1} : Ces cas sont plus faciles que le cas Let.

\underline{Preuve} : (de la contraction de radical) Soit A un environnement de typage et τ un type tel que A ⊢ a_{1} : τ (1). Nous montrons que A_{2} ⊢ a_{2} : τ (2) par cas sur le radical a_{1}. Chaque cas peut être vérifié indépendamment.

Cas a_{1} est (fun (x) a) v: Une dérivation de (1) se termine par :

\begin{aligned}(3) A_{1} ⊕ (x : τ_{1}) ⊢ a : τ \\ & (Fun) \\ A_{1} ⊢ a : τ_{1} → τ \end{aligned} (4) A_{1} ⊢ v : τ_{1} (App)

A_{1} ⊢ a_{1} : τ

Le lemme précédent appliqué à (4) et (3) conduit directement à la conclusion.

Cas a_{1} est let x = v in a: Une dérivation de (1) se termine par :

(5) A_{1} ⊢ v : τ_{1} (6) A_{1} ⊕ (x : Gen(τ_{1}, A)) ⊢ a : τ (Let)

A_{1} ⊢ let x = v in a : τ

Nous concluons en appliquant le lemme de remplacement de termes à (5) et (6) avec A_{1} pour A_{2}.

Cas a_{1} est c^{k} v_{2} … v_{k}: Il s’agit donc d’une réduction a_{1} ⟶_{δ} a_{2}. La première partie de l’hypothèse sur les δ-règles fournit directement la conclusion.

En utilisant une généralisation du lemme 6, il n’est pas nécessaire que l’expression liée par un Let soit une valeur. On pourrait montrer que le typage est conservé par réduction forte des expressions de liaisons, c’est-à-dire en effectuant la réduction

let x = a_{1} in a_{2} ⟶ a_{2}[a_{1}/x]

dans un contexte quelconque. Notons â le terme obtenu, qui ne contient donc plus de liasons Let. Nous avons a ⊑ â, et puisque â ne comporte plus de Let, l’expression â est typable dans le calcul simplement typé.

On peut se demander si l’inverse de l’auto-réduction est également vérifié, ce qui signifierait que la réduction n’ajoute pas de typages, c’est-à-dire si

a_{1} ⟶ a_{2} ⟹^{?} a_{2} ⊑ a_{1}

2.2. CORRECTION DU TYPAGE VIS À VIS DE LA SÉMANTIQUE 23

Cette propriété est fausse car la réduction perd des morceaux de termes : il suffit de considérer, par exemple, le programme (fun (x) a_{1}) a_{2} où le programme a_{1} est typable, mais pas a_{2}. Toutefois, on pourrait montrer qu’en remplaçant la règle Gen-Let par la règle suivante

\frac{A ⊢ a_{1} : τ_{1} A ⊢ a_{2}[a_{1}/x] : τ_{2}}{A ⊢ let x = a_{1} in a_{2} : τ_{2}}

on conserverait les mêmes typages.

Théorème 2 (Formes Normales) Les expressions irréductibles et bien typées dans l’environnement initial sont des valeurs.

Ce théorème énonce que les termes bien typés qui ne peuvent être réduits sont des valeurs, en conséquence l’évaluation des termes bien typés n’est jamais bloquée.

\underline{Preuve} : Nous montrons d’abord que si A_{0} ⊢ v : τ alors

• Si τ est un type fonctionnel, alors v est une valeur fonctionnelle,

• Si τ est une valeur construite, alors v est une valeur construite.

Il suffit pour cela de montrer que :

• Si v est une valeur fonctionnelle, alors τ est un type fonctionnel,

• Si v est une valeur construite, alors τ est une valeur construite.

En effet 1- les valeurs fonctionnelles et les valeurs construites forment une partition de l’ensemble des valeurs, et 2- les types fonctionnnel et les types construits forment une partition (d’un sous ensemble des types). Chaque cas se vérifie très facilement par analyse de la dérivation de typage.

La preuve est une récurrence structurelle sur a. Nous supposons que a : τ (1) pour un certain type τ et que a ne peut pas être réduit.

Cas a est z: Puisque a est clos, z est une constante ; c’est donc une valeur.

Cas a est a_{1} a_{2} : Une dérivation de (1) montre qu’il existe un type τ_{1} tel que a_{1} : τ_{1} → τ et a_{2} : τ_{2}. L’hypothèse de récurrence appliquée à chacune des prémisses montre que a_{1} et a_{2} sont des valeurs. En particulier, comme a est irréductible, a_{1} ne peut pas être une fonction ; c’est donc une constante partiellement appliquée, c’est-à-dire de la forme c^{k} v_{1} … v_{q}; ainsi a est de la forme c^{k} v_{1} … v_{q} v. Comme a est irréductible, l’hypothèse (H2) implique que c n’est pas une primitive complétement appliquée, c’est donc un constructeur, ou une primitive patiellement appliquée dans a. Dans les deux cas, a est une valeur.

Cas a est let x = a_{1} in a_{2} : Une dérivation de (1) se termine par :

(1) A ⊢ a_{1} : τ_{1} … (Let)

A ⊢ let x = a_{1} in a_{2} : τ_{2}

L’hypothèse de récurrence appliquée à (1) montre que a_{1} est une valeur. Donc a pourrait être réduit.

Cas a est fun (x) a_{1} : Alors a est une valeur.

2.3 Quelques extensions “gratuites” du langage

Pour illustrer l’intérêt d’avoir paramétrer la définition du langage et donc les preuves par un ensemble de primitives, nous décrivons quelques instances.

L’ajout des paires est la plus simple sans doute, et nous la traitons en détails. D’un autre coté, une extension très générale consiste à ajouter des types concrets et du filtrage. Nous laissons en exercice l’ajout de booléens. Nous la traitons dans un cas particulier. Les booléens, les paires, etc. sont des cas particulier de types concrets.

Les paires

Pour étendre le langage avec des paires, il nous faut d’abord choisir un constructeur de type pour les paires.

g ::= ( ∗ )

puis un constructeur de valeurs ( , ) d’arité 2 et deux fonctions de projections (i.e. deux primitives) fst et snd avec les δ-règles suivantes :

fst (v_{1}, v_{2}) ⟶_{r} v_{1}  (Fst)
snd (v_{1}, v_{2}) ⟶_{r} v_{2}  (Snd)

Le typage des primitives est donné par l’environnement de typage initial suivant :

\begin{matrix}( , ) : & ∀ α_{1}, α_{2}. α_{1} → α_{2} → (α_{1} ∗ α_{2}) \\ fst : & ∀ α_{1}, α_{2}. (α_{1} ∗ α_{2}) → α_{1} \\ snd : & ∀ α_{1}, α_{2}. (α_{1} ∗ α_{2}) → α_{2} \end{matrix}

Pour bénéficier de l’étude précédente, et en déduire la correction du typage pour le langage avec paires, il suffit de vérifier que les hypothèses sont satisfaites.

\underline{Preuve} : En effet,

H0 : Cette hypothèse est satisfaite par construction.

H1 : En analysant pour chaque δ-règles les dérivations de typage possibles pour le terme de gauche, et on en déduit facilement le typage du terme de droite.

H2 : On remarque que le la seule valeur construite est la paire Les valeurs bien typés dans l’environnement initial de la forme qui ont un type construit sont donc des paires.

Nous pouvons maintenant vérifier la seconde proporiété par cas sur chaque constante :

Sous-cas (v_{1}, v_{2}) v_{3} : Ceci n’est pas possible car ce programme n’est pas typable.

Sous-cas fst v: Une dérivation de ce programme impose que A_{x} ⊢ v : τ_{1} ∗ τ_{2}. Une valeur de ce type est nécessairement de la forme (v_{1}, v_{2}), donc le programme initial est réductible.

Sous-cas snd v: Ce cas est symétrique du précédent.

Exercice 6 Formaliser directement le cas des booléens. Vérifier que toutes les propriétés restent valables (refaire leur démonstration, en faisant bien attention à leur structures ; on laisser de coté les branches de la preuve inchangée par rapport au noyau).

Exercice 7 (**) Définir les paires de façon primitive, en étendant le langage. Vérifier que les preuves peuvent être étendues. Les nouveaux cas sont-ils des sous-cas des constantes ?

Exercice 8 (***) On note ML_{1} le langage où les paires sont ajoutées comme des constantes et ML_{2} le langage où elle sont ajoutées de façon primitive. Proposer une traduction des programmes de ML_{2} dans ML_{1}. Montrer que la traduction commute avec la réduction. Peut on faire un codage dans le sens inverse ? Comment montrer que les deux sont équivalents ?

Les tuples peuvent être ajoutés au langage de façon similaire, ou bien simplement codés à partir des paires. En fait, il est fréquent (c’est plus simple mais plus long) de formaliser les paires directement dans le langage ; on peut alors se limiter à des primitives ou des constructeurs d’artité 0 ou 1, les arguments multiples étant remplacés par des tuples.

Valeurs construites et filtrage

Une extension simple du noyau ML consiste à ajouter des valeurs construites et du filtrage superficiel (le filtrage en profondeur étant plus compliqué).

Pour simplifier la formalisation, nous ignorons les déclarations de types et nous paramétrons le langage par une collection de types concrets prédéfinis. Dans une premier temps nous ne considérons qu’un seul type concret. En fait, nous laisons en exercice le cas de plusieurs types concrets. Le cas de déclarations de types locales est plus compliqué. Par exemple, la définition suivante

                       type τ g = Cof τ_{i} | . . . Cof τ_{n}

revient à ajouter n constructeurs C_{1}, … C_{n} et une primitive F_{g} d’arité n + 1 :

C^{1} ::= C_{1}| … C_{n}  Constructeurs
f^{n+1} ::= F_{g}  Primitive de filtrage

La primitive F_{g} se réduit ainsi :

F_{g} (C_{k} v) v_{1} … v_{k} ⟶ v_{k} v  (δ_{g})

L’environnement de typage contient maintenant les déclarations

\begin{aligned}C_{i} & : ∀ V. τ_{i} → τ g \\ F_{g} & : ∀ V. τ g → (τ_{1} → τ′) → … (τ_{n} → τ′) → τ′ \end{aligned}

Attention ! il est important de se restreindre au cas où l’union des variables libres dans les τ_{i} apparaissent sont aussi libres dans τ.

On pourra ajouter le sucre syntaxique qui consiste à noter

match a withC_{1} (x) ⇒ a_{1} … | C_{n} (x) ⇒ a_{n}

pour

F_{g} a (fun (x) a_{1}) … (fun (x) a_{n})

Il s’agit juste d’une convention de notation, qui ne change rien à la formalisation ; il s’agit simplement de choisir une notation plus commode. En ce sens, le sucre syntaxique est “gratuit”.

Exercice 9 (**) Que se passe-t-il si une variable libre de τ_{i} n’apparaît pas dans τ (donner un exemple) ? Commenter. Est-il possible qu’inversement une variable libre dans τ n’apparaisse dans aucun τ_{i} (donner un exemple) ?

Exercice 10 Montrer que les hypothèses H sont satisfaites.

Exercice 11 (*) Vérifier que le cas des booléens est un cas particulier des types construits

Exercice 12 (***) Vérifier que le cas des paires est aussi un cas particulier d’une généralisation des types construits.

Exercice 13 (*) Formaliser directement le cas des types construits. On utilisera la syntaxe habituelle pour le pattern matching :

match a withC_{1} (x) ⇒ a_{1} … | C_{n} (x) ⇒ a_{n}

Montrer que l’on retrouve la règle de typage habituelle. en utilisant l’ajout de constantes.

Combinateur de point-fixe

On peut ajouter une constante

Y : ∀ α_{1}, α_{2}. ((α_{1} → α_{2}) → α_{1} → α_{2}) → α_{1} → α_{2}

d’arité 2, avec la δ-règle

Y F v ⟶ F (Y F) v

Comme Y est d’arité 2, Y F est une valeur, et l’évaluation du membre droit ci-dessus doit continuer avec la réduction de l’application externe. Il est important que Y soit d’arité deux, pour que Y calcule le point fixe “paresseusement”. Par exemple, si Y était d’arité 1 avec la δ-règle

Y F ⟶ (fun (x) F (Y F) x)

alors l’évaluation de Y F v partirait dans une boucle infinie (nous avons souligné le radical actif) :

\underline{Y F} v ⟶ Y (\underline{Y F}) v ⟶ Y (F (\underline{F v}))v ⟶ …

Exercice 14 (*) Écrire la fonction factorielle à l’aide de Y.

Exercice 15 Vérifier que les hypothèses H1 et H2 sont satisfaites pour l’ajout du combinateur Y.

La constante Y se comporte comme l’expression

fun (F) (fun (f x) F (f f) x) (fun (f x) F (f f) x)

qui n’est cependant pas typable en ML “pur” (il faudrait autoriser les types récursifs).

La construction let rec fx = a_{1} in a_{2} est donc simplement du sucre syntaxique pour let f = Y (fun (f x) a_{1}) in a_{2}.

Exercice 16 Les types concrets peuvent être récursifs, c’est-à-dire, dans une définition :

                       type τ g = Cof τ_{i} | . . . Cof τ_{n}

le constructeur de type g peut apparaître dans les types τ_{i}. En fait, ce constructeur ne peut apparaître qu’avec le même type τ. C’est donc τ g qui peut apparaître dans τ_{i} plutôt que g. Sinon, l’égalité de deux déclarations de types concrets deviendrait indécidables. Donner un exemple de type concret récursifs. Pour écrire le pointy fixe, il suffit d’un type récursif de la forme valeur égal à valeur → valeur. Donner une définition du type concret valeur. Donner une fonction de coercion deplier d’une valeur en une fonction de type valeur → valeur et son inverse replier. Les utiliser pour définir Y sans utiliser la récursion (on cherchera donc à écrire une version typée de l’expression donnée ci-dessus).

Exercice 17 (programmation) Étendre le programme de l’exercice 5 avec les paires, les expressions booléennes et le combinateur de point fixe.

Contraintes de type

On peut également étendre le langage avec des contraintes de types. En effet, on peut voir une expression (a : τ) comme du sucre syntaxique l’application ( : τ) a où ( : τ) est une primitive de type principal ∀ V. τ → τ, et avec la δ-règle (v : τ) ⟶ v.

Exercice 18 Vérifier que les hypothèses sont satisfaites.

Les contraintes de types que nous proposons ici sont locales (les variables sont quantifiés localement). En particulier, deux contraintes dans la même phrase utilisant les même variables de types sont indépendante. On peut aussi choisir une stratégie opposée qui consiste à ne jamais généraliser les variables de type dans les contraintes, et ainsi les partager entre les différentes contraintes.

Conclusion

La sémantique à petits pas est supérieure par presque tous ses aspects à la sémantique à grands pas. Elle est plus simple parce qu’elle s’exprime dans le langage même. Les valeurs sont un sous-ensemble des expressions et non pas des objets extérieurs au langage. La sémantique à petits pas est plus concise. Mais son avantage essentiel est d’être plus précise puisqu’elle permet de décrire simplement des calculs en cours qui ne termineront peut-être pas, et donc de distinguer clairement la divergence des erreurs de calculs sans avoir recours à un artifice.

On lui reproche parfois d’être trop éloignée de la sémantique réelle, implantée dans un compilateur, rendant plus difficile la vérification qu’un compilateur est correct vis à vis de la sémantique. Elle se rapproche en effet beaucoup plus d’un interpréteur naïf qui procéderait par réécriture du code source. En particulier, elle effectue des substitutions “coûteuses” pendant le calcul, alors que la sémantique à grands pas pouvait grâce aux fermetures, modéliser une machine à environnement. Mais n’est-ce pas là le bon niveau d’abstraction entre une sémantique trop près de la machine et la sémantique dénotationnelle trop éloignée de l’évaluation ?

Nous avons vu que la sémantique à réduction se prête très bien à des extensions du langage car elle est modulaire. Nous verrons dans le chapitre suivant qu’elle s’applique également, et de façon simple, aux constructions impératives.

Pour en savoir plus

Sur d’autres approches de la sémantique des langages de programmation, lire [?]. La comparaison entre sémantique à petits pas et la sémantique à grand pas est détaillée dans [?]. Pour les propriétés générales du typage et le typage avec types récursifs, on pourra lire [?]. Le traitement des types concrets est abordé dans [?], [?] et [?].

Solutions des exercices

Exercice 1, page 18

Il y a deux radicaux qui peuvent être réduits dans un ordre arbitraire, on obtient les termes :

let f = fun (y) y in (fun (z) z) f ou (fun (z) z) (fun (y) y)

qui tous deux se réduisent en (fun (y) y). En appel par valeur, seule la seconde réduction est permise, car il n’est pas possible de réduire sous une liaison.

Exercice 2, page 18

Si l’on veut être formel, on peut le montrer très facilement par une récurrence structurelle sur la taille des expressions.

Exercice 3, page 18

Dans le calcul sans constantes, il faut réduire les contextes d’évaluation à

E ::= [] | E a

pour interdire l’évaluation des arguments et autoriser la β-réduction dans toute sa généralité :

(fun (x) a_{1}) a_{2} ⟶^{ϵ} a_{1}[a_{2}/x]  Fun
let x = a_{2} in a_{1} ⟶^{ϵ} a_{1}[a_{2}/x]  Let

Avec des constantes, le plus simple serait de supposer que les constantes acceptent des arguments non évalués, mais c’est cacher la difficulté. Car les constantes doivent forcer le calcul des arguments strictement nécessaires.

Exercice 7, page 25

Pour traiter les paires de façon primitive, il faut d’abord étendre la syntaxe des expressions, sans oublier d’étendre également les valeurs :

a ::= … | (a, a) | fst a | snd a
v ::= … (v, v)

Ensuite il faut étendre la notion de réduction, c’est-à-dire ajouter les contextes d’évaluation suivants :

E ::= … | (E, a) | (v, E)

puis les deux réductions :

fst (v_{1}, v_{2}) ⟶ v_{1} et snd (v_{1}, v_{2}) ⟶ v_{2}

Pour formuler le typage, on définit un nouveau symbol de type ( ∗ ). Nous pouvons tricher en définissant le typage des paires comme celui des constantes, mais sinon, il nous faut écrire les règles

\frac{A ⊢ a_{1} : τ_{1} A ⊢ a_{2} : τ_{2}}{A ⊢ (a_{1}, a_{2}) : τ_{1} ∗ τ_{2}}  \frac{A ⊢ a : τ_{1} ∗ τ_{2}}{A ⊢ fst a : τ_{1}}  \frac{A ⊢ a : τ_{1} ∗ τ_{2}}{A ⊢ snd a : τ_{2}}

Pour être rigoureux, il faudrait refaire toutes les preuves sur le typage, puisque nous avons changé la relation de typage… De même il nous faut a priori refaire toutes les preuves de correction de la sémantique. Nous nous contentons de décrire les cas à ajouter dans les preuves. Dans le lemme 4, page 20 ces cas sont analogues à ceux de l’application. Dans le lemme 6, page 21, ces cas sont triviaux. Dans le théorème 1 (contraction de radical), il faut vérifier les cas suivants :

Cas A est fst (a_{1}, a_{2}) : En reconstruisant la dérivation de typage de a, il est facile de montrer que A ⊢ a_{1} : τ.

Cas A est snd (a_{1}, a_{2}) : est symétrique du précédent.

Enfin dans le théorème 2, page 23, il faut ajouter les cas suivants :

Cas a est fst a_{1} : Comme a_{1} est une valeur, il est facile de montrer à partir de la dérivation de typage de a que A ⊢ a_{1} : τ_{1} ∗ τ_{2}. Les seules valeurs de types produit sont les produits donc a_{1} est de la forme (a_{2}, a_{3}) et a peut être réduit.

Cas a est snd a_{1} : Ce cas est symétrique du précédent.

Cas a est (a_{1}, a_{2}) : a est une valeur.

Les cas que nous avons explicitement traités ci-dessus correspondent exactement à la vérification des deux hypothèses sur les constantes. Mais, si nous voulons être complets, il faut également vérifier d’autres cas, similaires à l’application que nous avons ignorés ci-dessus.

Les arguments ci-dessus ne constituent pas exactement une démonstration, mais plutôt un méta-raisonnement, c’est-à-dire un discours sur comment faire une vraie démonstration. Ce discours nous rend très confiant sur la possibilité d’écrire vraiment la démonstration. Mais, pour être plus formel, il faudrait réécrire toutes les preuves, ou bien, ce qui revient au même, avoir incorporés les paires dès le début du chapitre précédent.

Exercice 8, page 25

Nous ne donnons pas un corrigé complet, mais les idées principales. On définit la traduction [[a]] par récurrence structurelle. Les trois nouvelles constructions se traduisent pas des applications de primitives, les autres sont homomorphes. Pour montrer que la réduction commute, il faut montrer formellement que si a_{1} ⟶ a_{2} alors [[a_{1}]] ⟶ [[a_{2}]], par récurrence structurelle sur a. Plus simple est de remarquer que [[E[a]]] est égal à [[E]][[[a]]]. Il suffit alors de vérifier la propriété précédente pour les radicaux. Les cas intéressants sont les deux nouvelles règles de ML_{1} qui correspondance dans ML_{2} à des δ-règles.

Pour montrer l’équivalence, on rencontre le problème des expressions (a, ) bien formées dans ML_{2}, car ce sont des primitives partiellement appliquées (lire ( , ) a_{1}), alors que la syntaxe les interdit dans ML_{1}. Une solution est de se restreindre dans ML_{2} aux programmes où les primitives ne sont jamais partiellement appliquées (propriété heureusement conservée par réduction). On peut alors montrer que la traduction composée avec la traduction inverse est l’identité. Nous avons mis en bijection les expressions des deux langages et leur relation de réduction. Pour éliminer la restriction, on pourrait définir dans ML_{2} une transformation qui remplace les primitives ( , ) par fun (x y) (x, y) et montrer qu’un programme et son transformé sont observationnellement équivalents, c’est-à-dire que si placés dans le même contexte l’un se réduit en une valeur non fonctionnelle alors le second se réduit sur la même valeur. Ceci est plus difficile à formaliser.

Exercice 9, page 26

Sinon, on pourrait définir type g = C of α. et écrire la fonction fun (x) (F_{g} (C x)) qui se comporte comme l’identité mais à le type τ → τ′ quelque soient τ et τ′. Pour des instances bien choisies de τ et τ′ cela contredit la préservation des types.

En fait la définition ci-dessus est possible, mais il faut alors s’interdire de généraliser la variable α dans A_{0}.

Par contre, il est tout à fait possible que τ contiennent des variables superflu. Pour s’en assurer, il suffit de vérifier que cela se ramène au cas général en ajoutant un constructeur suplémentaire C_{n+1} of α qui rend cette variable de type non superflue et ne jamais utiliser le nouveau constructeur C_{n+1} !

Exercice 11, page 26

On peut définir type bool = true | false et choisir la primitive if then else égale à

F_{bool}.

L’utilisateur doit cependant écrire if then else a_{1} (fun () a_{2}) (fun () a_{3}) au lieu

de if a_{1} then a_{2} else a_{3}.

En fait, on peut ajouter du sucre syntaxique, c’est-à-dire écrire if a_{1} then a_{2} else a_{3} pour signifier if then else a_{1} (fun () a_{2}) (fun () a_{3}).

Exercice 12, page 26

Il faut simplement généraliser les types construits à des constructeurs d’arité multiples de la forme :

                       type τ̄ g = Cof τ̄_{i} | . . . Cof τ̄_{n}

La généralisation est facile, et laissée en exercice. On peut alors définir :

type (α_{1}, α_{2}) ( ∗ ) = ( , ) of (α_{1}, α_{2})

fst=^{def} fun (z) (F_{∗} z (fun (x) fun (y) x)) snd=^{def} fun (z) (F_{∗} z (fun (x) fun (y) y))

Exercice 13, page 26

On étend le langage avec les expressions ci-dessus, et les constructions C_{i} a. Les règles de typages sont

(C_{i}) ; \frac{A ⊢ a : τ_{i}}{A ⊢ C_{i} a : τ g} (Match)

\frac{A ⊢ a : τ g A ⊕ (x : τ_{i}) ⊢ a_{i} : τ′}{match a withC_{1} (x) ⇒ a_{1} … | C_{n} (x) ⇒ a_{n} : τ′}

La réduction est alors une règle :

(matchC_{k} (v) withC_{1} (x) ⇒ a_{1} … | C_{n} (x) ⇒ a_{n})⟶ (fun (x) a_{k}) v

Il faut montrer bien sûr que les preuves s’étendent aux nouvelles constructions, ce qui revient à montrer les hypothèses H_{1} et H_{2} plus d’autres cas redondants (car similaires à l’application). d’une autre façon.

Exercice 14, page 27

let Fact fact x = if x = 0 then 1 else x * fact (x−1)
let fact x = Y Fact x