Stroj SECD je virtuální stroj (nazývaný také abstraktní stroj ), který byl navržen tak, aby sloužil jako cíl pro kompilaci prvních programovacích jazyků a měl velký vliv na počátky výpočetních a programovacích jazyků, včetně virtuálního prostředí Java. stroj . SCDS jeho zkratka pochází ze čtyř složek jeho zdravotní stav a to baterie ( s stehování v angličtině), na e nvironment, o c ontrol, na d eposit ( d UMP v angličtině).
Tento stroj od Petera J. Landina byl prvním formálním popisem vyhodnocení lambda-kalkulu a byl vyvinut v roce 1963 ve spolupráci s jeho projektem programovacího jazyka ISWIM . Vzhledem k tomu, že Landinův původní popis ve tmě zanechal mnoho podrobností, nejpoužívanější prezentací SECD je ta, kterou Peter Henderson vytvořil v roce 1980 jako součást svého překladače Lisp Lispkit . Od té doby se používá jako cíl pro několik překladačů a zejména jako základ pro implementaci hardwaru prováděnou vědci z University of Calgary.
Stroj SECD je stroj na vytváření zásob a hodnot, který implementuje volání podle hodnoty pro lambda-kalkul. V lambda-kalkulu je hodnotou buď proměnná, nebo abstrakce . Vyhodnocení ve volání podle hodnoty znamená, že vyhodnotíme výraz (λ x. A) B , vyhodnocením B pak λ x. . Jinými slovy vyhodnotíme volání funkce aplikované na parametry tak, že nejprve vyhodnotíme parametry, potom tělo funkce. Ve stroji SECD zásobník S a prostředí E ukládají pouze hodnoty, zatímco D se používá k vyhodnocení ostatních, tj. Aplikací. Stav stroj je n-tice ( S , E , C , D ).
Před spuštěním je výraz, který má být vyhodnocen, přeložen do reverzní polské notace s jediným operátorem ap (tj. Operátor aplikace), poté nainstalován do části C zprávy (ovládací prvek), zatímco E , S a D jsou prázdné. Například výraz x (yz) vytváří výraz z : y : ap : x : ap, což je seznam [z, y, ap , x, ap ] . Zařízení přepíná z jednoho stavu do druhého následujícím způsobem.
Napsáno ve formě pravidel:
(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) je hodnota spojená s x v prostředí E a E '+ (x ↦ v) je prostředí E' obohacené o odkaz z v na x .
Počáteční stav je (□, □, C , □) a konečný stav je ([V], E , □, □)
Stroj SECD musí být umístěn v historickém kontextu (1963), kde se rodí funkční programovací jazyky , kde rekurze v počítačové vědě je zárodkem, kde je pojem zásobníku sotva vymazán, zatímco se objevují metody hodnocení (volání podle jména a volání podle hodnoty). Pokud si pamatujeme, že se jedná o první abstraktní stroj pro implementaci programovacího jazyka, jaký byl kdy vynalezen, chápeme, že Peter J. Landin je vizionář a že SECD znamenal zásadní krok v chápání rekurze, která se začíná objevovat v programovacích jazycích Jako Algol 60 .