D in Declaration
U in Any-syntax-domain
A in Actual-parameter
D ::= ...| define I(I: theta) = U
U ::= ...| invoke I(A)
A ::= N | E | C | L | D | T
- Various parameters for U-abstractions.
- Criterium whether parameter forms fit to original language?
- Correspondence Principle
- define I = U.
- define I(I:theta) = ...in ...I(U).
- Semantics of binding I to U is the same.
For every abstraction form there may be a corresponding parameterization
form (and vice versa) with same binding semantics.
