Machine de Krivine

En informatique théorique, la machine de Krivine est une machine abstraite au même titre que les machines de Turing ou que la machine SECD avec laquelle elle partage un certain nombre de spécificités. Elle explique comment calculer une fonction récursive. Plus précisément, elle sert à définir rigoureusement la réduction en forme normale de tête d'un terme du lambda-calcul en utilisant la réduction par appel par nom[1]. À ce titre, elle explique en détail comment se passe une certaine forme de réduction et sert de support théorique à la sémantique opérationnelle des langages de programmation fonctionnelle.

Une vue imagée d'une machine de Krivine

D'autre part, elle implémente l'appel par nom, parce qu'elle évalue le corps d'un β-redex avant d'en évaluer le paramètre, autrement dit dans une expression (λ x. t) u elle évalue d'abord λ x. t avant d'évaluer u. En programmation fonctionnelle cela voudrait dire que pour évaluer une fonction appliquée à un paramètre, on évalue d'abord la partie fonction avant d'évaluer le paramètre.

La machine de Krivine a été inventée par le logicien français Jean-Louis Krivine au début des années 1980.

Appel par nom et réduction en forme normale de tête

La machine abstraite de Krivine est sous-tendue par deux concepts relatifs au lambda-calcul, à savoir la réduction en forme normale de tête et l'appel par nom. D'autre part, elle s'appuie sur une représentation des lambda-termes avec des indices de de Bruijn[2].

Réduction en forme normale de tête

Un rédex du lambda-calcul (on dit aussi β-rédex) est un terme du lambda-calcul de la forme (λ x. t) u. Si un terme a la forme (λ x. t) u $_{1}$ ... u $_{n}$ , on dit que c'est un rédex de tête. Une forme normale de tête est un terme du lambda-calcul qui n'a pas la forme d'un rédex de tête[3]. Une réduction de tête est une chaîne (non vide) de contractions d'un terme qui contracte seulement des rédex de tête. Une réduction en forme normale de tête d'un terme t (qui est supposé ne pas être en forme normale de tête) est une réduction de tête qui part du terme t et aboutit à une forme normale de tête. D'un point de vue abstrait, la réduction en forme normale de tête est la façon dont calcule un programme quand il évalue un sous-programme récursif ; il est donc important de bien comprendre comment une telle réduction peut-être mise en œuvre et décrite ; l'un des objectifs de la machine de Krivine est de proposer un procédé pour réduire en forme normale de tête et de décrire ce procédé formellement. De la même manière que Turing a utilisé une machine abstraite pour définir formellement la notion d'algorithme, Krivine a utilisé une machine abstraite pour définir formellement la réduction en forme normale de tête.

Machine abstraite, la machine de Krivine utilise une représentation des termes du lambda-calcul, moins lisibles pour l'humain, mais plus adaptée à une manipulation par une machine, à savoir la notation avec des indices de de Bruijn. Rappelons que dans cette notation chaque variable liée est remplacée par un entier qui est le nombre de λ que l'on croise pour atteindre le λ qui lie cette variable.

Un exemple

