Abstract Context Logic as Modal Logic Completeness and Parametric Inexpressivity Separation

更新时间：2023-07-18 20:05:01 阅读量：实用文档文档下载

说明：文章内容仅供预览，部分内容可能不全。下载后的文档，内容与下面显示的完全一致。下载之前请确认下面内容是否您想要的，是否完整无缺。

abstract推荐度：
相关推荐

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

Context Logic as Modal Logic: Completeness and Parametric Inexpressivity

Cristiano Calcagno Philippa Gardner Uri Zarfaty

Department of Computing,Imperial College London

{ccris,pg,udz}@doc.ic.ac.uk

Abstract

Separation Logic,Ambient Logic and Context Logic are based on a similar style of reasoning about structured data.They each consist of a structural(separating)composition for reasoning about dis-joint subdata,and corresponding structural adjoint(s)for reasoning hypothetically about data.We show how to interpret these struc-tural connectives as modalities in Modal Logic and prove complete-ness results.The structural connectives are essential for describing properties of the underlying data,such as weakest preconditions for Hoare reasoning for Separation and Context Logic,and secu-rity properties for Ambient Logic.In fact,we introduced Context Logic to reason about tree update,precisely because the structural connectives of the Ambient Logic did not have enough expressive power.Despite these connectives being essential,?rst Lozes then Dawar,Gardner and Ghelli proved elimination results for Separa-tion Logic and Ambient Logic(without quanti?ers).In this paper, we solve this apparent contradiction.We study parametric inexpres-sivity results,which demonstrate that the structural connectives are indeed fundamental for this style of reasoning.

Categories and Subject Descriptors D.2.4[Software/Program veri?cation]:Correctness proofs,Formal methods,Validation General Terms Languages,Theory,Veri?cation

Keywords Logic,Expressivity,Structured Data,Contexts

1.Introduction

Separation Logic(SL)and Ambient Logic(AL)are related log-ics for reasoning about heaps and trees respectively.O’Hearn, Reynolds and Yang introduced SL[8,11,13]to develop local Hoare reasoning about heap update,based on the general theory of Bunched Logic(BL)due to O’Hearn and Pym[10].Cardelli and Gordon independently introduced AL[5]for reasoning about static trees.AL has been used to reason about security properties of ?rewalls and structural properties of XML[6].We have integrated these two lines of research.In[3],we showed that it is not possible to use AL to reason about tree update(XML update).Instead,we introduced the general theory of Context Logic(CL)for reasoning about structured data,which generalises BL.We demonstrated that the application of CL-reasoning to trees can be used as a basis for Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for pro?t or commercial advantage and that copies bear this notice and the full citation on the?rst page.To copy otherwise,to republish,to post on servers or to redistribute to lists,requires prior speci?c permission and/or a fee.

POPL’07January17–19,2007,Nice,France.

Copyright c 2007ACM1-59593-575-4/07/0001...$5.00local Hoare reasoning about tree update,whilst the application of CL-reasoning to heaps exactly corresponds to SL-reasoning.

These logics are based on a similar style of reasoning about structured data.They each extend propositional connectives with a structural(separating)composition for reasoning about disjoint subdata,and the corresponding structural adjoint(s).1We show how to interpret the structural connectives of BL and CL as modalities in modal logic(ML).We present additional axioms for these modali-ties to give a precise correspondence between the original presenta-tion of BL and CL,and their ML-interpretations.These axioms are well-behaved,in that they satisfy the conditions necessary for us to apply a general completeness result about ML(Sahlqvist’s the-orem).We thus prove that the CL-proof theory is sound and com-plete with respect to the set of CL-models(and analogously for BL).This work follows previous unpublished work by Calcagno and Yang,who proved completeness for CL from?rst principles.

The structural connectives are essential for modular reason-ing about programs,and for describing weakest preconditions and safety properties.However,recent expressivity results for SL and AL due to Lozes[9]appear to contradict this fundamental claim. Lozes concentrates on expressivity for closed formulae,determin-ing whether an arbitrary closed formula specifying a set of data in one logic can be expressed by a formula in the other logic speci-fying the same set of data.For example,Lozes has shown that SL and Propositional Logic(PL)with simple atomic heap formulae are equally expressive using this de?nition of expressivity.How-ever,our experience says that SL is more expressive than PL,since for example we can reason directly about disjointness and dynamic update of linked lists.We solve this apparent mismatch between the theoretical results and our practical experience by proving in-expressivity results for stronger de?nitions of expressivity.

SL forms the basis of local Hoare reasoning about heap update. An important part of the reasoning is to be able to express the weakest preconditions,which provide completeness for straight-line code and have a key role in some veri?cation tools(to verify a Hoare triple,?rst?nd the weakest precondition of a given postcon-dition and then prove that the given precondition implies the weak-est precondition).Our results show that the weakest preconditions cannot be expressed in PL for heaps.To illustrate this,consider the weakest precondition of allocation(n→0)??p,specifying that whenever a cell with address n and value0is added to the given heap then the resulting heap satis?es post-condition p.Lozes’result says that,for every interpretation of p as a set of data determined by a closed formula,there is a corresponding PL-formula.How-ever,these PL-formulae are highly non-uniform with respect to the post-condition p,and Lozes’result says nothing about whether the weakest precondition itself can be speci?ed in PL.We show that it is not possible,by studying expressivity for open formulae con-1In this paper,we do not consider quanti?cation.

taining propositional variables.This notion of expressivity deter-mines whether an arbitrary open formula in one logic,specifying a function from sets to data to sets of data,can be expressed by a formula in the other logic.There are two choices for the domain of this function,either as sets of data speci?ed by closed formulae or as arbitrary sets of data.The?rst option is enough to determine whether the weakest precondition can be speci?ed in PL.It does not however allow for natural extensions to SL,such as the addition of inductive predicates.We therefore study the second option.We call this type of expressivity parametric expressivity,and show that SL is parametrically more expressive than PL for heaps by demonstrat-ing that(n→0)??p cannot be expressed in PL.

