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.

D'autre part, elle implémente l'appel par nom, parce qu'elle évalue le corps d'un β-redex^[2] 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.

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^[3].

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${\displaystyle _{1}}$ ... u${\displaystyle _{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^[4]. 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.

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

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^[5]. La machine de Krivine met en œuvre l'appel par nom du lambda-calcul.

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 est formé de trois composants:

1. un terme,
2. une pile,
3. 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^[6]. 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.

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

Transitions de la machine de Krivine^[7]

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.

Évaluons d'abord le terme (λ 0 0) (λ 0) qui correspond au terme (λ x. x x) (λ x. x)^[8]. 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).

La présentation qui est donnée ici est celle de Pierre-Louis Curien^[9] à 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é).

Machine à environment

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

Il existe une présentation de la machine de Krivine^[10] 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 ${\displaystyle t\star \pi }$, où ${\displaystyle t}$ est un terme et où ${\displaystyle \pi }$ est une pile de termes. Empiler ${\displaystyle u}$ sur ${\displaystyle \pi }$ s'écrit ${\displaystyle u::\pi }$. Les deux règles sont :

Transitions de la machine compacte

Nom	Avant	Après
Push	${\displaystyle t~s~\star ~\pi }$	${\displaystyle t~\star ~s::\pi }$
Grab	${\displaystyle \lambda x.t~\star ~s::\pi }$	${\displaystyle t[x:=s]~\star ~\pi }$

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^{[11],[12],[13],[14],[15]}.

Aussi, la machine de Krivine correspond syntaxiquement au ${\displaystyle \lambda {\widehat {\rho }}}$ calcul -- une version du ${\displaystyle \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^{[16],[17],[18]}. Si le ${\displaystyle \lambda {\widehat {\rho }}}$ calcul inclut la ${\displaystyle \beta }$ réduction généralisée (c'est-à-dire que le ${\displaystyle \beta }$ redex emboité ${\displaystyle (\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 coïncide avec le « brouillon » de Jean-Louis Krivine^[17]. (Et si la stratégie de réduction est l'appel par valeur de droite à gauche et inclut la ${\displaystyle \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.)^[19],[17]

• 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

• Sémantique des langages de programmation
• Sémantique opérationnelle
• Substitution explicite
• Réécriture (informatique)
• Fermeture (informatique)

• Portail de la logique
• Portail de l'informatique théorique
• Portail de la programmation informatique