Le terme ((λ 0) (λ 0)) (λ 0) (qui correspond, si l'on utilise des variables explicites, au terme (λx.x) (λy.y) (λz.z)) n'est pas en forme normale de tête parce que (λ 0) (λ 0) se contracte en (λ 0) donnant lieu au rédex de tête (λ 0) (λ 0) qui lui-même se contracte en (λ 0) qui est donc la forme normale de tête de ((λ 0) (λ 0)) (λ 0). Autrement dit la contraction en forme normale de tête est :

((λ 0) (λ 0)) (λ 0) ➝ (λ 0) (λ 0) ➝ λ 0,

qui correspond à :

(λx.x) (λy.y) (λz.z) ➝ (λy.y) (λz.z) ➝ λz.z.

Nous verrons plus loin comment la machine de Krivine réduit le terme ((λ 0) (λ 0)) (λ 0).

Appel par nom

Pour implémenter la réduction de tête d'un terme u v qui est une application, mais qui n'est pas un rédex, il faut réduire le corps u pour faire apparaître une abstraction et ainsi constituer un rédex avec v. Quand un rédex apparaît on le réduit. Le fait de réduire toujours d'abord le corps d'une application s'appelle de l'appel par nom[4]. La machine de Krivine met en œuvre l'appel par nom du lambda-calcul.

Description

La présentation de la machine de Krivine que nous donnons ici s'appuie sur la notation des termes du lambda-calcul par indices de de Bruijn et suppose que les termes dont elle calcule la forme normale de tête sont clos. Son fonctionnement consiste à modifier l'état courant jusqu'à ce qu'elle ne puisse plus le faire, auquel cas elle obtient une forme normale qui représente le résultat du calcul ou bien elle aboutit à une erreur, ce qui signifie que le terme dont elle est partie est incorrect. Elle peut aussi entrer dans une suite infinie de transitions, ce qui signifie que le terme qu'elle tente de réduire n'a pas de forme normale de tête et correspond à un calcul qui ne se termine pas.

Il a été démontré que la machine de Krivine implémente correctement la réduction en forme normale de tête du lambda-calcul, par appel par nom. De plus, il est à noter que la machine de Krivine est déterministe, car à chaque motif de l'état correspond au plus une transition de la machine.

L'état

L'état est formé de trois composants:

un terme,
une pile,
un environnement.

Le terme est un λ-terme avec indice de Bruijn. La pile et l'environnement appartiennent à la même structure de données récursive, à savoir qu'un environnement non vide est défini à partir d'environnements. Plus précisément, un environnement de même qu'une pile est une liste de couples <terme, environnement>, que l'on appelle une clôture. Dans ce qui suit, l'insertion en tête d'une liste ℓ (pile ou environnement) d'un élément a sera notée a:ℓ, tandis que la liste vide sera notée □. La pile est l'endroit où l'on stocke les clôtures qu'il reste à évaluer, tandis que l'environnement est l'association entre les indices et les clôtures à un moment donné de l'évaluation. Pour sa part, le premier élément de l'environnement correspond à la clôture associée à l'indice 0, le deuxième élément correspond à la clôture associée à l'indice 1 etc. Si l'on doit évaluer un indice, c'est là que l'on va chercher le couple <terme, environnement>, c'est-à-dire la clôture, qui donne le terme à évaluer et l'environnement dans lequel on doit évaluer ce terme[5]. Ces explications intuitives doivent permettre de comprendre les règles de fonctionnement de la machine. Si l'on note t un terme, p une pile et e un environnement, l'état correspondant à ces trois entités sera noté t, p, e. Les règles vont expliquer comment la machine transforme un état en un autre état en repérant des motifs parmi les états.

L' état initial vise à évaluer un terme t, c'est l'état t,□,□. C'est donc l'état où le terme est t et la pile ainsi que l'environnement sont vides. L'état final (en l'absence d'erreur) est de la forme λ t,□,e, autrement dit le terme résultat est une abstraction et son environnement avec une pile vide.

Les transitions

La machine de Krivine a quatre transitions : App, Abs, Zero, Succ.

Transitions de la machine de Krivine[6]
Nom	Avant	Après
App	t u, p, e	t, <u,e>:p, e
Abs	λ t, <u,e'>:p, e	t, p, <u,e'>:e
Zero	0, p, <t, e'>:e	t, p, e'
Succ	n+1, p, <t,e'>:e	n, p, e

La transition App enlève le paramètre d'une application et le met sur la pile pour une évaluation ultérieure. La transition Abs enlève le λ du terme et déplace la clôture du sommet de la pile vers l'environnement. Cette clôture correspondra à l'indice de de Bruijn 0 dans le nouvel environnement. La transition Zero prend la première clôture de l'environnement et récupère le terme qui devient le terme courant et l'environnement qui devient l'environnement courant. La transition Succ enlève le premier item de la liste environnement et en même temps décroît la valeur de l'indice.

Des exemples

Évaluons d'abord le terme (λ 0 0) (λ 0) qui correspond au terme (λ x. x x) (λ x. x)[7]. Nous commençons donc par l'état (λ 0 0) (λ 0), □, □.

Évaluation du terme *(λ 0 0) (λ 0)*
(λ 0 0) (λ 0), □, □
λ 0 0, [<λ 0, □>], □
0 0 , □, [<λ 0, □>]
0, [<0, <λ 0, □>>], [<λ 0, □>]
λ 0, [<0, <λ 0, □>>], □
0, □, [<0, <λ 0, □>>]
0, □, [<λ 0, □>]
λ 0, □, □

On en conclut que la forme normale de tête du terme (λ 0 0) (λ 0) est λ 0, ce qui, traduit avec des variables, donne: la forme normale de tête du terme (λ x. x x) (λ x. x) est λ x. x.

Évaluons maintenant le terme ((λ 0) (λ 0)) (λ 0)

Évaluation de *((λ 0) (λ 0)) (λ 0)*
((λ 0) (λ 0)) (λ 0), □, □
(λ 0) (λ 0), [<(λ 0), □>], □
(λ 0), [<(λ 0), □>,<(λ 0), □>], □
0, [<(λ 0), □>], [<(λ 0), □>]
λ 0, [<(λ 0), □>], □
0, □, [<(λ 0), □>]
(λ 0), □, □

ce qui confirme le fait affirmé plus haut que le forme normale de tête du terme ((λ 0) (λ 0)) (λ 0) est (λ 0).

Discussion

La présentation qui est donnée ici est celle de Pierre-Louis Curien[8] à la nuance près que ce qu'il appelle code, term, stack est ce que nous appelons terme, environnement, pile respectivement. La machine décrite par Krivine dans son article de Higher-Order and Symbolic Computation est une machine paresseuse qui diffère de sa machine d'origine et qui implémente l'appel par nécessité (voir aussi l'article de Frédéric Lang cité).

