Go backward to Eager Evaluation
Go up to Top
Go forward to Semantics of Eager Evaluation
Semantics of Lazy Evaluation
- Store is given when function is invoked.
- [[p |- define I=U: {I:H}dec]]e s
= {I=f},
where f s' = [[p |- U:H]]e s'.
- [[p |- invoke I:H]]e s = f s,
where (I=f) in e.
- Soundness of copy rule:
- [[ |- define I_j=V_j in C: comm]]
= [[{} |- [V_j/I_j]C: comm]]{}.
- Relation to core language:
- Core semantics [[.]]_c, extended semantics [[.]]_a.
- If C contains no identifiers, then [[C: comm]]_c =
[[p |- C: comm]]_a e, for e consistent with p.
- Copy rule semantics:
- [[ |- define I_1=V_1, ..., I_n=V_n in
C: comm]]_a = [[ [V_j/I_j]C: comm]]_c.
Copy rule simpler than basic semantics!
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: abstraction.tex,v 1.1 1996/03/05 08:55:21 schreine Exp schreine