Abstract Context Logic as Modal Logic Completeness and Param(11)

similar style of reasoning about structured data. They each consist of a structural (separating) composition for reasoning about disjoint subdata, and corresponding structural adjoint(s) for reasoning hypothetically about data. We show how to interpret the

the inexpressivity result we seek.Consider two sequences α1=a ·a ·a and α2=a ·a ·a ,where a =a are not in A .Observe that α1∼α2,as adjacent letters are distinct in both sequences,σ,α1|=(0 p )(a )but σ,α2|=(0 p )(a ).Assuming ∼is a bisimulation for B L Seq A ,{p },Proposition 33implies that σ,α1|=BL P iff σ,α2|=BL P for all BL-formulae P .We have therefore proved that there cannot be a BL-formula P which is equivalent to P .Note that our proof depends on A being an infinite set,since we need to pick new elements a and a not in A .

Finally,we must show that ∼is indeed a bisimulation for all the modalities of B L Seq A ,{p }.We only look at the ◦and −•modalities;the other cases are analogous or trivial.For the ◦modality,assume α·β=γand γ∼γ .We must show that ∃α ,β such that α ·β =γ and α∼α and β∼β .Choose α ,β as the unique splitting of γ such that |α |=|α|and |β |=|β|.Clearly α∼α and β∼β ,since adjacent elements in α and β are also adjacent in γ .For the −•modality,assume α·β=γand α∼α .We need to show that ∃β ,γ such that α ·β =γ and β∼β and γ∼γ .Since αand α might end in different letters,we must construct a β such that its first element relates to the last element of α in the same way as the first element of βrelates to the last

element of α.Let f :A →A be a bijection such that f (αi )=α i

.Such an f exists since α∼α .We define β

as the unique sequence

such that |β |=|β|,β

i

=f (βi )and γ α ·β .It is easy to see that β∼β and γ∼γ .5.3

Trees

We have the following results for trees for alphabet A :

•B L T ree A ,V D (−{−•,b µ,b })=C L T ree A ,V D (−{ , })•B L T ree A ,V D =C L T ree A ,V D (−{ })•B L T ree A ,{p } C L T ree A ,{p }if A is infinite.

The first result states that CL and BL for trees without adjoints have the same parametric expressive power.The second result states that adding the modality to CL gives the same expressivity as BL.This formalises our intuition that the modality is a compact way to express the adjoints of AL (plus ˆ ).The third result is a para-metric inexpressivity result,showing that CL for trees is parametri-cally more expressive than BL for trees.This result illustrates that is the key modality for giving CL its additional expressive power.In [3],we observed that it was important for expressing the weak-est preconditions of update commands.Our inexpressivity result formalises this intuition,which we had previously motivated by ex-ample.

Our first parametric expressivity result is that BL and CL for trees without adjoints are equally expressive.The proof shows that context formulae can be reduced to a canonical form,allowing con-text application to be eliminated by a form of syntactic substitution.Theorem 42(Parametric Expressivity).

B L T ree A ,V D (−{−•,b µ,b })=

C L T ree A ,V

D (−{ , })Proof.Note that propositional variables are restricted to sort D,so the context formulae of C L T ree A ,V D (−{ , })are:

K ::=I |K ∨K |¬K |False |µ[K ]|P ◦K We define a canonical subset,similar to that given in Theorem 39:

K ::=K ∨K |True |False |P ◦I |P ◦η[K ]η

::=

{a 1,...,a n }|{a 1,...,a n }⊥

The composition formulae analyse whether the hole is at the top level or under a node label.The formulae {a 1,...,a n }[K ]and {a 1,...,a n }⊥

[K ]are syntactic sugar for W i a i [K ]and V i a ⊥i [K ]respectively.Just as for Theorem 39,it is enough to show the following results:

(1)every CL-formula K is equivalent to a canonical formula K ;

(2)every application K (P )is equivalent to the substitution for-mula K [P/I, P/True ].To prove (1),we define a translation tr from context formulae to the canonical subset by:

tr (I )

0◦I

tr (K 1∨K 2)

tr (K 1)∨tr (K 2)tr (¬K ) Not (tr (K ))tr (False ) False

tr (µ[K ]) 0◦µ[tr (K )]tr (P ◦K )

Add (P,tr (K ))

where Not (K )and Add (P,K )are defined by induction on the structure of the canonical formulae.

Before defining Not ,we define a function And on canonical formulae such that And (K 1,K 2)is equivalent to K 1∧K 2:And (K 1∨K 2,K 3) And (K 1,K 3)∨And (K 2,K 3)

And (True ,K ) K And (False ,K ) False

And (P 1◦I,P 2◦I ) (P 1∧P 2)◦I And (P 1◦I,P 2◦η[K ]) False And (P 1◦η1[K 1],P 2◦η2[K 2])

(P 1∧P 2)◦(η1∧η2)[And (K 1,K 2)]

where,for sets S i ,we define S 1∧S 2=S 1∩S 2,S 1∧S ⊥

2

=S 1−S 2,and S ⊥1∧S ⊥2=(S 1∪S 2)⊥

.We now define the function Not such that Not (K )is equivalent to ¬(K ):

Not (K 1∨K 2)

And (Not (K 1),Not (K 2))Not (True ) False Not (False ) True

Not (P ◦I ) (¬P )◦I ∨true ◦∅⊥[True ]Not (P ◦η[K ])

true ◦I ∨true ◦η⊥[True ]∨

(¬P )◦η[True ]∨true ◦η[Not (K )]We finally define Add such that Add (P,K )is equivalent to P ◦K :Add (P,K 1∨K 2)

Add (P,K 1)∨Add (P,K 2)

Add (P,True ) (P ◦true )◦I ∨(P ◦true )◦∅⊥[True ]Add (P,False ) False

Add (P 1,P 2◦I ) (P 1◦P 2)◦I Add (P 1,P 2◦η[K ])

(P 1◦P 2)◦η[K ]

To prove (2),we proceed by induction on K .For case K 1∨K 2,note that (K 1∨K 2)(P )is equivalent to K 1(P )∨K 2(P )and hence,by induction,is equivalent to K 1[P/I, P/True ]∨K 2[P/I, P/True ].For case True,observe that True (P )is equiv-alent to P .Case False i …… 此处隐藏：4007字，全部文档内容请下载后查看。喜欢就下载吧 ……