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

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

We often call D the data set and C the context set,because of the form of our motivating examples.Of course,there are mod-els which do notfit this structured data intuition.We prove com-pleteness for these CL-models(theorem23)and the analogous BL-models(section3.2).

Example3.

•Mon D=(D,D,·,{e})where D is a partial monoid with

binary operation·:(D×D) D and unit e∈D.•Heap is an example of Mon D where D=N+ fin N is the set offinite partial functions denoting the heaps and e denotes

the empty heap.The domain N+=N−{0}does not include

0as it is reserved for the null location.Given heaps h,h ,the

heap composition h·h is function union which is only defined

when dom(h)∩dom(h )=∅.

•T ermΣ=(DΣ,CΣ,ap,{})where DΣis the data set of

terms constructed from the n-ary function symbols in signature

Σ,CΣis the corresponding set of contexts,ap denotes the

standard application of contexts to terms,and denotes the

empty context.

•Seq A=(D A,C A,ap,{})where D A is the set of sequences

constructed from the elements in alphabet A,C A is the corre-

sponding set of contexts,and ap and are as for T ermΣ.

•T ree A is an example of T ermΣwith an additional equality

relation on terms.The terms are generated by the signatureΣ

constructed from the setsΣ0={0},Σ1=A andΣ2={|},

whereΣi denotes the function symbols of arity i.We use the

notation t|t for|(t,t )and a[t]for a(t).Terms are considered

modulo an equality relation generated by the axioms0|t≡t,

t|t ≡t |t,(t|t )|t ≡t|(t |t ),and closed by the

obvious structural rules for the function symbols.

•Rel D=(D,P(D×D),ap,{i})where D is an arbitrary

set,P(D×D)denotes the set of binary relations on D,ap

is relational application,and i is the identity relation.

Definition4(CL-Satisfaction Relation).Given a CL-model M= (D,C,ap,I),the CL-satisfaction relation CL consists of two re-lationsσ,M,d P P andσ,M,c K K where d∈D,c∈C and interpretation functionσ:V→P(D∪K)maps data proposi-tional variables to sets of data,and context propositional variables to sets of contexts.The two relations are defined by induction on the structure of the formulae:the cases for the propositional variables and the boolean additive connectives are standard;the cases for the structural connectives are

σ,M,d P K(P)iff∃c∈C,d ∈D.

ap(c,d )=d∧σ,M,c K K∧σ,M,d P P σ,M,d P K P iff∀c∈C,d ∈D.

σ,M,c K K∧ap(c,d)=d ⇒σ,M,d P P σ,M,c K I iff c∈I

σ,M,c K P1 P2iff∀d,d ∈D.

σ,M,d P P1∧ap(c,d)=d ⇒σ,M,d P P2 We sometimes omit the subscripts P and K.

In section4,we study applications of CL to heaps,sequences and trees,which extend CL with simple atomic formulae specific to these models.Here,we use the Seq A model and the additional zero formula0,denoting the empty sequence,to illustrate our CL-reasoning.Consider the derived formula1 ¬0∧¬(¬I)(¬0), which states that the sequence only contains one element:that is, it is non-empty and cannot be split into a non-empty context and non-empty data.Now consider the judgement

σ,Seq A,s (0 p)(1),whereσ(p)denotes the set of sequences with equal elements and s denotes a sequence.This judgement only holds if s is non-empty and all the elements in s are equal except possibly one:for example, it holds when s is b·a·b,but not when s is b·a·c.

We use the standard derived classical formulae for both data and context formulae:true,P∧P and P⇒P;similarly for contexts, writing True for the context formula that is always satisfied.We shall also use the following derived formulae:

• P True(P)specifies that somewhere property P holds;•P1 P2 ¬(P1 ¬P2)specifies that there exists some data element satisfying property P1such that,when it is put in the hole of the given context,the resulting data satisfies P2;

•K P2 ¬(K ¬P2)specifies that there exists a context satisfying property K such that,when the given data element is put in the hole,the resulting data satisfies P2.

We give a Hilbert-style proof theory,following the style for BL in[10].The axioms and rules for the structural operators state that K P2and P1 P2are right adjoints of K(P1),and I is the identity of application.

Definition5(CL-Proof Theory).The Hilbert-style CL-proof the-ory consists of the standard axioms and rules for the boolean addi-tive connectives,and the following axioms and rules for the struc-tural connectives:

P P I(P)

K1 K K2P1 P P2

K1(P1) P K2(P2)

K(P1) P P2

K K P1 P2

K K P1 P2P P P1

K(P) P P2

K(P1) P P2

P1 P K P2

P1 P K P2K1 K K

K1(P1) P P2

We sometimes omit the subscripts in P and K,and sometimes write CL to refer explicitly to this CL-proof theory.

The proof theory given here emphasises the right adjoint proper-ties of and .In the next section,we show that this proof theory is equivalent to the standard ML-proof theory plus an additional set of axioms specific to CL.This alternative formulation emphasises the derived connectives and instead.

2.2Bunched Logic

We also present(a variant of)BL[10],its models and satisfaction relation,and compare it to CL.We use the notation◦and−◦, instead of the standard∗and−∗for the multiplicative conjunction and its adjoint.Our variation of standard BL does not require◦to be commutative,since one of our key example models is sequences where◦denotes concatenation.

Definition6(BL-For …… 此处隐藏：4125字，全部文档内容请下载后查看。喜欢就下载吧 ……