Le λ-calcul faible et étiquettes

λ-calcul faible et étiquettes

Jusqu’`a présent, nous avons considéré des calculs dits forts, c’est-`a-dire qui autorisent la règle de contexte ξ : (ξ) M → N λx.M → λx.N Par contraste, un calcul faible n’autorise pas cette règle ; les contractions internes aux abstractions ne sont pas permises. En cela, le calcul faible est plus proche des implémentations des langages fonctionnels [28, 40]. Pourtant, si le calcul fort a fait l’objet de nombreux travaux, le calcul faible n’a pas autant été étudié. La notion de partage dans le λ-calcul fort a notamment été étudiée en profondeur dans les multiples travaux d’Abadi, Asperti, Coppola, Gonthier, Guerrini, Lamping, Lawall, Lévy, Mairson, Martini [5, 6, 18, 25, 27, 29]. Pour exprimer le partage dans le calcul fort, les termes sont représentés par des graphes dont les sous-contextes peuvent ˆetre partagés. Par exemple, dans le terme (λx.xa(xb))(λy.Iy) o`u I = λx.x, il est nécessaire de partager le radical Iy indépendamment de la valeur de y. Ainsi, on doit partager le sous-contexte I[ ].

Après la réduction des radicaux externes, on obtient (λy.Iy)a((λy.Iy)b) puis Ia((λy.Iy)b) ou le sou contexte (partagé) I[ ] est instancié avec deux sous-termes différents : a et y. En utilisant les notations de Lamping, le partage d’un sous-contexte se fait par un nœud fan-in qui multiplexe des aretes provenant des termes qui l’utilisent. Les nœuds fan-out permettent de remplir les vides de ces sous-contextes par une opération de démultiplexage. Les aretes sortant du nœud fan-out pointent sur les termes correspondant `a ces trous. Lamping a élaboré un calcul optimal opérant sur ces graphes. Les réductions de son calcul obéissent `a la sémantique des contextes définie par Gonthier, Abadi et Lévy [18]. Dans le calcul faible, les contractions ne peuvent se produire sous une abstraction. Ainsi, dans le précédent exemple, le sous-terme Iy de (λx.xa(xb))(λy.Iy) ne peut ˆetre réduit puisqu’il est contenu par l’abstraction λy.Iy. Plus généralement, un sous-terme ne pourra ˆetre réduit que s’il ne contient plus de variable liée par un radical externe. Par conséquent, les sous-contextes ne sont plus nécessaires pour partager les sous-termes. On peut représenter les termes avec partage simplement avec des graphes acycliques orientés, au lieu de la structure cyclique utilisée par Lamping. Dans [43], Wadsworth décrit deux algorithmes pour la réduction de termes dans le λ-calcul faible avec partage.

Dans le premier algorithme, les arguments des radicaux contractés sont partagés. Cependant, si une abstraction partagée est impliquée dans un radical R, cette abstraction est dupliquée avant de contracter R. Pour son deuxième algorithme, Wadsworth remarque qu’il n’est pas nécessaire de dupliquer l’abstraction en entier : les sous-termes qui ne contiennent pas la variable liée peuvent rester partagés. Des duplications inutiles sont donc évitées. La figure 3.1 illustre ces deux algorithmes pour la réduction de M = (λx.(xy)(xz))λu.Iu. Le premier radical contracté est R1 = M. Dans le terme obtenu par les deux algorithmes, l’argument λu.(λv.v)u du 69 λ-calcul faible et étiquettes 70 λ-calcul faible et étiquettes Fig. 3.1 – Réductions de M = (λx.(xy)(xz))λu.Iu par les deux algorithmes de Wadsworth radical contracté est partagé. Le deuxième radical contracté est R2 = (λu.(λv.v)u)y. L’abstraction de ce radical est partagée. Avec le premier algorithme, cette dernière est entièrement départagée avant la réduction.

Avec le deuxième algorithme, seul le contexte λu.([ ])u (le contexte minimal qui contient toutes les variables liées par l’abstraction) est départagé. Cet algorithme plus fin permet de maintenir le partage du sous-terme λv.v après la réduction, au contraire du premier algorithme. En s’inspirant des conclusions de Wadsworth, Shivers et Wand [38] proposent une implémentation réaliste qui représente les termes sous forme de graphes. Dans ces graphes, le nœud correspondant `a une abstraction λx.M est non seulement relié au sous-terme correspondant `a M mais aussi aux occurrences de x dans M. Les nœuds des termes sont reliés entre eux par des arˆetes dans les deux sens. Cette représentation facilite la duplication des sous-termes : cette duplication s’effectue en partant des occurrences de la variable liée vers le lieur. Ceci permet d’offrir une implémentation efficace du deuxième algorithme de Wadsworth.

Le λ-calcul faible

Avant de s’intéresser `a la notion de partage, nous nous penchons tout d’abord sur les propriétés élémentaires du λ-calcul faible. Si on se contente de soustraire au λ-calcul fort la règle de contexte (ξ), on obtient un calcul qui n’est pas confluent. Pour s’en convaincre, on observe les réductions du terme R = (λx.λy.x)(Iu) qui sont illustrées sur la figure 3.2. Le terme R se réduit vers les termes M1 et M2. Ces derniers sont `a la fois distincts et en formes normales. Cette non-confluence s’explique par le fait que le sous-terme Iu qui est initialement un radical de R, est, après contraction de R, gelé dans M1 sous l’abstraction λy.Iu. Le sous-terme Iu de M1 n’est plus un radical. Intuitivement, ce sous-terme Iu de M1 pourrait pourtant etre considéré comme un radical puisqu’il ne dépend pas véritablement de l’abstraction qui le contient, dans la mesure ou il ne contient pas la variable y liée par ce radical. En effet, le sous-terme Iu a été injecté sous l’abstraction par une substitution. Cette intuition est exploitée par Lévy et Maranget. Ils proposent dans [30] une variante du λ-calcul faible qui est inspirée par les travaux de C¸ agman et Hindley pour la Logique Combinatoire [11]. Dans cette variante, une nouvelle règle de contexte est ajoutée. (σ) N → N′ M linéaire en x M{x\N} → M{x\N′} Dans cette règle, la condition “M linéaire en x” signifie qu’il existe une unique occurrence de x dans M.

L’usage de la substitution reflète le fait que N ne contient pas de variables liées par une abstraction de M. Ceci signifie que N ne dépend ni des abstractions de M, ni de leur argument potentiel. Ces conditions rejoignent l’intuition issue de l’exemple mentionné plus haut. Par ailleurs, la condition de linéarité évite de considérer des pas de réduction parallèles. Dans cette partie, au lieu de la règle (σ), on utilise une approche voisine. Les règles de notre variante du λ-calcul faible sont les suivantes. (βw) R = (λx.M)N R−→w M{x\N} (νw) M R−→w M′ MN R−→w M′N (ξ ′ w) M R−→w M′ x 6∈ FV(R) λx.M R−→w λx.M′ (µw) N R−→w N′ MN R−→w MN′ La règle de base (βw) est conservée du λ-calcul fort. On note simplement que la réduction R−→w est annotée avec le radical contracté. En cas d’absence d’ambigüité, on omettra cette annotation. Aux règles classiques (µw) et (νw), on ajoute une nouvelle règle (ξ ′ w). Par définition de cette règle, le corps d’une abstraction peut etre réduit seulement si le radical contracté ne contient pas la 72 λ-calcul faible et étiquettes variable liée par l’abstraction. Ceci montre la correction de la notation R−→w puisque l’α-conversion ne change pas le radical R qui annote la réduction. Au lieu d’utiliser la substitution pour exprimer l’absence de variable liée dans un sous-terme d’une abstraction, cette règle (ξ ′ w) exprime plus directement cette contrainte. De l`a, les radicaux de cette variante du λ-calcul faible sont donc les radicaux (λx.M)N du λ-calcul fort qui ne contiennent pas de variable liée. Ces radicaux vérifient la propriété suivante. Lemme 3.1 On suppose M S−→ M′ o`u S est un βw-radical. On a M S−→w M′ et les β-résidus d’un βw-radical R sont des βw-radicaux de M′ . Preuve : Comme R est un βw-radical de M, il ne contient pas de variable liée par une abstraction externe. Par conséquent, ses β-résidus sont des β-radicaux qui vérifient la même propriété : ce sont donc des βw-radicaux. 

Cette propriété permet de donner la définition suivante de βw-résidu : si M S−→w M′ , les βw-résidus d’un βw-radical R de M dans M′ sont les β-résidus de R dans M′ . Comparativement au λ-calcul fort, on observe qu’il existe une nouvelle façon de créer des radicaux dans le λ-calcul faible en plus des créations par le haut et par le bas. Après avoir contracté M = (λx.Ix)y, nous obtenons un radical Iy qui n’est pas un résidu d’un radical de M et qui n’est pas un radical créé au sens du λ-calcul fort. En réalité, si le sous-terme Ix est un radical pour le calcul fort, il n’est pas un radical pour le calcul faible : il est gelé dans M par l’occurrence de x. La contraction de l’abstraction contenant Ix crée le radical Iy en le dégelant. L’introduction de la règle (ξ ′ w) permet d’obtenir un calcul localement confluent. Comme dans le cas du calcul fort, la preuve de confluence locale s’appuie essentiellement sur les propriétés suivantes qui mettent en jeu la substitution et la réduction.