Machine SECD

La machine SECD est une machine virtuelle (dite encore machine abstraite) qui a été conçue pour servir de cible^[1] à la compilation des premiers langages de programmation et a eu une grande influence sur les origines de l'informatique et des langages de programmation, y compris la machine virtuelle Java. Son acronyme SECD provient des quatre constituants de son état^[2] à savoir la pile (stack en anglais), l'environnement, le contrôle, le dépôt (dump en anglais).

Cette machine, due à Peter J. Landin, a été la première description formelle de l'évaluation du lambda-calcul et fut élaborée en 1963 en association avec son projet de langage de programmation ISWIM. Comme la description originelle de Landin laissait beaucoup de détails dans l'ombre, la présentation de la SECD qui est la plus communément acceptée est celle que Peter Henderson a faite en 1980 dans le cadre de son compilateur Lisp Lispkit. Depuis, elle a été utilisée comme cible de plusieurs compilateurs et en particulier comme base d'une implantation matérielle réalisée par des chercheurs de l'université de Calgary^[3].

Description informelle

La machine SECD est une machine à base de piles et de valeurs, qui implante l'appel par valeur pour le lambda-calcul. En lambda-calcul, une valeur est soit une variable, soit une abstraction. Évaluer en appel par valeur signifie que l'on évalue une expression (λ x. A) B, en évaluant B puis λ x. A. Dit autrement, on évalue l'appel d'une fonction appliquée à des paramètres en évaluant d'abord les paramètres, puis le corps de la fonction. Dans la machine SECD, la pile S et l'environnement E ne stockent que des valeurs, tandis que D sert à évaluer le reste, c'est-à-dire les applications. Un état de la machine est un quadruplet (S, E, C, D).

Transitions

Avant de commencer, l'expression à évaluer est traduite en notation polonaise inverse avec comme seul opérateur ap (c'est-à-dire l'opérateur d'application), puis installée dans la partie C de l'état (le contrôle), tandis que E, S et D sont vides. Par exemple l'expression x (y z) produit l'expression z : y : ap : x : ap qui est la liste [z, y, ap, x, ap]. La machine passe d'un état à un autre comme suit.

• Si le premier élément de la liste C est une valeur, elle est mise sur la pile. Plus précisément,
  • si cette tête de liste est une variable, l'expression mise sur la pile S est la valeur associée à cette variable dans l'environnement E,
  • si cette tête de liste est une abstraction, une clôture est alors créée avec l'environnement E et mise sur la pile S.
• Si le premier élément de la liste C est un opérateur ap, le sommet de la pile est^[4] une valeur v suivie d'une abstraction λ x. c. Le contenu de S, E et C est mis sur D (qui fonctionne comme une pile de triplets) tandis que S est réinitialisé à vide (noté □), C est réinitialisé à c et E est réinitialisé à E enrichi de la liaison de x à la valeur v ; puis l'évaluation continue à partir de ce nouvel état.
• Une évaluation incomplète est terminée quand la liste C du contrôle est vide, auquel cas un résultat v se trouve sur le sommet de la pile S. Mais, à ce stade, si le dépôt D n'est pas vide, le calcul n'est pas terminé. Les trois constituants S, E, C sont alors dépilés du dépôt D et rétablis dans l'état courant, puis on ajoute v sur le sommet de la nouvelle pile, initiant un nouveau calcul.
• Quand C et D sont vides le calcul est complètement terminé et le résultat final se trouve dans la pile S.

Écrit sous forme de règles cela donne:

(S, E, x:C, D) ➝ (E(x) : S, E, C, D)

(S, E, (λ x. C') : C, D) ➝ (<(λ x. C'), E> : S, E, C, D)

(v : <(λ x. C'), E'> : S, E, ap : C, D) ➝ (□, E'+(x ↦ v), C', (S, E, C) : D)

(v : S, E, □, (S', E', C') : D) ➝ (v : S', E', C', D)

E(x) est la valeur associée à x dans l'environnement E et E'+(x ↦ v) est l'environnement E' enrichi de la liaison de v à x.

Début et fin

L' état initial est (□, □ , C, □) et l' état final est ([v], E, □, □)

Aspect historique

La machine SECD doit être replacée dans un contexte historique (1963) où les langages de programmation fonctionnelle naissent, où la récursivité en informatique est embryonnaire, où la notion de pile est à peine dégagée^[5] tandis qu'émergent les méthodes d'évaluation (appel par nom et appel par valeur). Si on se souvient qu'elle est la première machine abstraite d'implantation d'un langage de programmation jamais inventée, on comprend que Peter J. Landin fasse figure de visionnaire et que la SECD ait marqué une étape fondamentale dans la compréhension de la récursivité qui commence à apparaître dans les langages de programmation comme Algol 60.