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

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

Since CL p∧¬(k q)⇒¬(k q)and CL¬(k q)⇔k ¬q by definition,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(Definition5)is sound and complete with respect to the class of CL-models(Definition2).

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 satisfies 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 specific modalities which can be interpreted in the CL-model Heap(Example3).The extra modalities specify the empty heap and heaps containing a specific cell.

Definition24(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 satisfies P2.

To illustrate the difference between◦and∧,notice that the formula (n→m)◦(n→m)is not satisfied by any heap,whereas the formula(n→m)∧(n→m)specifies 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 defined similarly to C L Heap,by extending the signatureΣBL to include modalities for specifying the existence of heap cells.

Definition25(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 defined in Definition24.

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(Definition31).

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 defined 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-cific 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.