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
- 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.
- L'état d'une machine virtuelle est une structure de donnée qui est transformée par les transitions de la machine.
- Un article sur la conception SECD: DESIGN ISSUES est disponible.
- C'est toujours ainsi dans un calcul qui se déroule correctement !
- Claude Pair n'a soumis sa thèse Étude de la notion de pile : application à l'analyse syntaxique qu'en 1966.
Bibliographie
- Danvy, Olivier. A Rational Deconstruction of Landin's SECD Machine. BRICS research report RS-04-30, 2004. ISSN 0909-0878
- Field, Anthony J. Field and Peter G. Harrison. 1988 Functional Programming. Addison-Wesley. (ISBN 0-201-19249-7)
- Graham, Brian T. 1992 "The SECD Microprocessor: A Verification Case Study". Springer. (ISBN 0-7923-9245-0)
- Henderson, Peter. 1980 Functional Programming: Application and Implementation. Prentice Hall. (ISBN 0-13-331579-7)
- Kogge, Peter M. The Architecture of Symbolic Computers. (ISBN 0-07-035596-7)
- Peter J. Landin, « The Mechanical Evaluation of Expressions », Comput. J., vol. 6, no 4,‎ , p. 308–320 (DOI 10.1093/comjnl/6.4.308)
- Peter J. Landin, « The next 700 programming languages », Comm. ACM, vol. 9, no 3,‎ , p. 157–166 (DOI 10.1145/365230.365257, lire en ligne)
Voir aussi
- SĂ©mantique des langages de programmation
- Sémantique opérationnelle
- Machine de Krivine
- Machine virtuelle Java
- Système de transition d'états
- (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « SECD machine » (voir la liste des auteurs).