Go backward to Semantics of Parameter Lists Go up to Top Go forward to Summary (Typing Rules)

Lambda Abstraction Principle

The parameterization principle is a lambda abstraction principle.

• Parameterized abstraction is just abstraction whose body is parameterized phrase.
• Lambda notation emphasizes this point.
  • lambdaI:theta. U
• Parameterization is distinct from abstraction!
  • Parameterized phrases need not be named.
  • (lambdaX:intexp. A:=X)(@A+1)
• Typing rules use new type attribute.
  • theta₁ -> theta₂

Abstraction and parameterization are orthagonal principles.