Go backward to Semantics of Records and Lambda Abstractions
Go up to Top
Go forward to Lazy Evaluation Semantics
Lazy Evaluation Semantics
- Lazily evaluated abstractions/records:
-
[[pi |- I=E: {I:theta}]] = {I = [[pi |- E:
theta]]}
-
[[pi |- E,E: pi U pi]] =
([[pi |- E: pi]])
union ([[pi |- E: pi]])
-
[[pi |- with do : theta]] =
[[pi -U- pi |- E: theta]](
-U- [[pi |- E: pi]])
-
[[pi |- I: theta]] = , where (I=) in
-
[[pi |- lambdaI:theta. E: theta
theta]] =
where = [[pi -U- {I:theta} |- E:
theta]]( -U- {I=})
-
[[pi |- E E: theta]] =
([[pi |- E: theta
theta]])([[pi |- E: theta]])
- Type semantics:
-
[[{:theta}]] =
{ :[[theta]] }
-
[[theta theta]] = [[theta]]
[[theta]]
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: records.tex,v 1.1 1996/05/20 12:33:10 schreine Exp schreine