Go backward to
Summary (Typing Rules V)
Go up to
Top
Go forward to
Summary (Semantics II)
Summary (Semantics I)
Lazy evaluation semantics of abstractions:
[[
P
|-
define
I=U: {I:
H
}
dec
]]
e
s
= {I=
f
},
where
f s'
= [[
P
|- U:
H
]]
e
s'
.
[[
P
|-
invoke
I:
H
]]
e
s
=
f s
,
where (I=
f
) in
e
.
Recursively defined abstractions (example)
[[
P
|-
rec-proc
I=C: {I:
comm
}
dec
]]
e
s
= ({I=
r
},
s
)
where
r(s')
= [[
P
U {I:
comm
} |- C:
comm
]] (
e
union{I=
r
})
s'
.
Soundness of typing rules:
[[
P
|- U:
H
]] in
Env
P
->
[[
H
]].
Program
[[D
in
C:
comm
]]
s
= [[
P
1
|- C:
comm
]]
e
1
s
,
where (
e
1
,
s
1
) = [[{} |- D:
P
1
dec
]]{}
s
Author:
Wolfgang Schreiner
Last Modification: April 23, 1998
