λ-calcul par valeur et étiquettes

Les langages fonctionnels tels que Lisp, Objective Caml, SML/NJ ou Haskell [20, 28, 40, 34] sont fondés sur le λ-calcul. Si plusieurs radicaux peuvent coexister dans un terme du λ-calcul, au moment d’évaluer ce terme, par exemple dans un interpréteur, on peut se demander quel radical réduire en premier. En présence d’effets de bord, l’ordre d’évaluation est critique puisque le résultat obtenu peut dépendre de cet ordre. Plus simplement, dans le λ-calcul pur, si l’abstraction d’un radical R = (λx.M)N ne contient pas d’occurrences de x, réduire le terme N peut sembler inutile, puisque ce terme disparaitra de toute façon quand R sera contracté. La réduction de N pourrait même boucler alors que R est normalisable. En revanche, si le corps M de l’abstraction contient plusieurs occurrences de x, contracter R dupliquerait les réductions a faire dans N. Faire ces réductions avant la contraction de R revient `a les factoriser. Dans la mesure où on s’attend `a ce que l’argument d’une fonction soit utilisé, la stratégie d’évaluation adoptée par Objective Caml et SML/NJ est en appel par valeur. Les arguments des applications sont réduits jusqu’`a obtenir des valeurs. Puis l’application est réduite.

Au moment de l’étude de la propriété de non-interférence, exposée dans le chapitre 5, nous avons souhaité étudier cette propriété au sein d’un λ-calcul étendu par des traits impératifs permettant de manipuler la mémoire. La présence d’effets de bord nous a poussé `a définir un ordre d’évaluation. Nous avons choisi, comme pour Objective Caml et SML/NJ, une évaluation en appel par valeur, c’est-`a-dire une évaluation dans laquelle les arguments des βradicaux sont des valeurs. Ce choix a motivé l’étude dans le λ-calcul de ces réductions particulières où les radicaux contractés sont de la forme (λx.M)V . Dans la section 2.1, nous introduisons les règles de la réduction par valeur →v. Ces règles s’appliquent aux termes du λ-calcul. Par abus, nous appellerons λ-calcul par valeur le langage constitué des termes du λ-calcul et muni de la réduction par valeur. Nous montrons que la réduction par valeur vérifie les mêmes propriétés essentielles que la réduction → classique. On obtient donc une propriété de confluence. On montre également que le λ-calcul par valeur vérifie le théorème des développements finis. En utilisant une définition de la réduction standard spécifique au λ-calcul par valeur (différente de celle du λ-calcul), on prouve que le théorème de standardisation est vérifié. Les propriétés de monotonie et de stabilité du λ-calcul sont également conservées. On constate dans la section 2.2 que les étiquettes du λ-calcul ne vérifient plus, en utilisant la réduction par valeur, la propriété de stabilité énoncée dans le résultat 1.15. On introduit de nouvelles étiquettes spécifiques au λ-calcul par valeur. Ce calcul étiqueté est confluent. En utilisant une démonstration intuitive, fondée sur une notion d’imbrication des radicaux qui tient compte des imbrications futures, on montre le théorème des développements finis. Le λ-calcul par valeur étiqueté conserve la propriété de standardisation. Et les nouvelles étiquettes permettent d’obtenir la propriété de stabilité correspondant au résultat 1.15..

Le λ-calcul par valeur

Par abus, on appelle λ-calcul par valeur, le calcul dont les termes sont les termes du λ-calcul et dont les règles de réduction sont définies ci-dessous. (βv) (λx.X)V →v X{x\V } (νv) X →v X′ XY →v X′Y (µv) Y →v Y ′ XY →v XY ′ (ξv) X →v X′ λx.X →v λx.X′ La βv-réduction est une β-réduction où l’argument du β-radical est une valeur. Dans le cadre présent où les valeurs sont les abstractions, il peut sembler inutile d’utiliser cette notion. Cependant, cette dernière présente un avantage en terme de modularité si de nouveaux termes tels que les entiers sont ajoutés `a la syntaxe du langage. Ces entiers, considérés comme des valeurs, ne nécessiteraient pas de changement des règles de réduction. Les règles de contexte sont simplement adaptées. Par conséquent, si les réductions sont vues comme des relations, on a →v⊆→. Autrement énoncé, si X →v Y , alors on a X → Y . La notion de radical est modifiée en conséquence : les βv-radicaux sont les sous-termes de la forme (λx.X)V . De même que dans le λ-calcul, on a X →v X′ si et seulement s’il existe un contexte C tel que X = C[(λx.Y )V ] et X′ = C[Y {x\V }]. Pour définir la notion de βv-résidu, on s’appuie sur la définition de β-résidu. On commence par observer que la notion de βv-radical vérifie la propriété fondamentale suivante. Lemme 2.1 Si R est un βv-radical et N est un terme, alors R{x\N} est un βv-radical. Preuve : Ce résultat tient au fait que l’ensemble des valeurs est stable par substitution.  Ce lemme énonce le fait que l’ensemble des βv-radicaux est stable par substitution. A fortiori, cet ensemble est stable par substitution par une valeur. Cela permet d’obtenir le résultat suivant. Lemme 2.2 Si X → X′ , les β-résidus dans X′ des βv-radicaux de X sont des βv-radicaux. Preuve : Elémentaire, par inspection des cas.  Les β-résidus d’un βv-radical sont des βv-radicaux. Cette propriété est vraie pour une réduction → et, `a plus forte raison, pour une réduction →v. On peut donc définir la notion de βv-résidu de la façon suivante, en utilisant la notion de β-résidu : si X →v X′ , un βv-radical r ′ de X′ est βv-résidu d’un βv-radical r de X si et seulement si r ′ est β-résidu de r. On illustre cette définition avec la réduction R = (λx.Iλz.x)(yy) → Iλz.yy. Après la contraction de R, le β-résidu du βv-radical R′ = Iλz.x est le βv-radical Iλz.yy : ce dernier est le βv-résidu de R′ . On examine un deuxième exemple qui met en lumière une différence fondamentale entre le λ-calcul et le λ-calcul par valeur. Le terme R = I1(I2 I3) (où I1 = I2 = I3 = λx.x) contient deux β-radicaux : R et I2I3. Seul ce dernier est un βv-radical. Le terme R se réduit par la réduction R →v I1I3 = R′ . Alors que R′ est le β-résidu du β-radical R, le βv-radical R′ n’est pas un βv-résidu d’un βv-radical de R : le βv-radical R′ est donc créé par la contraction de R. La réduction en appel par valeur entraine donc des changements dans la relation de création entre les radicaux par rapport au λ-calcul : un nouveau cas de création apparait. En plus de la création “par le haut” et “par le bas”, un βv-radical peut être créé “par la droite” lorsque l’argument d’une application devient une valeur. Ceci constitue la particularité fondamentale du λ-calcul par valeur. Nous verrons que cette dernière a un impact dans cette section sur la définition de réduction standard et, dans la section suivante, sur la propriété de stabilité. Dans la suite de cette section, on montre que le λ-calcul par valeur est localement confluent et confluent. On montre aussi que le théorème des développements finis est conservé et que, pour une définition spécifique de réduction standard, le théorème de standardisation est vérifié. Les propriétés de monotonie et de stabilité sont également conservé.