Go backward to
Soundness of Typing Rules
Go up to
Top
Go forward to
Parameter Copy Rule
Copy Rule
Lazy evaluated parameters:
define
I
1
(I
2
:
theta
) = U ...
in
...
invoke
I
1
(V) ...
......
in
...[V/I
2
]U ...
Augment copy rule by rule for parameter binding.
Lambda abstraction
define
I
1
=
lambda
I
2
:
theta
.U
pi
-U- {I:
theta
1
} |- E:
theta
2
pi
|- (
lambda
I:
theta
1
.E):
theta
1
->
theta
2
[[
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
})
Author:
Wolfgang Schreiner
Last Modification: May 7, 1998