Although the SL-adjoint??is important for the weakest pre-conditions and has a key role in some proofs[12],it is not typi-cally used for specifying safety properties.For example,it plays no role in the veri?cation tool Smallfoot[1],which combines in-ductive predicates with a cut-down decidable fragment of SL(with quanti?cation).A more fundamental SL-formula is p?q specifying that the heap can be split into two disjoint parts,one satisfying p and the other q.Lozes’results imply that,for every interpretation of p and q as sets of data corresponding to closed formulae,there is a corresponding PL-formula.Again,the PL-formulae are highly non-uniform.We show that it is not possible to express parametri-cally this formula in PL.However,with the Smallfoot application in mind,it is perhaps more interesting to determine a speci?c in-expressivity result,that it is not possible to express p?q in PL with the interpretation of p as list(3),denoting the existence of a 0-terminated linked list starting at address3,and q as list(4).To do this,we study the notion of strong expressivity which states that, for a speci?c interpretation of the propositional variables as arbi-trary sets of data,every formula with propositional variables in one logic can be expressed in the other logic.

To prove our strong inexpressivity results,we use a standard bisimulation technique from ML.For example,consider the heaps h1=[3→n ,4→n ,n →0,n →0]

h2=[3→n ,4→n ,n →0,n →0].

These heaps are distinguished by SL-formula p?q,with the in-terpretation of p and q as the lists list(3)and list(4)respectively, since h1can be split into the appropriate disjoint lists whereas h2 cannot due to the sharing at address n .Our proof shows that there is a PL-bisimulation relation relating h1and h2.Bisimulation has the well-known property that it is contained in logical equivalence. Thus,the heaps h1and h2are indistinguishable using PL.

Our original motivation for studying parametric inexpressivity results came from studying CL for trees and AL.We introduced CL to provide local Hoare reasoning about tree update[3],demon-strating that it was not possible to base our Hoare reasoning on AL since it had a missing adjoint.Whilst we believe that our argument was convincing,it was an argument given by example rather than by a formal inexpressivity result.Lozes’expressivity results,fo-cussing on the closed formulae,show that the argument is subtle since AL(without quanti?ers)is as expressive as the logic without the structural adjoints[9,6].We prove that CL for trees is paramet-rically more expressive than AL.Unlike the results for SL,we do not know how to prove this directly.Instead,we prove a strong in-expressivity result using an analogous proof method to that outlined above.Since strong inexpressivity implies parametric inexpressiv-ity,we have the result.In addition,we prove that CL for trees minus the extra adjoint is parametrically as expressive as AL,thus show-ing that the additional strength of the CL-reasoning does indeed come from this additional adjoint.We also prove similar results for CL for sequences and a variation of BL applied to sequences(?is non-commutative).Sequences provide the simplest example of the differences between CL-and BL-reasoning.Again,we prove our parametric inexpressivity result via strong inexpressivity.

2.Context Logic and Bunched Logic

We review the general theory of CL and BL.

2.1Context Logic

We introduced CL to reason about data update[3].Local data up-date typically identi?es the portion of data to be replaced,removes it,and inserts the new data in the same place.With CL,we reason about both data and this place of insertion(contexts).CL consists of data formula denoted by P,and context formulae denoted by K. In each case,these include standard formulae from propositional logic,and less familiar structural formulae for directly analysing the data and context structure.

De?nition1(CL-Formulae).The set of CL-formulae consists of disjoint sets of data formulae P and context formulae K,con-structed from a set of propositional variables V=V P∪V K where V P and V K are disjoint,countably in?nite sets of propositional data variables and context variables respectively.The formulae are given by the grammars:

data formulae

P::=K(P)|K P structural formulae

P∨P|¬P|false additive formulae

p,p1,p2,...prop vars in V P

context formulae

K::=I|P P structural formulae

K∨K|¬K|False additive formulae

k,k1,k2,...prop vars in V K The key formulae are the structural formulae K(P),K P, P1 P2and I.The application formula K(P)speci?es that the

given data element can be split into a context satisfying K applied to data satisfying P.For example,if we de?ne the context formula True ¬False,then the formula True(P)states that some subdata satis?es property P.The next two formulae are both(right)adjoints of application.The formula K P is satis?ed by the given data if,whenever we insert the data into a context satisfying K,then the result satis?es P.For example,the formula(True P)states that,when the data is put in any context,the resulting data satis?es property P.The analogous connectives for AL have been used to describe security properties of trees(ambients).Meanwhile,P1 P2is a statement on contexts.It is satis?ed by a given context if, whenever we insert in the context some data satisfying P1,then the result satis?es P2.Given the derived data formula true ¬false, the context formula(true P2)states that,regardless of what data is put in the context hole,the resulting data satis?es property P2.This adjoint is essential for expressing weakest preconditions for update commands,as we demonstrated in[3],and has no counterpart in AL.The context formula I speci?es the empty context.

De?nition2(CL-Model).A CL-model M is a tuple(D,C,ap,I) such that

1.D and C are sets;

2.ap?(C×D)×D is a relation,called application:we use the

notation ap(c,d1)=d2for((c,d1),d2)∈ap;

3.I?C acts as a left identity to ap:that is,

??d∈D,?i∈I,d ∈D.ap(i,d)=d ;

??d,d ∈D,?i∈I.ap(i,d)=d implies d=d .

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 not?t 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 of?nite 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 de?ned

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.

