SECD und so

Da ich mich gerade in der Vorbereitung auf eine Präsenzübung zum Thema SECD befinde und selbst im Internet leider sehr wenig dazu gefunden habe gibt es hier mal einige Regeln.

λISWIM -> SECD
Konstante
b -> b
Variable
X -> X
Funktion
λx.y -> <x, y>
Applikation
(x y) -> x y ap
Primitivum
(+ x y) -> x y prim+

SECD -> λISWIM
Konstante
b -> b
Variable
X -> X
Funktion
<x, y> -> λx.y
Applikation
x y ap -> (x y)
Primitivum
x y prim+ -> (+ x y)

SECD auswerten

Startzustand
S, E, C, D
Stack, Evironment, Code, Dump

Konstantenregel:
<S, E, bC, D> -> <bS, E, C, D>

Variablenregel:
<S, E, XC, D> -> <XS, E, C, D>

Abstraktionsregel:
<S, E, <x, y>C, D> -> <<<x, y>,E’>S, E, C, D>

Applikationsregel:
b, x sind im Stack
<b<xS>, E, ap C, D>
-> Stack wird geleert
-> Environment wird neu gesetzt
-> alte SECD-Maschine wird mit leerem Stack und Evironment in den Dump geschrieben
<S, (X -> b), Rest vom alten Stack, <ε, (), ap C, D>>

Primitivumregel:
<bo … b1S, E, prim+, D> -> <(prim+ b0 … b1)S, E, C, D>
anstatt der runden Klammer schreibt man gleich das Ergebnis hin, also b0 + … + b1

Beispiel:
<ε, (), <x, x x prim+>23 ap, ε>
-> Abstraktionsregel
<<x, x x prim+>, ()>, (), 23 ap, ε>
-> Konstantenregel
<23<x, x x prim+>, ()>, (), ap, ε>
->Applikationsregel
<ε, (x->23), x x prim+, <ε, (), ε, ε>>
-> Variablenregel
<23, (x->23), x prim+, <ε, (), ε, ε>>
-> Variablenregel
<23 23, (x->23). prim+, <ε, (), ε, ε>>
-> Primitivumregel
<46, (x->23), ε, <ε, (), ε, ε>>
-> wenn der Code leer ist ersetzt, sofern vorhanden, die letzte SECD-Maschine die im Dump gespeichert ist die aktuelle SECD-Maschine. mit Ausnahme des Stacks
<46, (), ε, ε>