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

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

satisfies P2;the other adjoint P1−◦P2places data to the right.This distinction has no effect in the heap model,but is important in the sequence model.As in CL,we define the negation duals of the ad-joints as P1−•P2 ¬(P1−◦¬P2)and P1•−P2 ¬(P1◦−¬P2). Definition7(BL-Model).A BL-model M is a tuple(D,·,e)such that

1.D is a set;

2.·⊆(D×D)×D is an associative relation:we use the notation

d1·d2=d3for((d1,d2),d3)∈·;

3.e⊆D acts as a left and right identity to·:that is,

•∀d∈D,∃e∈e,d ∈D.e·d=d

•∀d∈D,∃e∈e,d ∈D.d·e=d

•∀d,d ∈D,∀e∈e.e·d=d or d·e=d implies d=d .

Any BL-model M=(D,·,e)can be transformed into a CL-model M BL=(D,D,·,e).We highlight specific BL-models for heaps, sequences and trees,since we will use them throughout this paper.

Example8.

•Heap=(D,·,{e})where D,·and e are as in Example3.•Seq A=(D A,·,{0})where D A is the set of sequences con-structed from the elements in set A,·is sequence concatenation, and0is the empty sequence.

•T ree A=(D A,|,{0})where D A is the set of trees in Exam-ple3,|is horizontal tree composition,and0is the empty tree.

Contrast these BL-models with the analogous CL-models given in Example3,which also emphasise the context structure.The heap model is essentially the same,with the context set being the same as the data set.However,the sequence and tree models are different, since the context set is more complex than the data set.

Definition9(BL-Satisfaction Relation).Given a BL-model M= (D,·,e),the BL-satisfaction relation is of the formσ,M,d BL P where d∈D,andσ:V P→P(D).As before,it is defined by induction on the structure of formulae.We only give the cases for the structural connectives:

σ,M,d BL P1◦P2iff∃d1,d2∈D.

d1·d2=d∧σ,M,d1 BL P1∧σ,M,d2 BL P2σ,M,d BL0iff d∈e

σ,M,d BL P1−◦P2iff∀d1,d2∈D.

σ,M,d1 BL P1∧d·d1=d2⇒σ,M,d2 BL P2σ,M,d BL P1◦−P2iff∀d1,d2∈D.

σ,M,d1 BL P1∧d1·d=d2⇒σ,M,d2 BL P2

Consider the BL-model Seq A,the derived BL-formula1 ¬0∧¬(¬0◦¬0)specifying sequences of length one,and the BL-relation

σ,Seq A,s BL(0−◦p)◦1,

whereσ(p)again denotes the set of sequences with equal elements. This relation only holds if s is a non-empty sequence consisting of equal elements except the last one which can be anything:for example,the relation holds when s is b·b·a,but does not hold when s is b·a·b and b·a·c.This simple example illustrates the difference between BL-and CL-reasoning:BL-reasoning analyses the ends of the sequences,whereas CL-reasoning also analyses the middle. However,when the CL-model arises from a BL-model,there is a strong relationship between BL-reasoning and and CL-reasoning. We give this correspondence explicitly for heaps in Proposition26.

The Hilbert-style BL-proof theory consists of analogous rules to those given for the CL-proof theory(Definition5),with an additional axiom for the associativity of◦.3.Connection to Modal Logic

We recall some general theory of ML,and show how CL and BL fit within this formalism.We prove completeness results relating the CL-and BL-proof theories with their respective models,by appealing to a general theorem of ML due to Sahlqvist.

Definition10(ML-Signature).A ML-signature is a tripleΣ= (S,O,ρ:O→T),where S is a set of sorts ranged over by S, O is a set of modalities ranged over by∆,T is a set of types of the form(S1,...,S n)→S for S i,S∈S,andρis a function.We write∆:T whenρ(∆)=T.

Definition11(ML-Model2).Given a ML-signatureΣ=(S,O,ρ),

a ML-model MΣgenerated fromΣconsists of a set M S for each S∈S,and an interpretation M∆⊆(M S

1

×···×M S

n

)×M S for each modality∆of type(S1,...,S n)→S.

Example12(ML-signature for CL).Consider the ML-signature ΣCL consisting of two sorts D,C with modalities ap:(C,D)→D, I:()→C, :(D,D)→C and :(C,D)→D.Given a CL-model M=(D,C,ap,I),we can view it as a ML-model MΣ

CL

, where M D=D,M C=C,the interpretations M ap and M I are inherited from the CL-model,and M and M are given by(c,d,d )∈M ap iff(d,d ,c)∈M iff(c,d ,d)∈M . Hence,every CL-model can be interpreted as a ML-model.Notice that not all ML-models over signatureΣCL are CL-models,since the I modality need not have any relationship to the ap modality. Definition13(ML-Formulae).Given ML-signatureΣ=(S,O,ρ) and disjoint,countably infinite sets V S of propositional variables for each sort S,the set PΣof ML-formulae overΣis given by

P::=p S|P1∨P2|¬P|false

S

|∆(P1,...,P n) where p S∈V S and,for each∆:(S1,...,S n)→S,the formula ∆(P1,...,P n)has sort S provided the P i have sort S i.We write PΣ

S

for the set of formulae of sort S generated from signatureΣ. Definition14(ML-Satisfaction Relation).Given ML-signature Σ=(S,O,ρ)and ML-model MΣ,the ML-satisfaction relation ML consists of relations of the formσ,M,m S P for each sort S∈S,where m∈M S,formula P has sort S and,for each propositional variable p S,σ(p S)⊆M S.It is defined by induction on the structure of ML-formulae,with the modality case given by σ,M,m S∆(P1,...,P n)⇔∀i∈{1,...,n}.∃m i.

σ,M,m i S

i

P i∧((m1,...,m n),m)∈M∆. The other cases are evident.

Example15.Given CL-model M and corresponding ML-model MΣ

CL

from example12,the CL-and M …… 此处隐藏：4071字，全部文档内容请下载后查看。喜欢就下载吧 ……