Note that D(Z) is the expanded form of while x < 3 do x := x + 1 od.
Clearly, the set of linear programs L such that L 'LC D(Z) can informally
be described as (x < 3?; x := x + 1)*; —x < 3?, where * is the Kleene star.
We shall be interested in the set of linear programs L which derive a given
program P . The following proposition shows that it is immaterial whether
we take the notion 'C or the notion 'LC as the underlying entailment relation.
Leftmost derivations are closer to actual executions, but the order in which
we execute statements does not matter for our purposes.
Proposition 2 If L 'C P then L 'LC P
Proof. Let L 'C P. We use induction on the length n of the derivation
L = P1, . . . , Pn = P of P from L to show that a leftmost derivation of P from
L of length n can be constructed. If n = 1 then P = L and the derivation is
leftmost, so assume that n > 1. Then Pn is of the form L0; Q; Qn with Q of
one of the forms P0 ∪ P00 or hXi ^ Pi)*=1(P0). Consider the greatest i such
that Pi does not have the form L0 ; Q; Qi . Then Pk is of the form L0 ; Q; Qk
for i < k ≤ n, while Pi has the form L0; Q0; Qi+1 , Q follows from Q0 by the ∪
rule or the ρ rule, and Pi+1 is a leftmost immediate consequence of Pi . For
i < k ≤ n, define Pk0 to be L0; Q0; Qk. Then Pi = Pi0+1 and it is easily seen
that P1 , . . . , Pi-1 , Pi0+1 , . . . , Pn0 is a derivation of Pn0 from L of length n - 1.
Using induction we find a leftmost derivation of Pn0 from L of the same length.
Since Pn is a leftmost immediate consequence of Pn0 (= L0; Q0; Qn) this also
gives us a leftmost derivation of P from L of length n. □
4 Classical Type Logic
Mainly in order to fix notation, we give a short exposition of classical type
logic, Church’s formulation of Russell’s Simple Theory of Types. For more
extensive treatments see [2, 8, 9, 4, 25, 1].
In classical type logic (higher-order logic) every expression comes with a
type . Types are either basic or complex. The type t of truth values should
be among the basic types, but there may be other basic types as well. In this
paper we fix the set of basic types as {t, e, s}, where e is the type of natural
numbers and s the type of states. The logic we are describing here thus is
essentially the two-sorted type logic TY2 of [4] (but we shall add product
types).
We build up complex types in the following way.