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.
More intriguing information
1. Synchronisation and Differentiation: Two Stages of Coordinative Structure2. Cultural Neuroeconomics of Intertemporal Choice
3. Passing the burden: corporate tax incidence in open economies
4. Fiscal Policy Rules in Practice
5. The name is absent
6. Orientation discrimination in WS 2
7. Pass-through of external shocks along the pricing chain: A panel estimation approach for the euro area
8. The geography of collaborative knowledge production: entropy techniques and results for the European Union
9. Insurance within the firm
10. AGRICULTURAL TRADE IN THE URUGUAY ROUND: INTO FINAL BATTLE