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)!
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: parameter.tex,v 1.1 1996/04/25 11:40:48 schreine Exp schreine
