Go backward to
Summary (Semantics)
Go up to
Top
Go forward to
References
Summary (Lambda Abstraction)
Abstract syntax:
D ::= ...|
define
I
1
= A
A ::=
lambda
I:
theta
. U
U ::= ...|
invoke
I(V)
V ::= ...| I
Typing rules:
pi
-U- {I:
theta
1
} |- E:
theta
2
pi
|- (
lambda
I:
theta
1
.E):
theta
1
->
theta
2
Semantics:
[[
pi
|-
lambda
I:
theta
1
.E:
theta
1
->
theta
2
]]
e
=
f
where
f
v
= [[
pi
-U- {I:
theta
1
} |- E:
theta
2
]](
e
-U- {I=
v
})
Parameter copy rule:
(
lambda
I:
theta
. U)V
=>
[V/I]U
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: parameter.tex,v 1.1 1996/04/25 11:40:48 schreine Exp schreine