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. Factores de alteração da composição da Despesa Pública: o caso norte-americano2. Public Debt Management in Brazil
3. The name is absent
4. The name is absent
5. Poverty transition through targeted programme: the case of Bangladesh Poultry Model
6. Emissions Trading, Electricity Industry Restructuring and Investment in Pollution Abatement
7. IMPLICATIONS OF CHANGING AID PROGRAMS TO U.S. AGRICULTURE
8. Backpropagation Artificial Neural Network To Detect Hyperthermic Seizures In Rats
9. The name is absent
10. Family, social security and social insurance: General remarks and the present discussion in Germany as a case study