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.

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:

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:

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 boolé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] ρ κ =_def κ (ρ (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] ρ κ′ pour une continuation κ′ à trouver. Cette continuation κ′ est une fonction qui prend la valeur f de u, et va ensuite calculer v. Donc κ′ doit être de la forme (f ↦ [v] ρ′ κ″) pour un environnement ρ′ et une continuation κ″ à trouver. Mais v s’évalue dans le même environnement que uv, donc ρ′=ρ. D’autre part, κ″ 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é:

Cette formule peut avoir l’air illisible, mais voici un truc pour déchiffrer ce genre de notations intuitivement: [u] ρ (f ↦ … 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:

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é, la continuation devra juste retourner cette valeur: la continuation cherchée est l’identité id. En somme:

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] ρ κ =def κ (ρ (x))        [uv] ρ κ =def       [u] ρ  ⎛ ⎜ ⎝ f ↦ [v] ρ  ⎛ ⎜ ⎝ d ↦ ⎧ ⎨ ⎩           κ (f (d)) si f est une fonction            ⊥ sinon ⎞ ⎟ ⎠ ⎞ ⎟ ⎠       [λ x· u] ρ κ =def κ (d ↦ [u] (ρ[x:=d]) id)

Figure 5: Une sémantique de l’appel par valeur en style de passage de continuations

---

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

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 (erreur)
      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);
  }

Comme beaucoup de constructions en C, celle-ci manque de l’élégance des constructions similaires de langages fonctionnels, et la plus proche est une construction, appelé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:

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 continuation κ′, 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 comportement attendu:

Mais en fait, non, le comportement des continuations n’est pas le comportement 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:

alors que:

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 ↦ d)) signifie que si κ est la suite du programme, au lieu de retourner simplement la fonction d ↦ d, on va retourner d ↦ d, effectuer la suite du programme, et une fois que le programme aura terminé et retourné une valeur d′, on réexécutera la même suite κ du programme cette fois-ci sur la valeur d′ !

Le problème est dans la façon dont nous avons défini la sémantique de l’abstraction 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 κ′, alors u doit être évalué dans la pile κ′. Il est donc nécessaire de modifier la définition de sorte qu’elle prenne en paramètre la pile κ′ de l’appelant en plus de la valeur d de l’argument x:

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:

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

---

[x] ρ κ =def κ (ρ (x))        [uv] ρ κ =def [u] ρ  ⎛ ⎜ ⎝ f ↦ [v] ρ  ⎛ ⎜ ⎝ d ↦ ⎧ ⎨ ⎩           f (κ, d) si f est une fonction binaire            ⊥ sinon ⎞ ⎟ ⎠ ⎞ ⎟ ⎠       [λ x · u] ρ κ =def       κ ((κ′, d) ↦ [u] (ρ[x:=d]) κ′)        [callcc k in u] ρ κ =def       [u] (ρ [k:=κ]) κ        [throw k v] ρ κ =def [k] ρ (κ′ ↦ [v] ρ κ′)

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

---

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:

En fait, il est traditionnel lorsqu’on étudie les opérateurs de capture de continuation 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′ =_def throw k =_def λ x · throw k x: la valeur de k′ est la seule chose que call/cc a besoin de stocker. On définit donc (définitivement):

où (_, d′) ↦ κ′ (d′) est la fonction qui prend une continuation κ″, une valeur d′ et retourne κ′ (d′) après avoir jeté κ″.

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 ? Intuitivement, 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′ en écrivant C (λ k′ · …), et alors le calcul consistant à calculer t avec comme continuation la fonction qui prend la valeur f de t, l’applique à v et continue le calcul (par k′) est donc t [k:=λ f · k′ (f v)] — ceci du moins tant que v est une P-valeur. Ceci suggère que C (λ k · t) v = C (λ k′ · t [k:=λ f · k′ (f v)], au moins si v est une P-valeur. Plus généralement, posons u =_def λ k · t, et comparons les deux quantités C u v et C (λ k′ · u (λ f · k′ (f v))):

Tandis que:

On a donc démontré:

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:

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

Exercice 41 ()   Montrer que la règle ( C_R) 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 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:

à 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 langage 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 construction !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 argument 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:

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 valeur 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:

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 Mem.)

---

[x] ρ σ κ =def κ (σ, ρ (x))        [uv] ρ σ κ =def [u] ρ σ ⎛ ⎜ ⎝ (σ′, f) ↦ [v] ρ σ′ ⎛ ⎜ ⎝ (σ″, d) ↦ ⎧ ⎨ ⎩               f (κ, σ″, d) si f est une fonction                ⊥ sinon ⎞ ⎟ ⎠ ⎞ ⎟ ⎠       [λ x · u] ρ σ κ =def       κ (σ, (κ′, σ′, d) ↦ [u] (ρ[x:=d]) σ′ κ′)        [!u] ρ σ κ =def [u] ρ σ ⎛ ⎜ ⎝ (σ′, l) ↦ ⎧ ⎨ ⎩             κ (σ′, σ′ (l))             si l est dans le domaine de σ′              ⊥ sinon ⎞ ⎟ ⎠       [u:=v] ρ σ κ =def       [u] ρ σ  ⎛ ⎜ ⎝ (σ′, l) ↦ [v] ρ σ′  ⎛ ⎜ ⎝ (σ″, d) ↦ ⎧ ⎨ ⎩               κ (σ″[l:=d], d) si l∈ L                ⊥ sinon ⎞ ⎟ ⎠ ⎞ ⎟ ⎠       [ref u] ρ σ κ =def       [u] ρ σ ((σ′, d) ↦ κ (σ′[l:=d], l))      (l hors du domaine de σ′)        [u;v] ρ σ κ =def       [u] ρ σ ((σ′, _) ↦ [v] ρ σ′ κ)

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

---

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

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