Information Technology Reference
In-Depth Information
shape. For instance, if the law does not have the
wd
term of the transformed
program in its consequent, the elimination of the proviso in (5) fails. The imple-
mentation is, nonetheless, suciently robust to handle such cases; this merely
shows in the accumulation of provisos that could not be removed.
The examples used so far do not illustrate how provisos in the recast laws
reduce those of the former laws beyond typing conditions. For example, as-
signment is encoded by the semantic function
Assign
C
(
a
,
ns
,
es
)where
a
is
the alphabet, and
ns
and
es
are sequences of variables and expressions. Here,
wd Assign
C
(
a
,
ns
,
es
) does not merely constrain
a
to be of type
ALPHABET
,
ns
to be of type seq
VAR
,and
es
to be of type
WT EXPRESSION
, but states the
stronger (
a
,
ns
,
es
)
dom
Assign
C
, which, by definition of
Assign
C
,moreover
implies that the sequences
ns
and
es
have the same length. Conditions like these
would formerly have to be explicitly specified in the antecedent of the law. The
simplification becomes even more apparent when the left and right-hand pro-
grams of the law are more complex. Despite, experience so far shows that in cer-
tain cases we still need to specify non-trivial type provisos, namely when in a law
A
∈
B
we cannot prove
wd B
from
wd A
, but this is not very often the case.
The next section discusses an approach to the treatment of provisos similar to
the one above, but in the context of monotonicity theorems. It ensures that the
application of structural combinators does not introduce further assumptions.
4.2 Structural Combinators
The
ArcAngel
C
implementation requires, for each combinator, two monotonicity
theorems: one for equivalence and one for refinement. These theorems are used
when applying the respective combinator tactic. They also give rise to provisos
that accumulate. In general, the monotonicity theorems are of the form
:
T
k
;
p
1
,...,
p
n
:
T
;
p
1
,...,
p
n
:
T
∀
a
1
:
T
1
;
...
;
a
k
|
P
[
a
1
,...,
a
k
,
p
1
,...,
p
n
]
P
[
a
1
,...,
a
k
,
p
1
,...,
p
n
]
∧
•
p
1
p
1
∧
p
2
p
2
∧
...
∧
p
n
p
n
⇒
op
(
a
1
,...,
a
k
,
p
1
,...,
p
n
)
where
op
(
a
1
,...,
a
k
,
p
1
,...,
p
n
)isan(
n
+
k
)-ary operator with fixed arguments
a
1
,...,
a
k
and monotonic arguments
p
1
,...,
p
n
. For example, a conditional is a
programming operator whose condition is a fixed argument, and whose programs
are monotonic arguments. For action operators,
T
is
CIRCUS ACTION
.The
provisos
P
and
P
establish that the application of
op
is well-defined on both
sides of the concluding refinement. They imply that (
a
1
,...,
a
k
,
p
1
,...,
p
n
)and
(
a
1
,...,
a
k
,
p
1
,...,
p
n
) both belong to dom
op
.
Using the
wd
function, we generally express these theorems now as
∀
op
(
a
1
,...,
a
k
,
p
1
,...,
p
n
)
;
p
1
,...,
p
n
a
1
:
U
;
...
;
a
k
:
U
;
p
1
,...,
p
n
:
U
:
U
|
p
1
∈
p
n
∈
wd
(
op
(
a
1
,...,
a
k
,
p
1
,...,
p
n
))
∧
T
∧
...
∧
T
•
p
1
∧
p
2
∧
p
n
⇒
p
1
p
2
...
∧
p
n
op
(
a
1
,...,
a
k
,
p
1
,...,
p
n
)
op
(
a
1
,...,
a
k
,
p
1
,...,
p
n
)
∧
wd
(
op
(
a
1
,...,
a
k
,
p
1
,...,
p
n
))
.
Search WWH ::
Custom Search