The Qualification Principle

Any semantically meaningful syntactic class may admit local definitions.

• Local definitions.
  • Restrict scope of abstractions by
• Block structures:
  • U ::= ...| begin D in U end
  • Declarations D, block body U.
  • D visible only to U.

  • pi$$1 |- D: pi$$2dec	pi$$1 -U- pi$$2 |- U: theta
    pi$$1 |- begin D in U end: theta

• Correspondence to parameters:
  • For every parameterized abstraction form, a corresponding qualification form (and vice versa).
  • define I$$₁(I$$₂:theta) = U in I$$₁(V)
  • begin define I$$₂ = V in U end