Machine de Krivine
En informatique théorique, la machine de Krivine est une machine abstraite (on peut aussi dire une machine virtuelle) 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 implante 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, qui est un modèle de calcul à la base de l'évaluation des programmes récursifs comme on en trouve en programmation fonctionnelle, mais aussi dans la plupart des langages de programmation.
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 ... u, 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[2]. 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.
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 implanter 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[3]. 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 implante 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 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[4]. 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.
| 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). Nous commençons donc par l'état (λ 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)
| ((λ 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).
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.
- 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 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.
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, no 3 (2007)