De?nition4(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 de?ned 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 speci?c 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 satis?ed.We shall also use the following derived formulae:

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

?K P2 ¬(K ¬P2)speci?es that there exists a context satisfying property K such that,when the given data element is put in the hole,the resulting data satis?es 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.

De?nition5(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 speci?c 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.

De?nition6(BL-Formulae).The set of BL formulae P is con-structed from a countably in?nite set of propositional variables V P, and de?ned by the grammar:

P::=0|P?P|P??P|P??P structural formulae P∨P|¬P|false additive formulae

p,p1,p2,...prop vars in V P The key formulae are the structural formulae0,P1?P2,P1??P2 and P1??P2.The zero formula0speci?es empty data.The compo-sition formula splits the given data into two parts,the?rst satisfying P1and the second P2.For example,the formula¬0?¬0speci?es that the given data can be split into two disjoint,non-empty parts. Unlike the original BL,we have two right adjoints,due to?be-ing non-commutative:P1??P2speci?es that,whenever some data satisfying P1is placed to the left of the given data,then the result

satis?es 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 de?ne the negation duals of the ad-joints as P1??P2 ¬(P1??¬P2)and P1??P2 ¬(P1??¬P2). De?nition7(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 speci?c 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.

De?nition9(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 de?ned 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(De?nition5),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 ?t 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.

De?nition10(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.

De?nition11(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

×···×M S

)×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Σ

, 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. De?nition13(ML-Formulae).Given ML-signatureΣ=(S,O,ρ) and disjoint,countably in?nite 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

|?(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Σ

for the set of formulae of sort S generated from signatureΣ. De?nition14(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 de?ned 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

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

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

from example12,the CL-and ML-satisfaction relations are equal in the following sense.De?ne a translation function ||:P∪K→PΣ

from CL-formulae to ML-formulae overΣC L, by induction on the structure of the CL-formulae such that each case follows the structure of the formulae except that|P1 P2| ¬(|P1| ¬|P2|)and|P1 P2| ¬(|P1| ¬|P2|).We have σ,M,d CL P?σ,MΣ

,d ML|P|

σ,M,c CL K?σ,MΣ

,c ML|K| Recall that not all ML-models over signatureΣCL correspond to CL-models.To get a precise correspondence with CL,we will restrict the class of ML-models to those satisfying a certain set of CL-axioms.We?rst describe the general theory.

De?nition16(AX-Model).Given a ML-signatureΣand a set of axioms AX?PΣ,an AX-model generated fromΣis a ML-model M generated fromΣwhich also satis?esσ,M,m S P for all m∈M S,P∈AX andσ.

2Note that what we call a ML-model is typically called a frame in e.g.[2].

De?nition17(AX-Proof Theory).Given a ML-signatureΣand a set of axioms AX?PΣ,the ML-proof theory3generated by AX consists of the following axioms and rules:

P?Q P P∈AX P tautology

P[P /p]

:(S1,...,S n)→S

n S P()= (p1,...,,...,p n)

P(p i∨p i)?P(p i)∨P(p i)

We sometimes write AX to emphasise the set AX.

There is a well-known general completeness result for ML due to Sahlqvist,which relates the AX-satisfaction relation and the AX-proof theory as long as the axioms have a certain form.We state the result here,since we use it to show completeness for CL.

De?nition18(Very Simple Sahlqvist Formulae).Given ML-signatureΣ=(S,O,ρ),a very simple Sahlqvist antecedent A is a formula given by the grammar:

A::=true S|false

|p S|A∧A| (A1,...,A n)

for p S∈V S and :(S1,...,S n)→S.A very simple Sahlqvist formula is an implication of the form A?P+,where P+is a positive formula,in that every propositional letter p S appears under an even number of negations.

Theorem19(Sahlqvist(see[2])).For every axiom set AX con-sisting of very simple Sahlqvist formulae,the ML-proof theory gen-erated by AX is complete with respect to the class of AX-models.

3.1Context Logic as ML

We have shown that a CL-model can be viewed as a ML-model over signatureΣCL(example12),and that the corresponding sat-isfaction relations agree(example15).Now we identify an axiom set AX CL over signatureΣCL,such that the AX CL-models cor-respond exactly to the CL-models and the proof theories coincide. Since the AX CL-axioms are Sahlqvist axioms,the general com-pleteness result for ML(Theorem19)implies completeness for CL. De?nition20(CL-Axioms).Given ML-signatureΣCL,the axiom set AX CL overΣCL consists of the following formulae,where p,q∈V D and k∈V C:

1.I(p)?p

2.p?I(p)

3.q∧k(p)?True(p∧(k q))

4.q∧k(p)?(k∧(p q))(true)

5.p∧(k q)?True (q∧k(p))

6.k∧(p q)?true (q∧k(p))

The axioms in AX CL are very simple Sahlqvist formulae.The ?rst two axioms correspond directly to the identity axiom of CL. The other axioms capture the relationship between M ap,M ,and M ,which simply permutes elements(Example12).For example, the third axiom species that,if the given data satis?es q and can be split into a context satisfying k and subdata satisfying p,then there exists subdata satisfying p and k q(think of the same subdata).This axiom shifts the emphasis from the given data to the subdata.The?fth axiom is a sort of converse.It states that,if the given data satis?es p and k q,then it is possible to enclose it in a context(actually one satisfying k),such that q and k(p) are satis?ed.The third and?fth axiom together describe the exact connection between M ap and M .Similarly,the fourth and sixth axiom describe the exact connection between M ap and M .

3This is called the normal modal proof theory in[2].

We have already illustrated how a CL-model can be interpreted as a ML-model(Example12).This ML-model is indeed a AXΣ

-model.Conversely,every AXΣ

-model gives rise to a CL-model. Lemma21.

1.Every CL-Model M gives rise to an AX CL-model MΣ

. 2.Every AX CL-model M gives rise to a CL-model M AX

. 3.The CL-model M equals the CL-model(MΣ

)AX

4.The AX CL-model M equals the AX CL-model(M AX

)Σ

5.The satisfaction relations agree.

Proof.Part1follows from Example12by observing that the AX-axioms are satis?ed by MΣ

.The construction of M AX

and the proof of part2is given below.Parts3and4follow from the constructions of the models.Part5is stated in more detail and proved in Example15.For part2,let M be a AX CL-model,with sets M D and M C,and interpretations M ap,M I,M and M . The tuple M AX

=(M D,M C,M ap,M I)is a CL-model.In particular,axioms1and2give the condition that M I is a left unit of M ap.Axioms3to6give the condition(c,d,d )∈M ap?(c,d ,d)∈M ?(d,d ,c)∈M ,which captures exactly the relationship between connectives ap, , .

Finally,we connect the proof theory of CL and AX CL.

Lemma22.Given arbitrary P1,P2∈P and K1,K2∈K,

P1 CL P2iff AX

|P1|?|P2|

K1 CL K2iff AX

|K1|?|K2|

Proof.For simplicity of notation we omit the explicit conversion |P|.The proof consists of two parts:

1.the rules of CL are derivable in AX

;

2.the axioms in AX CL are derivable in CL.

For each part we give one case in detail,the other cases follow similarly.For the?rst part,we show that the following is derivable

K(P1)?P2

K?(P1 P2)

First observe that

K?(P1 P2)iff AX

¬((P1 ¬P2)∧K). Using AX CL-axiom5,we obtain:

K∧(P1 ¬P2)?true (¬P2∧K(P1))

From the assumption AX

K(P1)?P2we have

true (¬P2∧K(P1))?true (¬P2∧P2)

Since AX

true (¬P2∧P2)?false,we have proved

¬((P1 ¬P2)∧K)

For the second part,we show that axiom3is derivable,by proving the following stronger version:

CL q∧k(p)?k(p∧(k q))

Note that,for propositional variable r,we have:

CL k(p)?k(p∧(r∨¬r))?k(p∧r)∨k(p∧¬r)

If we replace r by¬(k q),then our stronger version of axiom3 follows from proving that

CL q∧k(p∧¬(k q))?false

Since CL p∧¬(k q)?¬(k q)and CL¬(k q)?k ¬q by de?nition,we derive

CL q∧k(p∧¬(k q))?q∧k(k ¬q) Finally,since CL k(k ¬q))?¬q,we conclude that

CL q∧k(k ¬q)?q∧¬q?

false

Theorem23(Soundness and Completeness).The proof theory of CL(De?nition5)is sound and complete with respect to the class of CL-models(De?nition2).

Proof.Immediate from Theorem19,using lemmas21and

22.

Using this result,it is also possible to prove completeness for the restricted class of functional CL-models:that is,those CL-models where ap is a function.For each relational model,it is possible to construct a functional model which satis?es the same formulae. This proof is given in Zarfaty’s forthcoming thesis.In[3],we also study CL with an additional zero formula0,since it has interesting logical structure.It is possible to give additional axioms for0,and provide an analogous completeness result.

3.2Bunched Logic as ML

We show how BL can be expressed in ML,by analogy with CL. The ML-signatureΣBL consists of one sort D with the modalities ?:(D,D)→D,0:()→D,??:(D,D)→D and ??:(D,D)→D.The axiom set AX BL is:

1.0?p?p

2.p?0?p

3.(p?q)?r?p?(q?r)

4.p?(q?r)?(p?q)?r

5.q∧(r?p)?true?(p∧(r??q))

6.q∧(r?p)?(r∧(p??q))?true

7.p∧(r??q)?true??(q∧(r?p))

8.r∧(p??q)?true??(q∧(r?p))

The set AX BL is a set of very simple Sahlqvist formulae,and hence we have an analogous completeness result to CL.We do not know how to prove completeness for the functional BL-models, because the construction of a functional model from a relational model does not preserve associativity.

4.Applications of Context Logic

We shall study three applications of CL:heaps to give an example where CL-and BL-reasoning are the same;sequences to give an example where CL-and BL-reasoning is different;trees to provide

a more substantial example where the reasoning is different.

4.1Heaps

CL for heaps is CL extended by speci?c modalities which can be interpreted in the CL-model Heap(Example3).The extra modalities specify the empty heap and heaps containing a speci?c cell.

De?nition24(CL for Heap).CL for heaps,denoted C L Heap,is given by the ML-signatureΣCL+Heap consisting ofΣCL extended by the modalities:

0:()→D,n →m:()→D for every n∈N+and m∈N.The CL-model Heap is a model of C L Heap with the the additional modalities interpreted as:

M0={e}where e denotes the empty heap M n →m={h∈D|h(n)=m}

We have the following derived formulae:

?P1?P2 (0 P1)(P2)specifying that a heap can be split into two disjoint parts,one satisfying P1and the other P2;

?n→m (n →m)∧¬(¬0?¬0)specifying that the given heap h contains just one cell with h(n)=m;

?P1??P2 (0 P1) P2specifying that,whenever a heap satisfying P1can be composed with the given heap,the result satis?es P2.

To illustrate the difference between?and∧,notice that the formula (n→m)?(n→m)is not satis?ed by any heap,whereas the formula(n→m)∧(n→m)speci?es a one-cell heap.Also, notice that logical equivalence of C L Heap is heap equality.This strength of analysis is typical for this style of logical reasoning.

BL for heaps is Separation Logic[11].It is de?ned similarly to C L Heap,by extending the signatureΣBL to include modalities for specifying the existence of heap cells.

De?nition25(BL for Heap).BL for heaps,denoted B L Heap,is given by the ML-signature

ΣBL+Heap=ΣBL∪{n →m:()→D|n∈N+,m∈N}. The BL-model Heap is a model of B L Heap,with the interpretation of the additional modalities de?ned in De?nition24.

Again,we can derive the BL-formula n→m denoting a one-cell heap.In SL,this formula is primitive.We choose n →m as primitive here,because of a comparison with propositional logic given in Section5,where n →m is the natural atomic formula.

From the derived CL-formulae given previously,we know that B L Heap is a sublogic of C L Heap.In fact,there is a collapse of the CL-structure for the heap case,in that C L Heap and B L Heap are equivalent logics on data(Proposition26).This result is strong,in that it implies that the logics are parametrically as expressive as each other on data(De?nition31).

Proposition26.Let PΣ

CL+Heap,V P

denote the restriction of set PΣ

CL+Heap

to those formulae with propositional variables in V P, and similarly for BL.There exists a bijection b:PΣ

CL+Heap,V P

→PΣ

BL+Heap,V P

which preserves the satisfaction relation:that is,

σ,d CL P?σ,d BL b P

σ,c CL K?σ,c(0) BL b K

Proof.The translation is de?ned inductively on the structure of data and context formulae.We give the cases for the modalities:

K(P) b K?b P b I 0

K P b K??b P

P1 P2 c P1??c P2

b0 0

n →m n →m

The proof follows by

induction.

4.2Sequences

CL for sequences generated by alphabet A is CL extended by spe-ci?c modalities which can be interpreted in the CL-model Seq A presented in Example3.The additional modalities specify the empty sequence,sequences with just one element a∈A,and modalities for analysing sequence contexts.

De?nition27(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

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

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

={(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 speci?es 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) P2speci?es that,whenever a sequence sat-isfying property P1is joined to the left of the given sequence,then the result satis?es P2;similarly for P1??P2 (I?P1) P2.For example,the formula a??P speci?es that joining a to the right of the sequence results in a sequence satisfying P.In contrast,notice that the formula(a P)(0)speci?es that,whenever an a is put somewhere in the given sequence,then the result satis?es property P.Again,logical equivalence of C L Seq

is sequence equality. De?nition28(BL for Seq A).BL for sequences generated from

alphabet A,denoted B L Seq

,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 de?ned as given in De?nition27.

B L Seq

A is a sublogic of C L Seq

.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

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

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

without the modality

is parametrically as expressive as B L Seq

4.3Trees

CL for trees generated by alphabet A is CL extended by speci?c 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.

De?nition29(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

quanti?cation 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.

De?nition30(BL for T ree A).BL for trees generated from

alphabet A,denoted B L T ree

,is given by the ML-signature

ΣBL+T ree

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

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

is a sublogic of C L T ree

.The BL-formulaµ[P]

speci?es a tree with top node described byµ.It is derivable in

C L T ree

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 node.In C L T ree

,this can be expressed as

¬(¬I(¬0))∧¬0.It is expressed in B L T ree

as a[0]∨a⊥[0],and

is not expressible without the a⊥modality.The BL-formula bµ[P]

is the adjoint.It speci?es that,whenever a top node is added to the

given tree with label speci?ed byµ,the resulting tree satis?es P.

It corresponds to the CL-formulaµ[I] P.AL has the formula

b a[P],with

c a⊥[P]derivable using existential quanti?cation and

label equality.The BL-formula (P)denotes that there is a subtree

satisfying P.Recall that this is expressible in CL as True(P).

Finally,the BL-formula b (P)is the corresponding adjoint.It states

that the given tree can be put in a context such that the result

satis?es P,and is expressible in CL as True P.AL has the

formulae (P),but surprisingly not the corresponding adjoint.We

will see that b plays an important role in an expressivity result

linking BL-and CL-reasoning without (Theorem40).

Just as for sequences,the CL-reasoning does not collapse for

trees,and the comparison between C L T ree

and B L T ree

is sub-

tle.Consider the CL-formula(0 b[0])(a[true]),which speci?es

that we can remove a subtree with root label a to obtain a tree with

one node labelled b.It corresponds to the BL-formula a[true]?b[0]∨

b[a[true]].Now consider the CL-formula(0 b[true])(a[true]).

It corresponds to the BL-formula (b[ a[true]])∨ ( (b[true])?

(a[true])).Notice that the structure of the CL-formulae is sim-

ilar,but the structure of the derivable BL-formulae is quite dif-

ferent.In Section5.3,we shall see that C L T ree

and B L T ree

are not parametrically as expressive,in the sense that CL-formula

(0 p)(a[true])cannot be expressed in B L T ree

.C L T ree

with-

out the modality is as expressive as B L T ree

5.Parametric Expressivity

We present our expressivity results.We prove parametric inexpres-sivity results comparing BL for heaps with and without the struc-tural connectives,using a direct proof method.We prove strong inexpressivity results for speci?c interpretations σ,corresponding to the extension of BL with list predicates.We also study para-metric inexpressivity results comparing CL and BL for sequences and trees.We cannot prove the parametric results directly for these applications.Instead,we prove strong inexpressivity results,and hence by implication the parametric results.In addition,we study BL for bounded heaps,presenting logics which have the same strong expressivity for every interpretation σ,but different para-metric expressivity.

First some notation.Given ML-signature Σ=(S ,O,ρ)and AX-model M Σ,we let L M Σ,V denote the modal logic determined by Σand M Σwith propositional variables in V .We use L M Σ,V S to denote the restriction to propositional variables of sort S ,and L M Σ,{p }for the restriction to propositional variable p .We write L M Σ,V (? )for the logic without modality .For example,C L Seq A ,V D (?{ })denotes C L Seq A without modality and with the propositional variables restricted to sort D.

De?nition 31(Parametric Expressivity).Let Σ=(S ,O,ρ)and Σ =(S ,O ,ρ )be two ML-signatures with sort S ∈S ∩S .Consider two models M ,M over the respective signatures such that M S =M S .Consider the logics L M ,V S and L M ,V S .1.Logic L M ,V S is as expressive as L M ,V S with respect to sort S ,written L M ,V S ?S L M ,V S ,if and only if ?P ∈L M ,V S .?P ∈L M ,V S .?σ.?m ∈M S .

σ,M ,m S P ?σ,M ,m S P .

We often write L M ,V S ?L M ,V S since the sort S is apparent.2.Given σ,logic L M ,V S is as σ-expressive as L M ,V S with respect to sort S ,written L M ,V S ?S,σL M ,V S ,if and only if ?P ∈L M ,V S .?P ∈L M ,V S .?m ∈M S .

σ,M ,m S P ?σ,M ,m S P .

Again,we write L M ,V S ?σL M ,V S since S is apparent.We write L M ,V S =L M ,V S when L M ,V S ?L M ,V S and L M ,V S ?L M ,V S ,and L M ,V S =σL M ,V S analogously.In fact,we concentrate on inexpressivity results,asking when a logic is strictly more expressive than another.We say that L M ,V S is parametrically more expressive than L M ,V S iff L M ,V S L M ,V S .We say that L M ,V S is strongly more expressive than L M ,V S iff there exists a σsuch that L M ,V S σL M ,V S .

To prove our strong inexpressivity results we rely heavily on the notion of bisimulation.Bisimulation has the property that,if two elements of the models are bisimilar,then they cannot be dis-tinguished from each other in the logic,and hence can be directly used to prove strong inexpressivity.

De?nition 32(Bisimulation).A symmetric binary relation ～=S

S ∈S ～S with ～S ?M S ×M S is a bisimulation for ML-model M Σif and only if,whenever ((m 1,...,m n ),m )∈M ?and

m ～m ,then there exist m i ∈M S i such that m i ～S i m

for i =1...n and ((m 1,...,m n ),m

)∈M ?.A bisimulation ～is compatible with interpretation σif and only if,for all m,p ,m ∈σ(p )∧m ～m ?m ∈σ(p ).

Proposition 33.Let ～be a bisimulation compatible with σfor ML-model M Σ.Then m 1～S m 2implies σ,M ,m 1 S P iff σ,M ,m 2 S P for all P ∈P ΣS .

To show that L M ,V S σL M ,V S ,our proof method consists of ?nding a formula P ∈L M ,V S of sort S and a bisimulation ～for M compatible with σ,such that P distinguishes two elements

which are identi?ed by ～.Inexpressivity then follows from Propo-sition 33that no formula in P Σcan distinguish the two elements.5.1

Heaps

We have the following results about heaps:

?B L Heap,V D =C L Heap,V D

?B L Heap,?(?{??}+{n →?})=B L Heap,??B L Heap,{p }(?{??}+{n →?}) B L Heap,{p }

The ?rst result is a parametric expressivity result,showing that the structure of CL collapses to BL in the heap case.This result follows from Proposition 26.The second result is a non-parametric expres-sivity result due to Lozes [9],which compares the expressivity of closed formulae.It states that the adjunct ??can be eliminated if we add formulae n →?to specify that address n is allocated:n →?speci?es that there exists m such that n →m .It is expressible using ??as ¬((n →0)??true );the current heap cannot be extended with cell n ,so n must already be allocated.Lozes’result was initially quite a surprise,since the adjuncts are used in an essential way to describe the weakest preconditions for Hoare reasoning based on BL for heaps.We address this apparent contradiction here,by proving the third result.

The third result is a parametric inexpressivity result,which we prove by showing that formula (n →0)??p cannot be expressed in BL for heaps without ??.This formula is interesting because it expresses the weakest precondition of allocation.This inexpres-sivity result says nothing about whether the formula is expressible for a particular interpretation of p .By Lozes’results,we know that it is expressible for every interpretation of p as a closed formula.We also prove a strong inexpressivity result using the same formula and a natural interpretation σlist which interprets p as list (m ):that is,the heap contains a 0-terminated linked list starting at m .This result is interesting because lists are one of the typical inductive predicates used in BL-reasoning.Theorem 34(Parametric Inexpressivity).

B L Heap,{p }(?{??}+{n →?}) B L Heap,{p }

Proof.We de?ne the notion of heap-reducing formulae,and prove that all the formulae in B L Heap,{p }(?{??}+{n →?})are heap-reducing,whereas formula (n →0)??p is not.This captures our intuition is that,without ??,the BL-modalities either leave the heap alone or make it smaller,whereas formula (n →0)??p crucially tests p on an extension of the initial heap with cell n .

Given heap h ,de?ne a binary relation on interpretations by

σ～h σ iff ?h ≤h.h ∈σ(p )?h ∈σ (p )

where h ≤h means dom (h )?dom (h )and ?n ∈dom (h ).h (n )=h (n ).We say that a formula P is heap-reducing if and only if,whenever σ～h σ ,it follows that σ,h |=P ?σ ,h |=P .Given formula P in B L Heap,{p }(?{??}+{n →?}),we show that P is heap-reducing by induction on the structure of P .Case p is immediate from the de?nition of σ～h σ .The only other interesting case is P 1?P 2.Suppose σ～h σ and σ,h |=P 1?P 2.There exists h i for i =1,2such that h =h 1·h 2and σ,h i |=P i .Since h i ≤h ,we have σ～h i σ for i =1,2and hence σ ,h i |=P i by the induction hypothesis.We conclude that σ ,h |=P .

Let P be (n →0)??p .We show that P is not heap-reducing.De?ne σ(p )={h |h :N + fin N }and σ (p )={e }where e is the empty heap.Then σ～e σ and σ,e |=P ,but σ ,e |=P .We now prove our strong inexpressivity result,that ??cannot be eliminated with interpretation σlist (p )=list (m ).With this interpretation,the formula (n →0)??p is satis?ed by a list segment

starting at m and stopping with dangling pointer n.This cannot be expressed without??,since only whole lists can be observed. Theorem35(Strong Inexpressivity).

B L Heap,{p}(?{??}+{n →?}) σ

list

B L Heap,{p}

Proof.Consider the BL-formula P (n→0)??p,and interpre-tationσlist(p)=list(m)for m=n.We show that there is no formula P in B L Heap,{p}(?{??}+{n →?})that is equivalent to P usingσlist.Expecting a contradiction,suppose that such a P exists,and let L?N be the?nite number of constants mentioned in P .Consider the restriction of B L Heap to constants in L,written

B L Heap

L .We choose a bisimulation～which identi?es two heaps

when they have the same domain,coincide on values in L,and are identical if one of them contains a list starting at m:

h1～h2iff dom(h1)=dom(h2)and

?i,j∈L.h1(i)=j iff h2(i)=j and

if h1|=list(m)or h2|=list(m)then h1=h2. Notice thatσlist(p)is compatible with～,since if h1～h2and h1|=list(m)then h2|=list(m).Assume for the moment that ～is indeed a bisimulation.With this assumption,we show that we do indeed obtain a contradiction.Take m /∈L∪{n,m}and consider the heaps h1=[m→m ,m →n]and h2=[m→m ,m →m ].Note that h1～h2andσ,h1|=(n→0)??p butσ,h2|=(n→0)??p.Assuming that～is a bisimulation

for B L Heap

L,{p}(?{??}+{n →?}),Proposition33implies that

σlist,h1|=BL P iffσlist,h2|=BL P .We have therefore proved that there cannot be a BL-formula P which is equivalent to P.

Finally,we must prove our assumption that～is a bisimulation for the modalities{0,?}∪{i →j,i →?|i,j∈L}.We only look at the?modality;the other cases are trivial.Assume h1=h 1·h 1 and h1～h2.We must show that?h 2,h 2such that h2=h 2·h 2 and h 1～h 2and h 1～h 2.Choose h 2,h 2as the unique splitting of h2such that dom(h 2)=dom(h 1)and dom(h 2)=dom(h 1).We show h 1～h 2;the case h 1～h 2is identical by symmetry.The?rst and second conditions in the de?nition of～are immediate.For the third condition,assume h 1|=list(m),which implies h1|=list(m) since h 1is a sublist of h1.By de?nition of h1～h2,we have h1=h2,hence h 1=h 2which is the desired conclusion.

Lozes also shows that,with an additional modality size r for determining the size of heaps,the?-modality can be removed.We show that?is essential for parametric reasoning.The results are:?B L Heap,?(?{?,??}+{size r})=B L Heap,?(?{??})

?B L Heap,{p,q}(?{?,??}+{size r}) B L Heap,{p,q}(?{??}). The results also hold with modality n →?.Thus,BL is as ex-pressive as PL with atomic formulae0,size r and n →?,but not parametrically so.We believe this parametric inexpressivity result demonstrates what has been always known intuitively,but by ex-ample only,that the?-modality is essential for modular reasoning.

We give a direct proof of our parametric inexpressivity result for?based on the trivial observation that,without?and??,all the modalities leave the current heap unchanged.The modality size r, for each r∈N+,is interpreted by h|=size r iff|dom(h)|≤r. We do not require size0as it corresponds to the zero formula0. Theorem36(Parametric Inexpressivity).

B L Heap,{p,q}(?{?,??}+{size r}) B L Heap,{p,q}(?{??}) Proof.The proof is analogous to that of Thm.34.A formula P is heap-invariant iff,when h∈σ(p)?h∈σ (p)for all p,then σ,h|=P?σ ,h|=P.The formulae in B L Heap,{p,q}(?{?,??}+ {size r})are heap-invariant,but p?q is not.We also prove a second strong inexpressivity result,that?cannot be eliminated with?xed interpretationσlist,which interprets p and q as list(m1)and list(m2)respectively for m1=m2.The?modality is essential for specifying the property that the two lists are in the heap and their tails never meet.

Theorem37(Strong Inexpressivity).

B L Heap,{p,q}(?{?,??}+{size r}) σ

l ist

B L Heap,{p,q}(?{??}) Proof.The structure of the proof is analogous to Theorem35. Consider the BL-formula p?q.As in Theorem35,we restrict our attention to BL-formulae mentioning at most a?nite set L?N of constants and the propositional variables p,q.

Consider the interpretation h∈σlist(p)iff h satis?es list(m1), and h∈σlist(q)iff h satis?es list(m2).De?ne relation～by: h1～h2iff|dom(h1)|=|dom(h2)|and

σ,h1|=P?σ,h2|=P for

P∈{p,q}∪{i →j|i,j∈L}

～is compatible withσand is a bisimulation for the modalities {0,size r}∪{i →j|i,j∈L}.Take h1=[m1→n ,m2→n ,n →0,n →0]and h2=[m1→n ,m2→n ,n →0,n →0]for distinct n ,n /∈L∪{m1,m2}.Then h1～h2 andσ,h1|=p?q,butσ,h2|=p?q.

From the previous examples,one might be tempted to conclude that whenever a parametric inexpressivity result holds,a corresponding strong inexpressivity result holds too.In fact,this is not the case as we demonstrate using bounded heaps.In bounded heaps,??cannot be eliminated parametrically for reasons identical to the unbounded case.However,given a speci?c interpretationσ,any formula is equivalent to a disjunction of characteristic formulae without??. Theorem38.Let Heap k denote the restriction of heaps,and correspondingly formulae,to locations≤k.The following hold: 1.B L Heap

k,{p}

(?{??}+{n →?}) B L Heap

k,{p}

2.B L Heap

k,{p}

(?{??}+{n →?})=σB L Heap

k,{p}

for allσ. Proof.The proof of part1is identical to the proof of The-orem34.For part2,we in fact prove a stronger claim:for any set of heaps H?Heap k,there exists a formula P H∈B L Heap

k,?

(?{0,?,??})such that h|=P H?h∈H.We show that the conclusion then follows from the claim.Given any σand P∈B L Heap

k,{p}

,let H={h|σ,h|=P}.Then P is equivalent to P H,by de?nition.To prove the claim,we?rst de?ne, given heap h,the characteristic formula P h as

n,m≤k.h(n)=m

n →m∧

n,m≤k.h(n)=m)

¬(n →m)

Clearly h |=P h?h=h ,and P h∈B L Heap

k,?

(?{0,?,??}). To conclude,we de?ne P H=

h∈H

P h.

5.2Sequences

We have the following results for sequences for alphabet A:

?B L Seq

A,?

(?{??,??})=B L Seq

A,?

=C L Seq

A,?

?B L Seq

A,V D

(?{??,??})=C L Seq

A,V D

(?{ , })

?B L Seq

A,V D

=C L Seq

A,V D

(?{ })

?B L Seq

A,{p}

C L Seq

A,{p}

if A is in?nite.

The?rst result is a standard expressivity result showing that BL and CL for sequences without propositional variables are equally expressive.The proof will appear in a forthcoming paper.The sec-ond result is a parametric expressivity result.It shows that,without adjuncts,BL for sequences is as expressive as CL for sequences.

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.

Our?rst parametric expressivity result for sequences shows that,without adjuncts,CL-application can be speci?ed 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 de?ne 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,?rst 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 de?ne 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 de?ned below by induction on the structure of the canonical formulae.

Before de?ning Not,we de?ne a function And on canonical

formulae such that And(K

1,K

)is equivalent to K

∧K

And(K

1∨K

) And(K

)∨And(K

)

And(P1?I?P2,P3?I?P4) (P1∧P3)?I?(P2∧P4) We now de?ne function Not:

Not(K

1∨K

) And(Not(K

),Not(K

))

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

(2)is proved by induction on K.For case K

1∨K

,note that

1∨K

)(P)is equivalent to K

(P)∨K

(P)and,by the

induction hypothesis,it is equivalent to K

1[P/I]∨K

[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)satis?ed 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 satis?ed 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 de?ne 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,?rst 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

∨K

,then(K

∨K

) P is equivalent to

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 in?nite 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 the?nite 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 observe subsequences obtained by removing letters from either side,not from the middle.With BL, we can only compare adjacent pairs of elements.With CL,we can compare arbitrary pairs of elements.We must?nd an interpretation functionσ,and a bisimulation relation～which is compatible with σand captures this intuitive difference in expressivity.

We choose an interpretationσwhich states that the interpreta-tion of p is the set of all sequences with equal elements.To express this formally,we?rst introduce some notation.Letα,βdenote se-quences,letαi denote the i-th element of sequenceα,and let|α| denote the length of the sequence.We de?neσby

σ(p) {α|?i∈1..|α|?1.αi=αi+1}

In addition,we de?ne a bisimulation relation which observes ele-ments in the set A and equality of adjacent elements:α～βiff?n.|α|=|β|=n∧

?i∈1...n?1.αi=αi+1?βi=βi+1∧

?i∈1...n,a ∈A .αi=a ?βi=a Clearly～is compatible withσ.Assume for the moment that it is indeed a BL-bisimulation.With this assumption,we prove

the inexpressivity result we seek.Consider two sequences α1=a ·a ·a and α2=a ·a ·a ,where a =a are not in A .Observe that α1～α2,as adjacent letters are distinct in both sequences,σ,α1|=(0 p )(a )but σ,α2|=(0 p )(a ).Assuming ～is a bisimulation for B L Seq A ,{p },Proposition 33implies that σ,α1|=BL P iff σ,α2|=BL P for all BL-formulae P .We have therefore proved that there cannot be a BL-formula P which is equivalent to P .Note that our proof depends on A being an in?nite set,since we need to pick new elements a and a not in A .

Finally,we must show that ～is indeed a bisimulation for all the modalities of B L Seq A ,{p }.We only look at the ?and ??modalities;the other cases are analogous or trivial.For the ?modality,assume α·β=γand γ～γ .We must show that ?α ,β such that α ·β =γ and α～α and β～β .Choose α ,β as the unique splitting of γ such that |α |=|α|and |β |=|β|.Clearly α～α and β～β ,since adjacent elements in α and β are also adjacent in γ .For the ??modality,assume α·β=γand α～α .We need to show that ?β ,γ such that α ·β =γ and β～β and γ～γ .Since αand α might end in different letters,we must construct a β such that its ?rst element relates to the last element of α in the same way as the ?rst element of βrelates to the last

element of α.Let f :A →A be a bijection such that f (αi )=α i

.Such an f exists since α～α .We de?ne β

as the unique sequence

such that |β |=|β|,β

=f (βi )and γ α ·β .It is easy to see that β～β and γ～γ .5.3

Trees

We have the following results for trees for alphabet A :

?B L T ree A ,V D (?{??,b µ,b })=C L T ree A ,V D (?{ , })?B L T ree A ,V D =C L T ree A ,V D (?{ })?B L T ree A ,{p } C L T ree A ,{p }if A is in?nite.

The ?rst result states that CL and BL for trees without adjoints have the same parametric expressive power.The second result states that adding the modality to CL gives the same expressivity as BL.This formalises our intuition that the modality is a compact way to express the adjoints of AL (plus ? ).The third result is a para-metric inexpressivity result,showing that CL for trees is parametri-cally more expressive than BL for trees.This result illustrates that is the key modality for giving CL its additional expressive power.In [3],we observed that it was important for expressing the weak-est preconditions of update commands.Our inexpressivity result formalises this intuition,which we had previously motivated by ex-ample.

Our ?rst parametric expressivity result is that BL and CL for trees without adjoints are equally expressive.The proof shows that context formulae can be reduced to a canonical form,allowing con-text application to be eliminated by a form of syntactic substitution.Theorem 42(Parametric Expressivity).

B L T ree A ,V D (?{??,b µ,b })=

C L T ree A ,V

D (?{ , })Proof.Note that propositional variables are restricted to sort D,so the context formulae of C L T ree A ,V D (?{ , })are:

K ::=I |K ∨K |¬K |False |µ[K ]|P ?K We de?ne a canonical subset,similar to that given in Theorem 39:

K ::=K ∨K |True |False |P ?I |P ?η[K ]η

::=

{a 1,...,a n }|{a 1,...,a n }⊥

The composition formulae analyse whether the hole is at the top level or under a node label.The formulae {a 1,...,a n }[K ]and {a 1,...,a n }⊥

[K ]are syntactic sugar for W i a i [K ]and V i a ⊥i [K ]respectively.Just as for Theorem 39,it is enough to show the following results:

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

(2)every application K (P )is equivalent to the substitution for-mula K [P/I, P/True ].To prove (1),we de?ne a translation tr from context formulae to the canonical subset by:

tr (I )

0?I

tr (K 1∨K 2)

tr (K 1)∨tr (K 2)tr (¬K ) Not (tr (K ))tr (False ) False

tr (µ[K ]) 0?µ[tr (K )]tr (P ?K )

Add (P,tr (K ))

where Not (K )and Add (P,K )are de?ned by induction on the structure of the canonical formulae.

Before de?ning Not ,we de?ne 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 (True ,K ) K And (False ,K ) False

And (P 1?I,P 2?I ) (P 1∧P 2)?I And (P 1?I,P 2?η[K ]) False And (P 1?η1[K 1],P 2?η2[K 2])

(P 1∧P 2)?(η1∧η2)[And (K 1,K 2)]

where,for sets S i ,we de?ne S 1∧S 2=S 1∩S 2,S 1∧S ⊥

=S 1?S 2,and S ⊥1∧S ⊥2=(S 1∪S 2)⊥

.We now de?ne the function Not such that Not (K )is equivalent to ¬(K ):

Not (K 1∨K 2)

And (Not (K 1),Not (K 2))Not (True ) False Not (False ) True

Not (P ?I ) (¬P )?I ∨true ??⊥[True ]Not (P ?η[K ])

true ?I ∨true ?η⊥[True ]∨

(¬P )?η[True ]∨true ?η[Not (K )]We ?nally de?ne Add such that Add (P,K )is equivalent to P ?K :Add (P,K 1∨K 2)

Add (P,K 1)∨Add (P,K 2)

Add (P,True ) (P ?true )?I ∨(P ?true )??⊥[True ]Add (P,False ) False

Add (P 1,P 2?I ) (P 1?P 2)?I Add (P 1,P 2?η[K ])

(P 1?P 2)?η[K ]

To prove (2),we proceed 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 hence,by induction,is equivalent to K 1[P/I, P/True ]∨K 2[P/I, P/True ].For case True,observe that True (P )is equiv-alent to P .Case False is immediate.Case P 1?I is also im-mediate since (P 1?I )(P 2)is equivalent to P 1?P 2.For case P 1?η[K ],?rst observe that (P 1?η[K ])(P 2)is equivalent to P 1?η[K (P 2)]which,by the induction hypothesis,is equivalent to (P 1?η[K [P 2/I, P/True ]]).

Consider CL formula (¬I )(P ),satis?ed by any tree hav-ing a strictly smaller subtree satisfying P .We have tr (¬I )=Not (tr (I ))=Not (0?I )=(¬0)?I ∨true ??⊥[True ].Therefore (¬I )(P )is equivalent to (¬0)?P ∨true ??⊥[ P ],satis?ed by any tree with either a subtree satisfying P at the top level composed with a non-empty tree,or a subtree satisfying P under a tree node.Our second parametric expressivity result for trees shows that CL for trees minus corresponds to BL.Theorem 43(Parametric Expressivity).

B L T ree A ,V D =

C L T ree A ,V

D (?{ })

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

we have(K

1∨K

) P equivalent to(K

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 a?xed number of edges usingµ. Theorem44(Parametric Inexpressivity).Let A be an in?nite 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 satis?es 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 a?nite set A ?A.We de?ne 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 de?ne 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

de?nition 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 de?nition 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 quanti?cation and?rst-order quanti?cation.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 without?rst-order quanti?cation,whereas their applications to analysing trees and heaps usually involve quanti?cation over node labels and heap addresses.Dawar,Gardner and Ghelli(with thanks to Yang)have shown that adjunct-elimination in AL with quan-ti?cation 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 down exactly why full SL seems to be more appropriate for modular reasoning about programs than?rst-order logic. Acknowledgments We would like to thank Peter O’Hearn for his insightful comments.This work was supported by EPSRC. References

[1]J.Berdine,C.Calcagno,and P.W.O’Hearn.Smallfoot:Modular

automatic assertion checking with separation logic.In Proceedings of FMCO’05,volume4111of LNCS,2006.

[2]Patrick Blackburn,Maarten de Rijke,and Yde Venema.Modal Logic.

Cambridge University Press,2001.

[3]C.Calcagno,P.Gardner,and U.Zarfaty.Context logic and tree

update.In POPL,2005.

[4]L.Cardelli and G.Ghelli.TQL:A query language for semistructured

data based on the ambient logic.To appear in MSCS.

[5]L.Cardelli and A.Gordon.Anytime,anywhere:Modal logics for

mobile ambients.In POPL,2000.

[6]A.Dawar,P.Gardner,and G.Ghelli.Adjunct elimination using

Enrenfeuch’s games.In FSTTCS,2004.