Go backward to
Other Standard Abstractions
Go up to
Top
Go forward to
Recursively Defined Abstractions
Semantics
General typing patterns:
p
|- U:
H
define
I=U: {I:
H
}
dec
p
|-
invoke
I:
H
, if (I:
H
) in
p
Procedures: lazy evaluation.
[[
p
|-
proc
I=C: {I:
comm
}
dec
]]
e
s
= {I=
r
},
where
r(s')
= [[
p
|- C:
comm
]]
e
s'
.
[[
p
|-
call
I:
comm
]]
e
s
=
r(s)
where (I=
r
) in
e
.
Eager procedures: backtracking (non-local jumps).
[[
p
|-
proc
I=C: {I:
comm
}
dec
]]
e
s
= {I=
s'
},
where
s'
= [[
p
|- C:
comm
]]
e
s
.
[[
p
|-
call
I:
comm
]]
e
s
=
s'
, where (I=
s'
) in
e
.
Constants: eager evaluation.
[[
p
|-
const
I=N: {I:
int
}
dec
]]
e
s
= {I=
n
},
where
n
= [[
p
|- N:
int
]]
e
.
Author:
Wolfgang Schreiner
Last Modification: April 2, 1998