Fixpunktberechnung im Interpreter

Erweiterung der abstrakten Syntax:

data Exp = ... | Rec Name Exp

Beispiel

App 
  (Rec g (Abs v (if v==0 then 0 else 2 + g(v-1))))
  5

Bedeutung: Rec x B bezeichnet den Fixpunkt von (λx.B) mathend000#

Definition der Semantik:

value (E, Rec x B) = 
    fixpoint $ \ v -> value (E[x:=v],B)



Johannes Waldmann 2014-03-31