Go backward to
Semantics
Go up to
Top
Go forward to
Example
Recursively Defined Abstractions
Typing rule:
p
U {I:
comm
} |- C:
comm
rec-proc
I=C: {I:
comm
}
dec
Procedure binding visible to own body!
Repetitive constructs:
while
E
do
C
od
=
call
W
where
rec-proc
W =
if
E
then
C;
call
W
else skip fi
.
Semantics:
[[
p
|-
rec-proc
I=C: {I:
comm
}
dec
]]
e
s
= {I=
r
}
where
r(s')
= [[
p
U {I:
comm
} |- C:
comm
]]
(
e
union{I=
r
})
s'
.
Copy rule:
rec-proc
I=C =
define
I=(
rec
I:
comm
. C).
(
rec
I:
comm
.C) => [(
rec
I:
comm
.C)/I]C.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: abstraction.tex,v 1.1 1996/03/05 08:55:21 schreine Exp schreine
