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

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

Definition27(CL for Seq A).CL for Sequences generated by al-

phabet A,denoted C L Seq

A ,is given by the ML-signatureΣCL+Seq

A

consisting ofΣCL extended by the modalities:

0:()→D,a:()→D,◦r:(C,D)→C◦l:(D,C)→C

for a∈A.The CL-model Seq A is a model of C L Seq

A with the

interpretation of the additional modalities given by:

M0={0}where0denotes the empty sequence

M a={a}for each a∈A

M◦

r ={(c,s,c·s)|c∈C A,s∈D A}

M◦

l

={(s,c,s·c)|s∈D A,c∈C A}

We will use the notation K◦P for◦r(K,P)and P◦K for ◦l(P,K),overloading◦as the subscripts can be inferred.

We require the additional modalities◦r and◦l for analysing se-

quence contexts,since unlike the heap case these cannot be derived from application.We can derive a formula for sequence compo-sition P1◦P2 (P1◦I)(P2)which specifies that a sequence can be split into two sequences,the left one satisfying P1and the right one P2.This is logically equivalent to(I◦P2)(P1). We also derive the two corresponding right adjoints:the formula P1◦−P2 (P1◦I) P2specifies that,whenever a sequence sat-isfying property P1is joined to the left of the given sequence,then the result satisfies P2;similarly for P1−◦P2 (I◦P1) P2.For example,the formula a−◦P specifies that joining a to the right of the sequence results in a sequence satisfying P.In contrast,notice that the formula(a P)(0)specifies that,whenever an a is put somewhere in the given sequence,then the result satisfies property P.Again,logical equivalence of C L Seq

A

is sequence equality. Definition28(BL for Seq A).BL for sequences generated from

alphabet A,denoted B L Seq

A

,is given by the ML-signature

ΣBL+Heap=ΣBL∪{a|a∈A}.

The BL-model Seq A is a model of B L Seq

A with the interpretation

of the additional modalities defined as given in Definition27.

B L Seq

A is a sublogic of C L Seq

A

.Unlike the heap case,there

is no collapse of the CL-reasoning,and the question of whether

C L Seq

A is more expressive than

B L Seq

A

is subtle.Consider the

CL-formula(0 b◦c)(a).It is logically equivalent to the formula a◦b◦c∨b◦a◦c∨b◦c◦a.Now consider the CL-formula (0 True(b))(a).It is equivalent to true◦b◦true◦a◦true∨true◦a◦true◦b◦true,which has very different structure to the previous

example.We shall see in section5.2that C L Seq

A and

B L Seq

A

are equality expressive in the sense that every CL-formula without propositional variables has an equivalent BL-formula.However, they are not parametrically as expressive,in the sense that the CL-formula(0 p)(a),for propositional data variable p,cannot be

expressed in B L Seq

A .By contrast,C L Seq

A

without the modality

is parametrically as expressive as B L Seq

A

.

4.3Trees

CL for trees generated by alphabet A is CL extended by specific modalities which can be interpreted in the CL-model T ree A pre-sented in Example3.The additional modalities correspond to the empty tree,and modalities for analysing tree contexts.

Definition29(CL for T ree A).CL for trees,denoted C L T ree

A ,

is given by the ML-signatureΣCL+T ree

A consisting ofΣCL ex-

tended by the additional modalities:

0:()→D,µ:(C)→C,◦:(D,C)→C

whereµ::=a|a⊥for a∈A.The CL-model T ree A is a model of

C L T ree

A with the interpretation of the additional modalities given

by:

M0={0}where0denotes the empty tree

M a={(c,a[c])|c∈C}

M a⊥={(c,a [c])|c∈C,a ∈A−{a}}

M◦={(t,c,t|c)|t∈D,c∈C}

We writeµ[K]forµ(K),and P◦K for◦(P,K).

Apart from the0,the additional modalities describe ways of

analysing tree contexts:either tree contexts consist of a rootµwith

a subcontext underneath,or they can be split at the top level into

data and a context.The rootµcan either be the node label a∈A,

or a⊥denoting any label which is not a.The a⊥modalities are

not given explicitly in[3],since they are derivable with existential

quantification and label equality.They are important for our com-

parison with BL-reasoning,and also play a prominent role in logic-

based query languages for XML(see XDUCE[7]).We only require

one modality◦for splitting contexts,since our tree composition is

commutative.Analogous to the heap case,we have the derived for-

mulae P1◦P2 (P1◦I)(P2)and P1−◦P2 (P1◦I) P2.

Definition30(BL for T ree A).BL for trees generated from

alphabet A,denoted B L T ree

A

,is given by the ML-signature

ΣBL+T ree

A

consisting ofΣBL extended by the modalities:

µ:(D)→D,bµ:(D)→D, :(D)→D b :(D)→D

The BL-model T ree A is a model of B L T ree

A

with the interpreta-

tion of the additional modalities given by:

M a={(t,a[t])|t∈D}

M a⊥={(t,a [t])|t∈D,a ∈A−{a}}

M bµ={(a [t],t)|(t,a [t])∈Mµ}

M ={(t,c(t))|t∈D,c∈C}

M b ={(c(t),t)|(t,c(t))∈M }

B L T ree

A

is a sublogic of C L T ree

A

.The BL-formulaµ[P]

specifies a tree with top node described byµ.It is derivable in

C L T ree

A

as(µ[P◦I])(0).The modalities a⊥are essential to

express deep properties of trees in BL.For example,let1denote

all the trees with one …… 此处隐藏：4777字，全部文档内容请下载后查看。喜欢就下载吧 ……