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

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

Proof.The proof extends the proof of Theorem42,just as the proof of Theorem39extends that of Theorem40.We use the same canonical forms as in Theorem42,and just need to show that

K P can be eliminated by induction on K.For case K

1∨K

2

,

we have(K

1∨K

2

) P equivalent to(K

1

P)∨(K2 P).

For case True,we have True P equivalent to b P.Case False is immediate,since False P is equivalent to false.Case P◦I is also immediate,since(P1◦I) P is equivalent to P1−•P. For case P◦η[K],we have(P1◦η[K]) P equivalent to K (bη(P1−•P))where,if S={a1,...,a n},then b S(P)is b a1(P)∨···∨c a n(P)and c S⊥(P)is c a⊥1(P)∧···∧c a⊥n(P).The result follows by the induction hypothesis.

Finally,we show that CL for trees is parametrically more expres-sive than BL.We are unable to give a direct proof.We instead show a strong inexpressivity result based on interpretationσeq,which in-terprets p as the property that all the labels in the tree are equal.We show that formula(0 p)(a[true]),corresponding to the weakest precondition of deleting a subtree with root label a,is not express-ible in BL.Intuitively,the result holds since CL can remove a sub-tree at an arbitrary position,while BL can only split trees at the top level using◦or under afixed number of edges usingµ. Theorem44(Parametric Inexpressivity).Let A be an infinite al-

phabet.Then B L T ree

A,{p} C L T ree

A,{p}

.

Proof.The structure of the proof is identical to that of Theorem41. Consider the CL formula P (0 p)(a[true]),which says that

we can remove a subtree with root a from the current tree and

the result satisfies p.Intuitively,BL can remove subtrees from the

top level of the current tree using◦,but cannot remove them from

arbitrary positions.As in Theorem41for sequences,we restrict our

attention to BL-formulae with a single propositional variable p and

node labels from afinite set A ⊆A.We define the interpretation

as t∈σ(p)iff all the labels in tree t are equal.

Let∼be the unique relation such that:

t∼t iff t∈σ(p)⇔t ∈σ(p)and

if t≡a1[t1]then∃a 1,t 1such that

t ≡a 1[t 1]and t1∼t 1and

a1∈A or a 1∈A implies a1=a 1and

if t≡t1|t2then∃t 1,t 2such that

t ≡t 1|t 2and t1∼t 1and t2∼t 2

It is easy to see that∼is compatible withσ,and we will show that

it is a BL-bisimulation.Let b,c be distinct labels not in A ∪{a}, and define t1 b[a[0]|b[0]]and t2 b[a[0]|c[0]].We have t1∼t2 andσ,t1|=P butσ,t2|=P,hence the result.

We must show that∼is a bisimulation for all the modalities

of B L T ree

A ,{p}

.The modalities0,◦,µare immediate from the

definition of∼.Modalities−•,bµ,b follow from the fact that∼is a congruence:that is,if t∼t then c(t)∼c(t )for all tree contexts c.For the modality,we need to show that,if c(t1)≡t and t∼t , then there exist c ,t 1such that t ≡c (t 1)and t1∼t 1.The proof is straightforward,by induction on the size of c.

6.Concluding Remarks

We have shown how to present CL and BL as ML,interpreting the structural connectives as modalities satisfying a set of well-behaved ML-axioms.We have given two applications of the general theory of ML:we have proved completeness results for CL and BL using a general theorem about ML due to Sahlqvist,and inexpressivity results using the standard ML-bisimulation technique.

Our parametric inexpressivity results for arbitrary formulae contrast with Lozes’expressivity results on closed formulae.We prove that SL is parametrically more expressive than PL for heaps,whereas Lozes shows that these logics have the same expressivity on closed formulae.We also prove that CL for trees is parametri-cally more expressive than AL,whereas Lozes shows that they have the same expressivity on closed formulae.Our definition of para-metric expressivity corresponds to that studied in the ML-literature, and corroborates our intuition that the structural connectives of CL and BL are essential for our local Hoare reasoning.Lozes’style of expressivity result is not typically explored in the ML-literature.It is interesting for our application of structured data:for example,we have shown that CL for sequences corresponds to the∗-free regu-lar languages on closed formulae.The structural connectives of CL and BL give rise to several examples of logics which are paramet-rically more expressive,but which have the same expressivity on closed formulae.We currently do not know of other examples of ML where this is the case,except for simple examples such as S4 and S5where all closed formulae correspond to either true or false.

We are only at the beginning of studying expressivity results for CL:for example,two natural extensions involve higher-order quantification andfirst-order quantification.The parametric expres-sivity results in this paper are based on formulae with propositional variables.Our results say nothing about the expressivity of higher-order SL over higher-order logic.Also,our results compare CL and BL withoutfirst-order quantification,whereas their applications to analysing trees and heaps usually involve quantification over node labels and heap addresses.Dawar,Gardner and Ghelli(with thanks to Yang)have shown that adjunct-elimination in AL with quan-tification is not possible[6],strengthening a previous result by Lozes[9].Despite this inexpressivity result,it still makes sense to ask for parametric inexpressivity results about particular formulae, to pin d …… 此处隐藏：5150字，全部文档内容请下载后查看。喜欢就下载吧 ……