A SECD-gép egy absztrakt gép , a λ-kalkulus kifejezéseinek értelmezője . Négy veremet használ: S ( eng. stack ) - objektumok halma rekurzív kifejezések kiszámításához, E ( eng. Environment ) - kontextus (azonosítók objektumokhoz való hozzárendelése), C ( angol vezérlőlista ) - vezérlősor (vezérlőlista), A D ( dump ) egy kiíratás, a korábbi állapotok tárolója, amely egy függvényhívásból visszatér.
Tolmácsot javasolt 1964-ben Peter Landina "The Mechanical Evaluation of Expressions" (kifejezések mechanikai kiértékelése) című cikkben [1] . A SECD gép számos funkcionális programozási nyelv gyakorlati megvalósításának alapját képezte ( buzgó és lusta értékelések egyaránt ), bár még optimalizálásra szorul. [2]
A SECD-gépnek bármikor van egy állapota, amelyet négy veremből álló sorként ábrázolnak , és működése egy állapotból a másikba való átmenet függvényével leírható.
Kezdetben az E kontextus, az S verem és a D dump üres, és a kiértékelendő kifejezés a C egyetlen elemeként betöltődik, amelyet a kiértékelés során fordított lengyel jelöléssé alakítanak át . Ebben az esetben az egyetlen művelet az application , amelyet ap szimbólum jelöl ( angolul apply - apply). Például az f (gx) kifejezést (a lista egyetlen elemét) a lista [x, g, ap, F, ap] helyettesíti.
C számítása fordított lengyel logika szerint történik. Ha a C első eleme egy érték, akkor az S verembe kerül. Pontosabban, ha az elem egy azonosító, akkor az érték lesz az adott azonosító kötése az aktuális E kontextusban. Ha az elem egy λ-absztrakció , hogy megőrizze szabad változó kötéseit(amelyek az E-ben vannak) egy lezárást alakítanak ki , és az S kötegre tolják.
Ha C eleme ap (alkalmazás), akkor a rendszer két értéket ugrik ki a veremből, és az elsőt alkalmazza a másodikra. Ha az alkalmazás eredménye egy érték, akkor az S verembe kerül.
Ha azonban az alkalmazás egy érték λ-absztrakciója, akkor ez egy lambda-számítási kifejezést eredményez, amely maga is lehet alkalmazás (nem pedig érték), és ezért nem tolható be a verembe. Ebben az esetben az S, E és C aktuális tartalma D-be kerül (amely ezeknek a hármasoknak a halma), S üres lesz, és C újra inicializálódik az alkalmazás eredményéhez, és E kap egy kontextust. ennek a kifejezésnek a szabad változóihoz, kiegészítve az alkalmazásokból származó kötésekkel. A számítások a fentiek szerint folytatódnak.
A közbenső számítások befejezésének jele az üres C verem. Ebben az esetben az eredmény az S veremben lesz. Ebben az esetben a számítások utolsó mentett állapotát a D veremből lekérjük és a megfelelő verembe helyezzük. . A számítás a fentiek szerint folytatódik.
Ha C és D is üres, a kiértékelés az S veremben lévő eredménnyel zárul.