SECD-mașină este o mașină abstractă , un interpret de expresii ale calculului λ . Utilizează patru stive: S ( eng. stack ) - un teanc de obiecte pentru calcularea expresiilor recursive, E ( eng. mediu ) - context (mapping identificatori la obiecte), C ( eng. control list ) - linie de control (lista de control), D ( dump ) este un dump, o stocare a stărilor anterioare folosită pentru a reveni de la un apel de funcție.
Interpret propus în 1964 de Peter Landinîn articolul „The Mechanical Evaluation of Expressions” (evaluarea mecanică a expresiilor) [1] . Mașina SECD a stat la baza multor implementări practice ale limbajelor de programare funcționale (atât evaluarea dornică , cât și leneșă ), deși încă trebuie optimizată. [2]
În orice moment, mașina SECD are o stare reprezentată ca un tuplu de patru stive, iar funcționarea sa poate fi descrisă folosind o funcție de tranziție de la o stare la alta.
Inițial, contextul E, stiva S și dump D sunt goale, iar expresia care trebuie evaluată este încărcată ca un singur element al lui C, care este convertit în notație poloneză inversă în timpul evaluării. Singura operație folosită în acest caz este application , notat cu simbolul ap (din engleză apply - apply). De exemplu, expresia f (gx) (singurul element al listei) este înlocuită cu lista [x, g, ap, F, ap].
Calculul lui C se efectuează conform logicii poloneze inverse. Dacă primul element din C este o valoare, acesta este împins în stiva S. Mai precis, dacă elementul este un identificator, valoarea va fi legătura pentru identificatorul respectiv în contextul curent E. Dacă elementul este o abstractizare λ , pentru a-și păstra legările variabile libere(care sunt în E) se formează o închidere și se împinge pe stiva S.
Dacă elementul C este ap (aplicație), două valori sunt scoase din stivă, iar prima este aplicată celei de-a doua. Dacă rezultatul aplicației este o valoare, aceasta este împinsă în stiva S.
Cu toate acestea, dacă aplicația este o abstracție λ a unei valori, aceasta va avea ca rezultat o expresie de calcul lambda care poate fi ea însăși o aplicație (mai degrabă decât o valoare) și, prin urmare, nu poate fi împinsă în stivă. În acest caz, conținutul curent al lui S, E și C este aruncat în D (care este o stivă a acestor triple), S este golit și C este reinițializat pentru rezultatul aplicației și lui E i se dă un context pentru variabilele libere ale acestei expresii, completate cu legăturile rezultate din aplicații. Calculele continuă ca mai sus.
Semnul finalizării calculelor intermediare este stiva goală C. În acest caz, rezultatul va fi în stiva S. În acest caz, ultima stare salvată a calculelor este preluată din stiva D și plasată pe stivele corespunzătoare. . Calculul continuă ca mai sus.
Dacă C și D sunt ambele goale, evaluarea se încheie cu rezultatul de pe stiva S.