Go backward to Consequences of Correspondence
Go up to Top
Go forward to Proof of Correspondence
Semantics of Correspondence
- Lazy evaluation semantics of functions:
-
[[pi |- fun I=E: {I: tauexp}dec]]
= ({I=f}, )
where () = [[pi |- E: tauexp]]
-
[[pi |- I: tauexp]] = ()
where (I=) in
- Semantics of expression parameters:
-
[[pi |- define I(I: tauexp) =
U: {I: tauexp theta}dec]]
= ({I=}, )
where
= [[pi -U- {I:tauexp}
|- U: theta]]( -U- {I=})
-
[[pi |- invoke I(E): theta]] =
where (I=) in
and = [[pi |- E: tauexp]]
-
[[pi |- I: tauexp]] = ()
where (I=) in e
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: parameter.tex,v 1.1 1996/04/25 11:40:48 schreine Exp schreine