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:
p
dec
]]{}
s
Declaration: [[D:
S
dec
]]:
Environment
->
Store
->
Environment
[[
p
|-
fun
I=E: {I:
T
exp
}]]
e
s
= {I=
f
}
where
f(s')
= [[
p
|- E:
T
exp
]]
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
1
dec
]]
e
s
and
e
2
= [[
p
|-D
2
:
p
2
dec
]]
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
1
dec
]]
e
s
and
e
2
= [[
p
U
p
1
|- D
2
:
p
2
dec
]](
e
union
e
1
)
s
Author:
Wolfgang Schreiner
Last Modification: April 2, 1998