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
}]]
e
= {I = [[
pi
|- E:
theta
]]
e
}
[[
pi
|- E
1
,E
2
:
pi
1
U
pi
2
]]
e
=
([[
pi
|- E
1
:
pi
1
]]
e
) union ([[
pi
|- E
2
:
pi
2
]]
e
)
[[
pi
|-
with
E
1
do
E
2
:
theta
]]
e
=
[[
pi
-U-
pi
1
|- E
2
:
theta
]](
e
-U- [[
pi
|- E
1
:
pi
1
]]
e
)
[[
pi
|- I:
theta
]]
e
=
v
, where (I=
v
) in
e
[[
pi
|-
lambda
I:
theta
1
. E:
theta
1
->
theta
2
]]
e
=
f
where
f
u
= [[
pi
-U- {I:
theta
1
} |- E:
theta
2
]](
e
-U- {I=
u
})
[[
pi
|- E
1
E
2
:
theta
2
]]
e
=
([[
pi
|- E
1
:
theta
1
->
theta
2
]]
e
)([[
pi
|- E
2
:
theta
1
]]
e
)
Type semantics:
[[{
i
:
theta
i
}
i
in
I
]] = {
i
:[[
theta
i
]] }
i
in
I
[[
theta
1
->
theta
2
]] = [[
theta
1
]]
->
[[
theta
2
]]
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998