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

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 third result shows that full BL is parametrically as expressive as CL without the modality.The fourth result illustrates that the importance of CL-reasoning lies in the modality,by showing that CL for sequences is parametrically more expressive than BL for se-quences.Unlike the heap case,we are unable to give a direct proof of the parametric result.We give a proof of strong inexpressivity, and hence prove parametric inexpressivity.

Ourfirst parametric expressivity result for sequences shows that,without adjuncts,CL-application can be specified by BL-composition.The proof shows that any context formula can be expressed as the disjunction of formulae of the form P1◦I◦P2, and the application(P1◦I◦P2)(P)corresponds to P1◦P◦P2. Theorem39(Parametric Expressivity).

B L Seq

A,V D (−{−•,•−})=C L Seq

A,V D

(−{ , })

Proof.Note that propositional variables are restricted to sort D,so the context formulae of C L Seq

A,V D

(−{ , })are

K::=I|K∨K|¬K|False|K◦P|P◦K.

We define a canonical subset

K::=K∨K|P◦I◦P

and show that

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

(2)every application formula K(P)is equivalent to the substitu-

tion formula K[P/I].

The result follows.Given an arbitrary CL-formula,first replace the context subformulae by canonical formulae,then replace the application subformulae by the equivalent substitution formulae. The resulting formula is a BL-formula equivalent to the original CL-formula.

To show(1),we define a translation tr from context formulae to the canonical formulae by:

tr(I) 0◦I◦0

tr(K1∨K2) tr(K1)∨tr(K2)

tr(¬K) Not(tr(K))

tr(False) false◦I◦false

tr(K◦P) Add l(tr(K),P)

tr(P◦K) Add r(P,tr(K))

where Not(K),Add r(P,K)and Add l(K,P)are defined below 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(P1◦I◦P2,P3◦I◦P4) (P1∧P3)◦I◦(P2∧P4) We now define function Not:

Not(K

1∨K

2

) And(Not(K

1

),Not(K

2

))

Not(P1◦I◦P2) (¬P1)◦I◦true∨true◦I◦(¬P2) Add r(P,K)and Add l(K,P)are defined similarly to And.

(2)is proved 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,by the

induction hypothesis,it is equivalent to K

1[P/I]∨K

2

[P/I].Case

P1◦I◦P2is immediate since(P1◦I◦P2)(P)is equivalent to P1◦P◦P2.

As an example,consider the CL-formula(¬I)(P)satisfied by any sequence having a strictly smaller subsequence satisfying P. We have tr(¬I)=Not(tr(I))=Not(0◦I◦0)=(¬0)◦I◦true∨true◦I◦(¬0).Therefore(¬I)(P)is equivalent to (¬0)◦P◦true∨true◦P◦(¬0),which is satisfied by any sequence containing a subsequence satisfying P composed with a nonempty

sequence on at least one side.

Our next result shows that CL for sequences minus is para-metrically as expressive as BL for sequences.

Theorem40(Parametric Expressivity).

B L Seq

A,V D

=C L Seq

A,V D

(−{ })

Proof.As in the proof of Theorem39,we define a canonical subset:

K::=K∨K|P◦I◦P

The only difference compared with Theorem39is that now data formulae may contain the adjoint formulae K P.Given an arbi-trary CL-formula,first replace the context subformulae by canon-ical formulae,as in(1)of Theorem39,then replace the applica-tion subformulae by the equivalent substitution formulae as in(2). We must show how to eliminate the adjoint formulae K P, by induction on the structure of K.When K is P1◦I◦P2, then(P1◦I◦P2) P is equivalent to P1•−(P2−•P).

When K is K

1

∨K

2

,then(K

1

∨K

2

) P is equivalent to

(K

1

P)∨(K2 P).

Finally,we show that CL for sequences is parametrically more expressive than BL for sequences.This additional expressivity for CL must lie in the use of the modality.Intuitively,BL can only add elements to either side of a given sequence,whilst can add elements wherever the hole happens to be.We initially searched for a direct proof of this result,trying to identify a property analo-gous to the heap-reducing formulae of theorem34which captured this difference between adding elements to the side or the middle of sequences.BL-formulae can however affect the middle of the sequence,by using◦and−•to remove the whole sequence and adding any desired sequence.We do not know if such a direct re-sult is possible.Here,we prove our parametric expressivity result via a strong inexpressivity result using bisimulation.

Theorem41(Parametric Inexpressivity).Let A be an infinite al-phabet.Then B L Seq

A,{p}

C L Seq

A,{p}

.

Proof.We consider BL and CL for sequences containing formulae with at most one propositional variable p.Consider CL-formula P (0 p)(a)for some a∈A.Expecting a contradiction, assume that P is equivalent to data formula P ,and let A ⊆A be thefinite set of letters occurring in P .Formula P says that p holds after removing an element a somewhere from the current sequence.By contrast,BL can only ob …… 此处隐藏：4058字，全部文档内容请下载后查看。喜欢就下载吧 ……