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. Credit Market Competition and Capital Regulation
4. THE INTERNATIONAL OUTLOOK FOR U.S. TOBACCO
5. Pupils’ attitudes towards art teaching in primary school: an evaluation tool
6. Behaviour-based Knowledge Systems: An Epigenetic Path from Behaviour to Knowledge
7. The name is absent
8. The name is absent
9. The technological mediation of mathematics and its learning
10. Nietzsche, immortality, singularity and eternal recurrence1