Go backward to Semantics of Lazy Evaluation
Go up to Top
Go forward to Other Standard Abstractions
Semantics of Eager Evaluation
- Store is given when function is defined.
- [[p |- define I=U: {I:H}dec]]e s
= {I=[[p |-U:H]]e s.
- [[p |- invoke I: H]]e s = v,
where (I=v) in e.
- Example:
- [[p |- const I=E: {I:Texp}]]e s
=
{I=[[p |- E: Texp]]e s}.
- [[p |- I: Texp]]e s = v,
where (I=v) in e.
- Improper meaning for body:
- [[p |- loop: intexp]]e s =
bottom.
- [[p |- fun A=loop in skip:
comm]]e s
=
[[ {A: intexp} |- skip: comm]]e_0 s,
where e_0 = {A=[[{}|- loop:
intexp]]{} s}
= {A = bottom
= [[{A: intexp} |- skip:
comm]]bottom s
= bottom.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: abstraction.tex,v 1.1 1996/03/05 08:55:21 schreine Exp schreine