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. Chebyshev polynomial approximation to approximate partial differential equations2. A dynamic approach to the tendency of industries to cluster
3. The name is absent
4. Innovation Trajectories in Honduras’ Coffee Value Chain. Public and Private Influence on the Use of New Knowledge and Technology among Coffee Growers
5. The name is absent
6. Tastes, castes, and culture: The influence of society on preferences
7. CONSIDERATIONS CONCERNING THE ROLE OF ACCOUNTING AS INFORMATIONAL SYSTEM AND ASSISTANCE OF DECISION
8. The name is absent
9. The name is absent
10. Poverty transition through targeted programme: the case of Bangladesh Poultry Model