Program Semantics and Classical Logic

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 = P₁, . . . , P_n = 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 ∪ P⁰⁰ or hXi ^ Pi)*=₁(P0). Consider the greatest i such
that P_i does not have the form L₀ ; Q; Q_i . Then P_k is of the form L₀ ; Q; Q_k
for i < k ≤ n, while P_i has the form L₀; Q⁰; Q_i+1 , Q follows from Q⁰ by the ∪
rule or the ρ rule, and Pi+1 is a leftmost immediate consequence of Pi . For
i < k ≤ n, define P_k⁰ to be L0; Q⁰; Qk. Then Pi = P_i⁰₊₁ and it is easily seen
that P1 , . . . , Pi-1 , P_i⁰₊₁ , . . . , P_n⁰ is a derivation of P_n⁰ from L of length n - 1.
Using induction we find a leftmost derivation of P_n⁰ from L of the same length.
Since P_n is a leftmost immediate consequence of P_n⁰ (= L₀; Q⁰; Q_n) 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.

<<   6   7   8   9   10   11   12   >>

More intriguing information