Go up to Top Go forward to Command Blocks

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.

  • pi1 |- D: pi2dec	pi1 -U- pi2 |- U: theta
    pi1 |- 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