Machine de Krivine

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Une vue imagée d'une 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[modifier | modifier le code]

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.

Réduction en forme normale de tête[modifier | modifier le code]

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.

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[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

L'état est formé de trois composants:

  1. un terme,
  2. une pile,
  3. 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[modifier | modifier le code]

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

Transitions de la machine de Krivine[5]
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[modifier | modifier le code]

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

La présentation qui est donnée ici est celle de Pierre-Louis Curien[7] à 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 implante l'appel par nécessité (voir aussi l'article de Frédéric Lang cité).

Notes et références[modifier | modifier le code]

  1. 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.
  2. Si on a seulement affaire à des termes clos il s'agit d'une abstraction, autrement dit un terme de la forme λ x. t.
  3. 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.
  4. 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.
  5. 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.
  6. Les x du termes sont liés à un λ que l'on atteint sans traverser aucun autre λ.
  7. Page 66 de « Pierre-Louis Curien. Categorical Combinators, Sequential Algorithms and Functional, Birkhaüser, 1993. 2nd edition ».

Bibliographie[modifier | modifier le code]

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

Voir aussi[modifier | modifier le code]