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.
pi
_{1}
|- D:
pi
_{2}
dec
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
_{1}
(I
_{2}
:
theta
) = U
in
I
_{1}
(V)
begin define
I
_{2}
= V
in
U
end
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998