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. The name is absent
3. The name is absent
4. The name is absent
5. The economic doctrines in the wine trade and wine production sectors: the case of Bastiat and the Port wine sector: 1850-1908
6. Secondary school teachers’ attitudes towards and beliefs about ability grouping
7. Temporary Work in Turbulent Times: The Swedish Experience
8. Centre for Longitudinal Studies
9. Wounds and reinscriptions: schools, sexualities and performative subjects
10. The name is absent