Go backward to Interpretation
Go up to Top
Go forward to The Semantics of Abstractions
The Semantics of Abstractions
- Environments hold function definitions.
- Set of (identifier, meaning) pairs.
- Must be propagated to all tree nodes.
- Program: [[P: comm]] in Store ->
Store_bottom
- [[|- D in C: comm]]s = [[p |- C:
comm]]e_0 s
where e_0 = [[{} |-D: pdec]]{} s
- Declaration: [[D: Sdec]]: Environment ->
Store -> Environment
- [[p |- fun I=E: {I:Texp}]]e s =
{I=f}
where f(s') = [[p |- E: Texp]]e s'
- [[p |- D_1;D_2: (p_1
U p_2)dec]]e s = e_1 union e_2
where e_1 = [[p |- D_1: p_1dec]]e s
and e_2 = [[p |-D_2: p_2dec]]e s
- [[p |-D_1;D_2: (p_1
U p_2)dec]]e s = e_1 union e_2
where e_1 = [[p |- D_1: p_1dec]]e s
and e_2 = [[p U p_1 |- D_2: p_2dec]](e
unione_1) s
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: abstraction.tex,v 1.1 1996/03/05 08:55:21 schreine Exp schreine