SECD-machine je abstraktní stroj , interpret výrazů λ-kalkulu . Používá čtyři zásobníky: S ( angl. stack ) - zásobník objektů pro výpočet rekurzivních výrazů, E ( angl. environment ) - kontext (mapování identifikátorů na objekty), C ( angl. control list ) - control line (control list), D ( dump ) je výpis, úložiště předchozích stavů používané k návratu z volání funkce.
Tlumočníka navrhl v roce 1964 Peter Landinv článku "The Mechanical Evaluation of Expressions" (mechanické hodnocení výrazů) [1] . Stroj SECD vytvořil základ mnoha praktických implementací funkčních programovacích jazyků (jak dychtivých, tak líných hodnocení ), i když je stále potřeba optimalizovat. [2]
V každém okamžiku má stroj SECD stav reprezentovaný jako n-tice čtyř zásobníků a jeho činnost lze popsat pomocí přechodové funkce z jednoho stavu do druhého.
Zpočátku jsou kontext E, zásobník S a výpis D prázdné a výraz, který má být vyhodnocen, je načten jako jeden prvek jazyka C, který je během vyhodnocování převeden na reverzní polskou notaci . Jediná operace použitá v tomto případě je application , označená symbolem ap (z anglického apply - apply). Například výraz f (gx) (jediný prvek seznamu) je nahrazen seznamem [x, g, ap, F, ap].
Výpočet C se provádí podle reverzní polské logiky. Pokud je prvním prvkem v C hodnota, je vložen do zásobníku S. Přesněji, pokud je prvkem identifikátor, hodnota bude vazbou pro tento identifikátor v aktuálním kontextu E. Pokud je prvek λ-abstrakce , aby se zachovaly jeho volné proměnné vazby(které jsou v E) se vytvoří uzávěr a nasune se na stoh S.
Pokud je prvkem C ap (aplikace), vyskočí ze zásobníku dvě hodnoty a první se použije na druhou. Pokud je výsledkem aplikace hodnota, přesune se do zásobníku S.
Pokud je však aplikace λ-abstrakce hodnoty, bude to mít za následek výraz lambda-kalkulu, který může být sám aplikací (spíše než hodnotou), a proto nemůže být vložen do zásobníku. V tomto případě se aktuální obsah S, E a C vysype do D (což je zásobník těchto trojic), S se vyprázdní a C se znovu inicializuje pro výsledek aplikace a E se poskytne kontext. pro volné proměnné tohoto výrazu, doplněné o vazby vyplývající z aplikací. Výpočty pokračují výše uvedeným způsobem.
Znakem dokončení mezivýpočtů je prázdný zásobník C. V tomto případě bude výsledek v zásobníku S. V tomto případě je poslední uložený stav výpočtů načten ze zásobníku D a umístěn na odpovídající zásobníky. . Výpočet pokračuje výše uvedeným způsobem.
Pokud jsou C a D prázdné, vyhodnocení skončí výsledkem na zásobníku S.