Accueil🇫🇷Chercher

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.

Notes et références

  1. En compilation le langage cible est le langage dans lequel le compilateur traduit les programmes du langage source. Ici on ne peut pas parler de langage cible puisqu'il s'agit d'une machine abstraite vers laquelle on traduit. On parle donc seulement de cible.
  2. L'état d'une machine virtuelle est une structure de donnée qui est transformée par les transitions de la machine.
  3. Un article sur la conception SECD: DESIGN ISSUES est disponible.
  4. C'est toujours ainsi dans un calcul qui se déroule correctement !
  5. Claude Pair n'a soumis sa thèse Étude de la notion de pile : application à l'analyse syntaxique qu'en 1966.

Bibliographie

Voir aussi

Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.