Machine de Krivine

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

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

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

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

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)[7]. Nous commençons donc par l'état (λ 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)

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