this procedural way, the rule is a generalisation of the procedural rule for the
μ operator studied in [21, 3].
The following definition says what it is for a program to follow from
another program in one step. Note that we make use of the notational
convention given in the previous section here: Q1 and Q2 may be taken to
be empty.
Definition 4 (Immediate Consequence) A program Q1 ; Q; Q2 is an im-
mediate consequence of a program Q1 ; Q0; Q2 iff Q follows from Q0 by the
∪ rule or the ρ rule. Q1 ; Q; Q2 is a leftmost immediate consequence of
Q1 ; Q0; Q2 if, moreover, Q1 is linear.
From the notion of immediate consequence we can define the notion of com-
putational entailment we are after.
Definition 5 (Computational Entailment) A (leftmost) derivation of Pn
from P1 is a sequence of programs P1 , . . . , Pn such that each Pi+1 is a (left-
most) immediate consequence of Pi. We write P 'C Q (P 'LC Q) iff there is
a (leftmost) derivation of Q from P.
Example 1 The following is a leftmost derivation of
hZ ^ (x < 3?; x := x + 1; Z) ∪ —x < 3?i(Z),
which we shall abbreviate as D(Z), from the linear program x < 3?; x :=
|
x + 1;x < 3?;x := |
x + 1; —x < 3?. | |||
|
1. |
x < 3?; x := |
x + 1;x < 3?;x : |
x + 1; —x < 3? |
(premise) |
|
2. |
x < 3?; x := |
x + 1;x < 3?;x : |
= x+ 1; —x < 3?) |
(∪ rule) |
|
3. |
x < 3?; x := |
x + 1;x < 3?;x : |
= x + 1; D(Z) |
(ρ rule) |
|
4. |
x < 3?; x := |
x + 1; ((x < 3?;x |
:= x + 1; D(Z)) ∪ —x < 3?) |
(∪ rule) |
|
5. |
x < 3?; x := |
x+1;D(Z) |
(ρ rule) | |
|
6. |
(x < 3?; x := |
= x + 1; D(Z)) ∪-x< 3? |
(∪ rule) | |
|
7. |
D(Z) |
(ρ rule) | ||
8
More intriguing information
1. The name is absent2. Herman Melville and the Problem of Evil
3. The name is absent
4. The name is absent
5. The Economic Value of Basin Protection to Improve the Quality and Reliability of Potable Water Supply: Some Evidence from Ecuador
6. Dynamic Explanations of Industry Structure and Performance
7. Imperfect competition and congestion in the City
8. The name is absent
9. Update to a program for saving a model fit as a dataset
10. Improving behaviour classification consistency: a technique from biological taxonomy