SECD-maskin är en abstrakt maskin , en tolkare av uttryck för λ-kalkylen . Använder fyra stackar: S ( eng. stack ) - en stack av objekt för att beräkna rekursiva uttryck, E ( eng. miljö ) - kontext (mappning av identifierare till objekt), C ( eng. kontrolllista ) - kontrollrad (kontrolllista), D ( dump ) är en dump, en lagring av tidigare tillstånd som används för att återvända från ett funktionsanrop.
Tolk föreslagen 1964 av Peter Landini artikeln "The Mechanical Evaluation of Expressions" (mekanisk utvärdering av uttryck) [1] . SECD-maskinen har legat till grund för många praktiska implementeringar av funktionella programmeringsspråk (både ivrig och lat utvärdering ), även om den fortfarande behöver optimeras. [2]
När som helst har SECD-maskinen ett tillstånd representerat som en tupel av fyra stackar, och dess funktion kan beskrivas med hjälp av en övergångsfunktion från ett tillstånd till ett annat.
Inledningsvis är kontext E, stack S och dump D tomma, och uttrycket som ska utvärderas laddas som ett enda element av C, vilket konverteras till omvänd polsk notation under utvärdering. Den enda operation som används i detta fall är application , betecknad med symbolen ap (från engelskan applicera - applicera). Till exempel ersätts uttrycket f (gx) (det enda elementet i listan) med listan [x, g, ap, F, ap].
Beräkningen av C utförs enligt omvänd polsk logik. Om det första elementet i C är ett värde, skjuts det till stack S. Närmare bestämt, om elementet är en identifierare, kommer värdet att vara bindande för den identifieraren i det aktuella sammanhanget E. Om elementet är en λ-abstraktion , för att bevara dess fria variabla bindningar(som är i E) en förslutning bildas och skjuts på stapeln S.
Om elementet i C är ap (applikation), tas två värden från stacken, och det första tillämpas på det andra. Om resultatet av applikationen är ett värde, skjuts det till stack S.
Men om applikationen är en λ-abstraktion av ett värde, kommer detta att resultera i ett lambda-kalkyluttryck som i sig kan vara en applikation (snarare än ett värde) och därför inte kan skjutas in i stacken. I det här fallet dumpas det aktuella innehållet i S, E och C i D (som är en stack av dessa trippel), S görs tomt och C återinitieras för resultatet av applikationen, och E får ett sammanhang för de fria variablerna för detta uttryck, komplett med de bindningar som härrör från applikationer. Beräkningarna fortsätter enligt ovan.
Tecknet på slutförandet av mellanliggande beräkningar är den tomma stacken C. I detta fall kommer resultatet att vara i stacken S. I detta fall hämtas det senast sparade tillståndet för beräkningarna från stacken D och placeras på motsvarande stackar . Beräkningen fortsätter enligt ovan.
Om C och D båda är tomma, avslutas utvärderingen med resultatet på stack S.