Go backward to
Parameterized Abstractions
Go up to
Top
Go forward to
Parameter Forms
Typing Rules
Abstraction:
pi
-U- {I
2
:
theta
1
} |- V:
theta
2
pi
|-
define
I
1
(I
2
:
theta
1
) = V: {I
1
:
theta
1
->
theta
2
}
dec
pi
1
-U-
pi
2
=
pi
2
-U-(
pi
1
- { (I:
v
) | (I:
w
) in
pi
2
, (I:
v
) in
pi
1
}).
Formal parameter cancels global identifier of same name.
Invocation:
pi
|- U:
theta
1
pi
|-
invoke
I(U):
theta
2
if (I:
theta
1
->
theta
2
) in
pi
Type of formal parameter must match type of actual parameter.
Formal parameter reference:
pi
|-I:
theta
if (I:
theta
) in
pi
Formal parameters are referenced like abstractions (correspondence)!
Author:
Wolfgang Schreiner
Last Modification: May 7, 1998