Une machine de Krivine avec noms

Machine à environment
Nom	Avant	Après
Fetch	$x[e],s$	$e(x),s$
App	$(M~N)[e],s$	$M[e],N[e]:s$
Abs	$(\lambda x.M)[e],c:s$	$M[e[c/x]],s$

Une présentation compacte

Il existe une présentation de la machine de Krivine[9] où l'on se limite à deux règles et où on n'utilise pas les indices de de Bruijn. Un état est décrit par une paire $t\star \pi$ , où $t$ est un terme et où $\pi$ est une pile de termes. Empiler $u$ sur $\pi$ s'écrit $u::\pi$ . Les deux règles sont :

Transitions de la machine compacte
Nom	Avant	Après
Push	$t~s~\star ~\pi$	$t~\star ~s::\pi$
Grab	$\lambda x.t~\star ~s::\pi$	$t[x:=s]~\star ~\pi$

Alternatives

Cheminer avec l'appel par nom au lieu de l'appel par valeur dans l'article de John Reynolds "Definitional Interpreters" mène à la machine de Krivine, qui correspond donc fonctionnellement à un évaluateur méta-circulaire avec appel par nom[10] - [11] - [12] - [13] - [14].

Aussi, la machine de Krivine correspond syntaxiquement au $\lambda {\widehat {\rho }}$ calcul -- une version du $\lambda {\widehat {\rho }}$ calcul avec substitutions explicites de Pierre-Louis Curien qui est close sous la réduction -- avec une stratégie d'ordre normal[15] - [16] - [17]. Si le $\lambda {\widehat {\rho }}$ calcul inclut la $\beta$ réduction généralisée (c'est à dire que le $\beta$ redex emboité $(\lambda x_{1}.\lambda x_{2}.e_{0})\;e_{1}\;e_{2}$ est contracté en un pas au lieu de deux, alors la machine de Krivine qui lui correspond syntaxiquement coincide avec le "brouillon" de Jean-Louis Krivine[16]. (Et si la stratégie de réduction est l'appel par valeur de droite à gauche et inclut la $\beta$ réduction généralisée, alors la machine qui lui correspond syntaxiquement est la "ZINC Abstract Machine" de Xavier Leroy, qui sous-tend OCaml.)[18] - [16]

Notes et références

L'appel par nom est une méthode d'évaluation des fonctions récursives, on l'oppose souvent à l'appel par valeur ou à l'appel par nécessité ou à l'évaluation paresseuse.
Le lecteur est supposé connaître le lambda-calcul, en particulier les indices de de Bruijn
Si on a seulement affaire à des termes clos il s'agit d'une abstraction, autrement dit un terme de la forme λ x. t.
Cette terminologie un peu vieillotte, mais toujours d'actualité, réfère à des concepts des années 1960 et peut difficilement être justifiée en 2015.
En utilisant le concept de clôture, on peut remplacer le triplet <terme, pile, environnement> qui définit l'état, par un couple <clôture, pile>, mais le changement est cosmétique.
Comme les noms des transitions ne sont pas standardisés dans la littérature, les noms choisis ici ont l'avantage d'être les mêmes en français et en anglais.
Les x du terme sont liés à un λ que l'on atteint sans traverser aucun autre λ.
Page 66 de « Pierre-Louis Curien. Categorical Combinators, Sequential Algorithms and Functional, Birkhaüser, 1993. 2nd edition ».
Malgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt, « Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines », LICS 2017,‎ juin 2017 (lire en ligne)
John C. Reynolds « Definitional Interpreters for Higher-Order Programming Languages » (1972) (DOI 10.1145/800194.805852)
— Proceedings of 25th ACM National Conference,
John C. Reynolds, « Definitional Interpreters Revisited », Higher-Order and Symbolic Computation, vol. 11, n^o 4,‎ 1998, p. 355-361 (DOI 10.1023/A:1010075320153)
David A. Schmidt « State transition machines for lambda calculus expressions » (1980) (DOI 10.1007/3-540-10250-7_32)
— Semantics-Directed Compiler Generation, LNCS 94,
David A. Schmidt, « State-transition machines, revisited », Higher-Order and Symbolic Computation, vol. 20, n^o 3,‎ 2007, p. 333-335 (DOI 10.1007/s10990-007-9017-x)
Mads Sig Ager, Dariusz Biernacki, Olivier Danvy et Jan Midtgaard « A Functional Correspondence between Evaluators and Abstract Machines » (2003) (DOI 10.7146/brics.v10i13.21783)
— 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'03),
Pierre-Louis Curien, « An Abstract Framework for Environment Machines », Theoretical Computer Science, vol. 82, n^o 2,‎ 1991, p. 389-402 (DOI 10.1016/0304-3975(91)90230-Y)
Małgorzata Biernacka et Olivier Danvy (Article #6), « A Concrete Framework for Environment Machines », ACM Transactions on Computational Logic, vol. 9, n^o 1,‎ 2007, p. 1-30 (DOI 10.7146/brics.v13i3.21909)
Wouter Swierstra « From mathematics to abstract machine: A formal derivation of an executable Krivine machine » (2012) (lire en ligne)
— Proceedings of the Fourth Workshop on Mathematically Structured Fsunctional Programming (MSFP 2012),
«_Xavier Leroy, The ZINC experiment: an economical implementation of the ML language, Inria, Rapport Technique 117, 1990 ».

Bibliographie

Jean-Louis Krivine: A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation 20(3): 199-207 (2007) archive.
Pierre-Louis Curien. Categorical Combinators, Sequential Algorithms and Functional Birkhaüser, 1993. 2nd edition.
Frédéric Lang: Explaining the lazy Krivine machine using explicit substitution and addresses. Higher-Order and Symbolic Computation 20(3): 257-270 (2007) archive.
Olivier Danvy (Éd.): éditorial du numéro spécial de Higher-Order and Symbolic Computation sur la machine de Krivine, vol. 20, n^o 3 (2007)
Pierre-Louis Curien et Roberto Amadio, Domains and Lambda-calculi, vol. 45, Cambridge University Press, coll. « Cambridge Tracts in theoretical computer science », 1998

Voir aussi

Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.