key: cord-0054940-va3x3t5z
authors: Polzer, Miriam; Goncharov, Sergey
title: Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store
date: 2020-04-17
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-45231-5_28
sha: 1365e865e6d3a67b74fac4b3982ef75210f5fce3
doc_id: 54940
cord_uid: va3x3t5z

Modelling and reasoning about dynamic memory allocation is one of the well-established strands of theoretical computer science, which is particularly well-known as a source of notorious challenges in semantics, reasoning, and proof theory. We capitalize on recent progress on categorical semantics of full ground store, in terms of a full ground store monad, to build a corresponding semantics of a higher order logic over the corresponding programs. Our main result is a construction of an (intuitionistic) BI-hyperdoctrine, which is arguably the semantic core of higher order logic over local store. Although we have made an extensive use of the existing generic tools, certain principled changes had to be made to enable the desired construction: while the original monad works over total heaps (to disable dangling pointers), our version involves partial heaps (heaplets) to enable compositional reasoning using separating conjunction. Another remarkable feature of our construction is that, in contrast to the existing generic approaches, our BI-algebra does not directly stem from an internal categorical partial commutative monoid.

Modelling and reasoning about dynamic memory allocation is a sophisticated subject in denotational semantics with a long history (e.g. [19, 15, 14, 16] ). Denotational models for dynamic references vary over a large spectrum, and in fact, in two dimensions: depending on the expressivity of the features being modelled (ground store -full ground store -higher order store) and depending on the amount of intensional information included in the model (intensionalextensional ), using the terminology of Abramsky [1] .

Recently, Kammar et al [9] constructed an extensional monad-based denotational model of the full ground store, i.e. permitting not only memory allocation for discrete values, but also storing mutually linked data. The key idea of the latter work is an explicit delineation between the target presheaf category rW, Sets on which the full ground store monad acts, and an auxiliary presheaf category rE, Sets of initializations, naturally hosting a heap functor H. The latter category also hosts a hiding monad P , which can be loosely understood as a semantic mechanism for idealized garbage collection. The full ground store monad is then assembled according to the scheme given in Fig. 1 . As a slogan: the local store monad is a global store monad transform of the hiding monad sandwiched within a geometric morphism. The fundamental reason, why extensional models of local store involve intricate constructions, such as presheaf categories is that the desirable program equalities include let : new v; 1 : new w in p " let 1 : new w; : new v in p p ı 1 q let : new v in ret ‹ " ret ‹ let : new v in pif " 1 then true else falseq " false p ı 1 q and these jointly do not have set-based models over countably infinite sets of locations [23, Proposition 6] . The first equation expresses irrelevance of the memory allocation order, the second expresses the fact that an unused cell is always garbage collected and the third guarantees that allocation of a fresh cell does indeed produce a cell different from any other. The aforementioned construction validates these equations and enjoys further pleasant properties, e.g. soundness and adequacy of a higher order language with user defined storable data structures. The goal of our present work is to complement the semantics of programs over local store with a corresponding principled semantics of higher order logic. In order to be able to specify and reason modularly about local store, more specifically, we seek a model of higher order separation logic [21] . It has been convincingly argued in previous work on categorical models of separation logic [2, 3] that a core abstraction device unifying such models is a notion of BI-hyperdoctrine, extending Lawvere's hyperdoctrines [10] , which provide a corresponding abstraction for the first order logic. BI-hyperdoctrines are standardly built on BI-algebras, which are also standardly constructed from partial commutative monoids (pcm), or more generally from resource algebras as in the Iris state of the art advanced framework for higher order separation logic [8] . One subtlety our construction reveals is that it does not seem to be possible to obtain a BI-algebra following general recipes from a pcm (or a resource algebra), due to the inherent local nature of the storage model, which does not allow one to canonically map store contents into a global address space. Another subtlety is that the devised logic is necessarily non-classical, which is intuitively explained by the fact that the semantics of programs must be suitably irrelevant to garbage collection, and in our case this follows from entirely formal considerations (Yoneda lemma). It is also worth mentioning that for this reason the logical theory that we obtain is incompatible with the standard (classical or intuitionistic) predicate logic. E.g. the formula D . Ñ 5 is always valid in our setup, which expresses the fact that a heap potentially contains a cell equal to 5 (which need not be reachable) -this is in accord with the second equation above -and correspondingly, the formula @ . p Ñ 5q is unsatisfiable. This and other similar phenomena are explained by the fact that our semantics essentially behaves as a Kripke semantics along two orthogonal axes: (proof relevant) cell allocation and (proof irrelevant) cell accessibility. While the latter captures a programming view of locality, the latter captures a reasoning view of locality, and as we argue (e.g. Example 26), they are generally mutually irreducible.

Related previous work As we already pointed out, we take inspiration from the recent categorical approaches to modelling program semantics for dynamic references [9] , as well as from higher order separation logic semantic frameworks [2] . Conceptually, the problem of combining separation logic with garbage collection mechanisms goes back to Reynolds [20] , who indicated that standard semantics of separation logic in not compatible with garbage collection, which we also reinforce with our construction. Calcagno et al [4] addressed this issue by providing two models. The first model is based on total heaps, featuring the aforementioned effect of "potential" allocations. To cope with heap separation the authors introduced another model based on partial heaps, in which this effect again disappears, and has to be compensated by syntactic restrictions on the assertion language.

Plan of the paper After preliminaries (Section 2), we give a modified presentation of a call-by-value language with full ground references and the full ground store monad (Sections 3 and 4) following the lines of [9] . In Section 5 we provide some general results for constructing semantics of higher order separation logics. The main development starts in Section 6 where we provide a construction of a BI-hyperdoctrine. We show some example illustrating our semantics in Section 7 and draw conclusions in Section 8.

We assume basic familiarity with the elementary concepts of category theory [12, 6] , all the way up to monads, toposes, (co)ends and Kan extensions. We denote by |C| the class of objects of a category C; we often suppress subscripts of natural transformation components if no confusion arises.

In this paper, we work with special kinds of covariant presheaf toposes, i.e. functor categories of the form rC, Sets, where C is small and satisfies the following amalgamation condition: for any f : a Ñ b and g : a Ñ c there exist g 1 : b Ñ d and f 1 : c Ñ d such that f 1˝g " g 1˝f . Such toposes are particularly well-behaved, and fall into the more general class of De Morgan toposes [7] . As presheaf toposes, De Morgan toposes are precisely characterized by the condition that 2 " 1`1 is a retract of the subobject classifier Ω. More specifically, our C support further useful structure, in particular, a strict monoidal tensor ' with jointly epic injections in 1 , in 2 , forming an independent coproduct structure, as recently identified by Simpson [22] . Moreover, if the coslices c Ñ C support independent products, we obtain local independent coproducts in C, which are essentially cospans

Given ρ 1 : c Ñ c 1 and ρ 2 : c Ñ c 2 , we thus always have ρ 1 ‚ ρ 2 : c 1 Ñ c 1 ' c c 2 and ρ 2 ‚ ρ 1 : S 2 Ñ c 1 ' c c 2 , such that pρ 1 ‚ ρ 2 q˝ρ 1 " pρ 2 ‚ ρ 1 q˝ρ 2 , and as a consequence, rC, Sets is a De Morgan topos. Intuitively, the category C represents worlds in the sense of possible world semantics [15, 19] . A morphism ρ : a Ñ b witnesses the fact that b is a future world w.r.t. a. Existence of local independent products intuitively ensures that diverse futures of a given world can eventually be unified in a canonical way.

Every functor f : C Ñ D induces a functor f ‹ : rD, Sets Ñ rC, Sets by precomposition with f. By general considerations, there is a right adjoint f ‹ : rC, Sets Ñ rD, Sets, computed as Ran f , the right Kan extension along f. This renders the adjunction f ‹ % f ‹ , as a geometric morphism, in particular, f ‹ preserves all finite limits.

To set the context, we consider the following higher order language of programs with local references by slightly adapting the language of Kammar et al [9] to match with the fine-grain call-by-value perspective [11] . This allows us to formally distinguish pure and effectful judgements. First, we postulate a collection of cell sorts S and then introduce further types with the grammar:

A type is first order if it does not involve the function type constructors A Ñ B.

We then fix a map CType, assigning a first order type to every given sort from S. We show three term formation rules over these data in Fig. 2 specific to local store.

Here the v-indices at the turnstiles indicate values and the c-indices indicate computations. In (put) the cell referenced by is updated with a value v, (get) returns a value under the reference and (new) simultaneously allocates new cells filled with the values v 1 , . . . , v n and makes them accessible in p under the corresponding references 1 , . . . , n . A fine-grain call-by-value language is interpreted standardly in a category with a monad, which in our case must additionally provide a semantics to the rules (put), (get) and (new). We present this monad in detail in the next section.

Example 1 (Doubly Linked Lists). Let S " {DLList} and let CTypepDLListq " 2ˆpRef DLList`1 qˆpRef DLList`1 q, which indicates that a list element is a Boolean (i.e. an element of 2 " 1`1) and two pointers (forwards and backwards) to list elements, each of which may be missing. Note that we thus avoid empty lists and null-pointers: every list contains at least one element, and the elements added by`1 cannot be dereferenced. This example provides a suitable illustration for the letref construct. E.g. the program

simultaneously creates two list elements pointing to each other and returns a reference to the first one.

We proceed to present the full ground store monad by slightly tweaking the original construction [9] towards higher generality. The main distinction is that we do not recur to any specific program syntax and proceed in a completely axiomatic manner in terms of functors and natural transformations. This mainly serves the purpose of developing our logic in Section 6, which will require a coherent upgrade of the present model. Besides this, in this section we demonstrate flexibility of our formulation by showing that it also instantiates to the model previously developed by Plotkin and Power [16] (Theorem 8).

Our present formalization is parametric in three aspects: the set of sorts S, the set of locations L and a map range, introduced below for interpreting S. We assume that L is canonically isomorphic to the set of natural numbers N under # : L -N. Using this isomorphism, we commonly use the "shift of P L by n P N", defined as follows: `n " # -1 p# `nq.

Heap layouts and abstract heap(let)s Let W be a category of (heap) layouts and injections defined as follows: an object w P |W| is a finitely supported partial function w : L á fin S and a morphism ρ : w Ñ w 1 is a type preserving injection ρ : dom w Ñ dom w 1 , i.e. for all l P img w, wp q " w 1 pρp qq. We will equivalently view w as a left-unique subset of LˆS and hence use the notation p : Sq P w as an equivalent of wp q " S. Injections ρ : w Ñ w 1 with the property that wp : Sq " : S for all p : Sq P w we also call inclusions and write w Ď w 1 instead of ρ : w Ñ w 1 , for obviously there is at most one inclusion from w to w 1 . If w Ď w 1 then we call w a sublayout of w 1 . We next postulate range : S Ñ rW, Sets.

The idea is, given a sort S P S and a heap layout w P |W|, rangepSqpwq yields the set of possible values for cells of type S over w.

Example 2. Assuming the grammar (1) and a corresponding map CType, a generic type A is interpreted as a presheaf A : W Ñ Set, by obvious structural induction, e.g. AˆB " AˆB, except for the clause for Ref, for which pRef S qw " w -1 pSq. This yields the following definition for range: rangepSq " CTypepSq [9] .

Example 3 (Simple Store). By taking S " {‹}, L " N (natural numbers) and rangep‹qpwq " V where V is a fixed set of values, we essentially obtain the model previously explored by Plotkin and Power [16] . We reserve the term simple store for this instance. Simple store is a ground store (since range is a constant functor), moreover this store is untyped (since S " {‹}) and the locations L are precisely the natural numbers.

A heap over a layout w assigns to each p : Sq P w an element from rangepSqpwq. More generally, a heaplet over w assigns an element from rangepSqpwq to some, possibly not all, p : Sq P w. We thus define the following heaplet bi-functor H : W opˆW Ñ Set:

and identify the elements of Hpw´, w`q with heaplets and the elements of Hpw, wq with heaps. Of course, we intend to use Hpw´, w`q for such w´and w`that the former is a sublayout of the latter. The contravariant action of H is given by projection and the covariant action is induced by functoriality of rangepSq.

pr p : Sq pHpw´, ρ 1 : w1 Ñ w2 qpη P Hpw´, w1 qqq " rangepSqpρ 1 qppr p : Sq ηq pr p : Sq pHpρ 2 : w2 Ñ w1 , w`qpη P Hpw1 , w`qqq " pr ρ2p : Sq η

The heaplet functor preserves independent coproduct, we overload the ' operation with the isomorphism ' : Hpw 1 , wqˆHpw 2 , wq -Hpw 1 ' w 2 , wq. 

For a heaplet example, consider w´" { 1 : Int, 2 : Ref Int } and w`" 3 : Int}. Hence, w´is a sublayout of w`. By viewing the elements of Hpw´, w`q as lists of assignments on w´, we can define s 1 , s 2 P Hpw´, w`q as follows: he category W supports (local) independent coproducts described in Section 2. These are constructed as follows. For w, w 1 P |C|, w ' w 1 " w Y { `n`1 : S | p , cq P w 1 } with n being the largest index for which w is defined on # -1 pnq. This yields a strict monoidal structure ' : WˆW Ñ W. Intuitively, w 1 ' w 2 is a canonical disjoint sum of w 1 and w 2 , but note that ' is not a coproduct in W (e.g. there is no ∇ : 1 ' 1 Ñ 1, for W only contains injections). For every ρ : w 1 Ñ w 2 , there is a canonical complement ρ A : w 2 a ρ Ñ w 2 whose domain w 2 a ρ " w 2 img ρ consists of all such cells p : Sq P w 2 that ρ misses. Given two morphisms ρ 1 : w Ñ w 1 and ρ 2 : w Ñ w 2 , we define the local independent coproduct w 1 ' w w 2 as the layout consisting of the locations from w, and the ones from w 1 and w 2 which are neither in the image of ρ 1 nor in the image of ρ 2 :

There are morphisms w 1 Fig. 3 illustrates this definition with a concrete example.

Initialization and hiding Note that in the simple store model (Definition 3), H is equivalently a contravariant functor H : W op Ñ Set with Hw " V w , hence H can be placed e.g. in rW op , Sets. In general, H is mix-variant, which calls for a more ingenious category where H could be placed. Designing such category is indeed the key insight of [9] . Closely following this work, we introduce a category E, whose objects are the same as those of W, and the morphisms P Epw, w 1 q, called initializations, consist of an injection ρ : w Ñ w 1 and a heaplet η P Hpw 1 a ρ, w 1 q:

Epw, w 1 q " ρ : wÑw 1 Hpw 1 a ρ, w 1 q.

Recall that the morphism ρ : w Ñ w 1 represents a move from a world with w allocated memory cells a world with w 1 allocated memory cells. A morphism of E is a morphism of W augmented with a heaplet part η, which provides the information how the newly allocated cells in w 1 a ρ are filled. The heap functor now can be viewed as a representable presheaf H : E Ñ Set essentially because by definition, Hw " Hpw, wq -Ep∅, wq. Let us agree to use the notation : w w 1 for morphisms in E to avoid confusion with the morphisms in W.

Like W, E supports local independent coproducts, but remarkably E does not have vanilla independent coproducts, due to the fact that E does not have an initial object. That is, in turn, because defining an inital morphism would amount to defining canonical fresh values for newly allocated cells, but those need not exist. The local independent coproducts of W and E agree in the sense that we can promote an initialization pρ 2 , ηq : w w 2 along an injection ρ 1 : w Ñ w 1 to obtain an initialization ρ 1 ‚ pρ 2 , ηq : w 1 ρ 1 ' w1 ρ 2 . This is accomplished by mapping the heaplet structure η forward along ρ 2 ‚ ρ 1 :

Hiding monad Recall that the local store is supposed to be insensitive to garbage collection. This is captured by identifying the stores that agree on their observable parts using the hiding monad P defined on rE, Sets as follows:

Here, u : E Ñ W is the obvious heaplet discarding functor upρ, ηq " ρ. Intuitively, in (2), we view the locations of w as public and the ones of w 1 a ρ as private. The integral sign denotes a coend, which in this case is just an ordinary colimit on Set and is computed as a quotient of ρ : wÑw 1 Pw Ñ u Xw 1 under the equivalence relation " obtained as a symmetric-transitive closure of the relation pρ : w Ñ w 1 , x P Xw 1 q pu ˝ρ : w Ñ w 2 , pX qpxq P Xw 2 q p : w 1 w 2 q

Note that is a preorder. Moreover, it enjoys the following diamond property.

Proposition 5. If pρ, xq pρ 1 , x 1 q and pρ, xq pρ 2 , x 2 q then pρ 1 , x 1 q pρ 1 , x 1 q and pρ 2 , x 2 q pρ 1 , x 1 q for a suitable pρ 1 , x 1 q. Hence pρ 1 , x 1 q " pρ 2 , x 2 q iff pρ 1 , x 1 q pρ, xq, pρ 2 , x 2 q pρ, xq for some pρ, xq.

Example 6. To illustrate the equivalence relation " behind P , we revisit the setting of Example 4. Consider the following situations:

Here, the solid lines indicate public locations and the dotted lines indicate private locations. The left equivalence holds because the private locations are not reachable from the public ones by references (depicted as arrows). On the right, although the public parts are equal, the reachable cells of the private parts reveal the distinction, preventing the equivalence under ". Intuitively, hiding identifies those heaps that agree both on their public and reachable private part.

The covariant action of P X (on E) is defined via promotion of initializations:

Furthermore, there is a contravariant hiding operation (on W) given by the canonical action of the coend: for ρ : w Ñ w 1 , we define hide ρ : P Xw 1 Ñ P Xw:

This allows us to regard P both as a functor rE, Sets Ñ rE, Sets and as a functor rE, Sets Ñ rW op , Sets.

Full ground store monad We now have all the necessary ingredients to obtain the full ground store monad T on rW, Sets. This monad is assembled by composing the functors in Fig. 1 in the following way. First, observe that pP p--ˆHqq H is a standard (global) store monad transform of P on rE, Sets. This monad is sandwiched between the adjunction u ‹ $ u ‹ induced by u (see Section 2). Since any monad itself resolves into an adjunction, sandwiching in it between an adjunction again yields a monad. In summary,

T " rW, Sets u ‹ rE, Sets P p´ˆHq H rE, Sets u‹ rW, Sets . (4)

Theorem 7. The monad T , defined by (4) is strong.

Proof. The proof is a straightforward generalization of the proof in [9] .

[ \ We can recover the monad previously developed by Plotkin and Power [16] by resorting to the simple store (Example 3).

Under the simple store model T is isomorphic to the local store monad from [16] :

pT Xqw -

Using (4), one obtains the requisite semantics to the language in Fig. 2 using the standard clauses of fine-grain call-by-value [11] , except for the special clauses for (put), (get) and (new), which require special operations of the monad:

To be able to give a categorical notion of higher order logic over local store, following Biering et al [2] , we aim to construct a BI-hyperdoctrine. Note that algebraic structures, such as monoids and Heyting algebras can be straightforwardly internalized in any category with finite products, which gives rise to internal monoids, internal Heyting algebras, etc. The situation changes when considering non-algebraic properties. In particular, recall that a Heyting algebra A is complete iff it has arbitrary joins, which are preserved by binary meets. The corresponding categorical notion is essentially obtained from spelling out generic definitions from internal category theory [6, B2] and is as follows.

Definition 9 (Internally Complete Heyting Algebras). An internal Heyting (Boolean) algebra A in a finitely complete category C is internally complete if for every f P CpI, Jq, there exist indexed joins f : CpI, Aq Ñ CpJ, Aq, left order-adjoint to p--q˝f : CpJ, Aq Ñ CpI, Aq such that for any pullback square on the left, the corresponding diagram on the right commutes (Beck-Chevalley condition):

It follows generally that existence of indexed joins implies existence of indexed meets , which then satisfy dual conditions ([6, Corollary 2.4.8]).

Remark 10 (Binary Joins/Meets). The adjointness condition for indexed joins means precisely that f φ ď ψ iff φ ď ψ˝f for every φ : I Ñ A and every ψ : J Ñ A. If C has binary coproducts, by taking f " ∇ : X`X Ñ X we obtain that ∇ φ ď ψ iff φ ď rψ, ψs iff φ˝inl ď ψ and φ˝inr ď ψ. This characterizes ∇ rφ 1 , φ 2 s : X Ñ A as the binary join of φ 1 , φ 2 : X Ñ A. Binary meets are characterized analogously.

Definition 11 ((First Order) (BI-)Hyperdoctrine). Let C be a category with finite products. A first order hyperdoctrine over C is a functor S : C op Ñ Poset with the following properties:

1. given X P |C|, SX is a Heyting algebra; 2. given f P CpX, Y q, Sf : SY Ñ SX is a Heyting algebra morphism; 3. for any product projection fst : XˆY Ñ X, there are pDY q X : SpXˆY q Ñ SX and p@Y q X : SpXˆY q Ñ SX, which are respective left and right orderadjoints of S fst : SpXˆY q Ñ SX, naturally in X; 4. for every X P |C|, there is " X P SpXˆXq such that for all φ P SpXˆXq, J ď pS id X , id X qpφq iff " X ď φ. 5. given X P |C|, SX is a BI-algebra, i.e. a commutative monoid equipped with a right order-adjoint to multiplication; 6. given f P CpX, Y q, Sf : SY Ñ SX is a BI-algebra morphism, then S is called a first order BI-hyperdoctrine.

In a (higher order) hyperdoctrine, C is additionally required to be Cartesian closed and every SX is required to be poset-isomorphic to CpX, Aq for a suitable internal Heyting algebra A P |C| naturally in X. Such a hyperdoctrine is a BI-hyperdoctrine if moreover A is an internal BI-algebra.

Proposition 12. Every internally complete Heyting algebra A in a Cartesian closed category C with finite limits gives rise to a canonical hyperdoctrine Cp--, Aq: for every X, CpX, Aq is a poset under f ď g iff f^g " f .

Proof. Clearly, every CpX, Aq is a Heyting algebra and every Cpf, Aq is a Heyting algebra morphism. The quantifies are defined mutually dually as follows:

Naturality in X follows from the corresponding Beck-Chevalley conditions. Finally, internal equality " X : XˆX Ñ A is defined as id X ,id X J.

[ \ A standard way to obtain an (internally) complete BI-algebra is to resort to ordered partial commutative monoids [18] .

Definition 13 (Ordered PCM [18] ). An ordered partial commutative monoid (pcm) is a tuple pM, E,¨, ďq where M is a set, E Ď M is a set of units, multipli-cation¨is a partial binary operation on M, and ď is a preorder on M, satisfying an number of axioms (see [18] for details).

We note that using general recipes [3] , for every internal ordered pcm M in a topos C with subobject classifier Ω, Cp--ˆM, Ωq forms a BI-hyperdoctrine, on particular, if C " Set then Setp--ˆM, 2q is a BI-hyperdoctrine.

We proceed to develop a local version of separation logic using semantic principles explored in the previous sections. That is, we seek an interpretation for the language in Fig. 4 in the category rW, Sets over the type system (1), extended with predicate types PA. The judgements Γ $ φ : prop type formulas depending on a variable context Γ . Additionally, we have judgements of the form Γ $ φ : PA for predicates in context. Both kinds of judgements are mutually convertible using the standard application-abstraction routine. Note that expressions for quantifiers Dx. φ are thus obtained in two steps: by forming a predicate x. φ, and subsequently applying D. Apart from the standard logical connectives, we postulate separating conjunction ‹ and separating implication‹.

Our goal is to build a BI-hyperdoctrine, using the recipes, summarized in the previous section. That is, we construct a certain internal BI-algebra Θ in rW, Sets, and subsequently conclude that r--, Θs is a BI-hyperdoctrine in question. In what follows, most of the effort is invested into constructing an internally complete Boolean algebraP˝pPĤq (hence r--,P˝pPĤqs is a hyperdoctrine), from which Θ is carved out as a subfunctor, identified by an upward closure condition. Here,P is a contravariant powerset functor, andP andĤ are certain modifications of the hiding and the heap functors from Section 4. As we shall see, the move fromP˝pPĤq to Θ remedies the problem of the former that the natural separation conjunction operator ‹ on it does not have unit ( Remark 19) .

In order to model resource separation, we must identify a domain of logical assertions over partial heaps, i.e. heaplets, instead of total heaps. We thus need to derive a unary (covariant) heaplet functor from the binary, mix-variant one H used before. We must still cope not only with heaplets, but with partially hidden heaplets, to model information hiding. A seemingly natural candidate functor for hidden heaplets is the composition P E wĎ--Hpw, --q Set : W op Ñ Set.

One problem of this definition is that the equivalence relation " underlying the construction of P (2) is too fine. Consider, for example, e w " p∅ Ď w, ‹q P w 1 Ďw Hpw 1 , wq. Then pid : w Ñ w, e w q  pinl : w Ñ w ' {‹ : 1}, e w'{‹ : 1} q, i.e. two hidden heaplets would not be equivalent if one extends the other by an inaccessible hidden cell. In order to arrive at a more reasonable model of logical assertions, we modify the previous model by replacing the category of initializations E is a categoryÊ of partial initializations. This will induce a hiding monadP over rÊ, Sets using exactly the same formula (2) as for P .

A partial initialization is a pair pρ, ηq with ρ P Wpw1 , w2 q and η P w´Ďw2 aρ Hpw´, w2 q. LetÊ be the category of heap layouts and partial initializations. Analogously to u, there is an obvious partial-heap-forgetting functor u :Ê Ñ W. LetĤ :Ê Ñ Set be the following heaplet functor :

Hw "

Given a partial initialization " pρ : w Ñ w 1 , pw 2 Ď w 1 aρ, η P Hpw 2 , w 1 qqq : w w 1 ,Ĥ :Ĥw ÑĤw 1 extends a given heaplet over w to a heaplet over w 1 via η: pĤ qpw 1 Ď w, η 1 P Hpw 1 , wqq " pρrw 1 s Y w 2 Ď w 1 , η 2 q where η 2 P Hpρrw 1 s Y w 2 Ď w 1 , w 1 q is as follows pr ρp : Sq η 2 " rangepSqpρqppr p : Sq η 1 q pp : Sq P w 1 q pr p : Sq η 2 " pr p : Sq η pp : Sq P w 2 q WithÊ andĤ as above instead of E and H, the framework described in Section 4 transforms coherently.

Remark 14. Let us fix a fresh symbol , and note that

Hw "

meaning that the passage from E, H and P toÊ,Ĥ andP is equivalent to extending the range function with designated values for inaccessible locations.

We prefer to think of this way and not as a content of dangling pointers, to emphasize that we deal with a reasoning phenomenon and not with a programming phenomenon, for our programs neither create nor process dangling pointers.

For the next proposition we need the following concrete description of the set u ‹ p2 X qw as the end ρ : wÑw 1 Pw Ñ u SetpXw 1 , 2q: this set is a space of dependent functions φ sending every injection ρ : w Ñ w 1 to a corresponding subset of Xw 1 , and satisfying the constraint: x P φpρq iff pX qpxq P φpû ˝ρq for every : w 1 w 2 . P˝p--q (using the fact that rW, Set op s op -rW op , Sets) whereP is the contravariant powerset functorP : Set op Ñ Set and for every X :Ê Ñ Set the relevant isomorphism Φ w :û ‹ p2 X qw -PpP Xwq is as follows:

Let us clarify the significance of Proposition 15. The exponential 2Ĥ in rÊ, Sets can be thought of as a carrier of Boolean predicates overĤ, and as we see next those form an internally complete Boolean algebra, which is carried from rÊ, Sets to rW, Sets byû ‹ . The alternative route viaP andP induces a Boolean algebra of predicates over hidden heapletsPĤ directly in rW, Sets. The equivalence established in Proposition 15 witnesses agreement of these two structures.

pointers as contrasted to the standard separation logic setting. We thus define a separating conjunction operator directly on everyPpPĤwq as follows:

pρ, pw 2 Ď w 1 , Hpw 2 Ď w 1 Z w 2 , w 1 qηqq " P ψ}.

Lemma 18. The operator ‹ w onPpPĤwq satisfies the following properties.

1. ‹ w is natural in w.

2. ‹ w is associative and commutative. 3. pρ : w Ñ w 1 , pw 2 Ď w 1 , η P Hpw 2 , w 1 qqq " P φ ‹ w ψ if and only if there exist w 1 , w 2 such that w 1 Z w 2 " w 2 , pρ, pw 1 Ď w 1 , Hpw 1 Ď w 2 , w 1 qηqq " P φ and pρ, pw 2 Ď w 1 , Hpw 2 Ď w 2 , w 1 qηqq " P ψ.

Property (3) specifically tells us that any representative of an equivalence class contained in a separating conjunction can be split in such a way that the respective pieces belong to the arguments of the separating conjunction.

Remark 19. The only candidate for the unit of the separating conjunction ‹ w would be the emptiness predicate empty w : 1 ÑPpPĤwq, identifying precisely the empty heaplets. However, empty w is not natural in w. In fact, it follows by Yoneda lemma that there are exactly two natural transformations 1 ÑP˝pPĤq, which are the total truth and the total false, none of which is a unit for ‹ w .

Remark 19 provides a formal argument why we cannot interpret classical separation logic overP˝pPĤq. We thus proceed to identify for every w a subset of PpPĤwq, for which the total truth predicate becomes the unit of the separating conjunction. Concretely, let Θ be the subfunctor ofP˝pPĤq identified by the following upward closure condition: φ P Θw if pρ, ηq " P φ, η ď η 1 imply pρ, η 1 q " P φ.

Lemma 20. Θ is an internal complete sublattice ofP˝pPĤq, i.e. the inclusion ι : Θ ÑP˝pPĤq preserves all meets and all joins. This canonically equips Θ with an internally complete Heyting algebra structure.

Proof (Sketch). The key idea is to establish a retraction pι, clq with cl˝ι " id. The requisite structure is then transferred fromP˝pPĤq to Θ along it. The Heyting implication for Θ is obtained using the standard formula pφ ñ ψq " {ξ | φ^ξ ď ψ} interpreted in the internal language.

[ \ Lemma 21. Separating conjunction preserves upward closure: for φ, ψ P Θw, φ ‹ w ψ " cl w pφ ‹ w ψq.

Lemma 22. Θ is a BI-algebra: ‹ w is obtained by restriction fromPpPĤwq by Lemma 21,PĤw is the unit for it and φ‹ w ψ " {pρ, ηq " P Θw | @ρ 1 : w Ñ w 1 , η 1 , η 2 PĤw 1 , η 1¨η2 definedp ρ, ηq " pρ 1 , η 1 q^pρ 1 , η 2 q " P φ ñ pρ 1 , η 1¨η2 q " P ψ}.

s, ρ, η |ù J s, ρ, η |ù φ^ψ if s, ρ, η |ù φ and s, ρ, η |ù ψ s, ρ, η |ù φ _ ψ if s, ρ, η |ù φ or s, ρ, η |ù ψ s, ρ, η |ù φ ñ ψ if for all pρ, ηq " pρ 1 , η 1 q and η 1 ď η 2 , s, ρ 1 , η 2 |ù φ implies s, ρ 1 , η 2 |ù ψ s, ρ, η |ù φpvq if s, ρ, pp Γ $v v : A w 1˝Γ ρqs, ηq |ù φ s, ρ, pa, ηq |ù x. φ if a " pXρqb and ps, bq, ρ, η |ù φ s, ρ, η |ù Ñ v if η " pw 2 Ď w 1 , δ P Hpw 2 , w 1 qq and

s, ρ, pw1 Ď w 1 , Hpw1 Ď w1 Z w2, w 1 qηq |ù φ and s, ρ, pw2 Ď w 1 , Hpw2 Ď w1 Z w2, w 1 qηq |ù ψ s, ρ, η |ù φ‹ ψ if for all pρ 1 , η1q " pρ, ηq and for all η2 such that η1¨η2 is defined, s, ρ 1 , η2 |ù φ implies s, ρ 1 , η1¨η2 |ù ψ s, ρ, η |ù Dφ if Γ pû ˝ρqs, id w 2 , pa,Ĥ ˝ηq |ù φ for some : w 1 w 2 , a P Aw 2 s, ρ, η |ù @φ if Γ pû ˝ρqs, id w 2 , pa,Ĥ ˝ηq |ù φ for all : w 1 w 2 , a P Aw 2 Proof. In view of Lemma 20, we are left to show that the given operations are natural and that Θ is an internal BI-algebra w.r.t. them. Since BI-algebras form a variety [5] , it suffices to show that each Θw is a BI-algebra. By Lemma 18 (ii), it suffices to show that every p--q ‹ w φ preserves arbitrary joins, for then we can use the standard formula to calculate φ‹ w ψ, which happens to be natural in w:

By unfolding the right-hand side, we obtain the expression for‹ w figuring in the statement of the lemma.

[ \ Theorem 23. Θ is an internally complete Heyting BI-algebra, hence r--, Θs is a BI-hyperdoctrine.

Proof. Follows from Lemmas 20 and 22.

[ \ This now provides us with a complete semantics of the language in Fig. 4 with Γ $ φ : prop : Γ Ñ Θ and Γ $ φ : PA : Γ Ñ PA where PA is the upward closed subfunctor ofP˝pP pûAˆĤqq, with upward closure only on theĤ-part, which is isomorphic to Θ A . The resulting semantics is defined in Fig. 5 where we write s, ρ, η |ù φ for pρ, ηq " P Γ $ φ : prop psq and s, ρ, pa, ηq |ù φ for pρ, pa, ηqq " P Γ $ φ : PA psq. The following properties [4] are then automatic.

Proposition 24. -(Monotonicity) If s, ρ, η |ù φ and η ď η 1 then s, ρ, η 1 |ù φ.

-(Shrinkage) If s, ρ, η |ù φ, η 1 ď η and η 1 contains all cells reachable from s and w then s, ρ, η 1 |ù φ.

Let us illustrate subtle features of our semantics by some examples.

Example 25. Consider the formula D : Ref Int . Ñ 5 from the introduction in the empty context --. Then --, ρ, η |ù D . Ñ 5 iff for some : w 1 w 2 , and some x P Ref Int w 2 , x, id w 2 , pĤ qη |ù 1 Ñ 5. The latter is true iff pr x ppĤ qηq " 5. Note that w 1 may not contain and it is always possible to choose so that w 2 contains and pr x ppĤ qηq " 5. Hence, the original formula is always valid.

Example 26. The clauses in Fig. 5 are very similar to the standard Kripke semantics of intuitionistic logic. Note however, that the clause for implication strikingly differs from the expected one s, ρ, η |ù φ ñ ψ if for all η ď η 1 , s, ρ, η 1 |ù φ implies s, ρ, η 1 |ù ψ, though. The latter is indeed not validated by our semantics, as witnessed by the following example. Consider the following formulas φ and ψ respectively:

:

The first formula is valid over heaplets, in which refers to a reference to some integer, while the second one is only valid over heaplets, in which refers to a reference to 6. Any η 1 ě η " pid w , p{ 2 } Ď { , 2 }, r 2 Þ Ñ 6sqq satisfies both (6) and (7) or none of them. However, the implication φ ñ ψ still is not valid over η in our semantics, for η " pw Ñ w ' p 1 : Intq, p{ 1 , 2 } Ď { , 1 , 2 }, r 1 Þ Ñ 5, 2 Þ Ñ 6sqq ď pw Ñ w ' p 1 : Intq, p{ , 1 , 2 } Ď { , 1 , 2 }, r Þ Ñ 1 , 1 Þ Ñ 5, 2 Þ Ñ 6sqq and the latter heaplet validates φ but not ψ.

Example 27. Least µ and greatest ν fixpoints can be encoded in higher order logic [2] . As an example, consider

isList " µγ. . Ñ null _ D 1 , x. Ñ px, 1 q ‹ γp 1 q, which specifies the fact that is a pointer to a head of a list (eliding coproduct injections in inl null and inrpx, 1 q). By definition, isList satisfies the following recursive equation:

isListp q " Ñ null _ D 1 , x. Ñ px, 1 q ‹ isListp 1 q Let us expand the semantics of the right hand side. We have : Ref list , isList : PpRef list q $ l Ñ null _ D 1 , x. Ñ px, 1 q ‹ isListp 1 q w pisListq " {pρ : w Ñ w 1 , pRef list ρqp q, δ PĤw 1 q " | pr ρp q pδq " null }Y : Ref list , isList : PpRef list q $ D 1 , x. Ñ px, 1 q ‹ isListp 1 q w pisListq " {pρ : w Ñ w 1 , pRef list ρqp q, δ PĤw 1 q " | pr ρp q pδq " null _ D 1 , x. pr ρp q δ " px, 1 q^pρ, 1 , δ ρp qq " P isList} where δ ρp q denotes the δ with the cell ρp q removed. In summary, pρ : w Ñ w 1 , pRef list ρqp q, δ PĤw 1 q " is in : Ref list , isList : PpRef list q $ isListp q w pisListq if and only if either pr ρp q δ " null or there exists an l 1 P w 1 such that pr ρp q δ " px, 1 q and pρ, 1 , δ ρp qq " P isList.

Compositionality is an uncontroversial desirable property in semantics and reasoning, which admits strikingly different, but equally valid interpretations, as becomes particularly instructive when modelling dynamic memory allocation. From the programming perspective it is desirable to provide compositional means for keeping track of integrity of the underlying data, in particular, for preventing dangling pointers. Reasoning however inherently requires introduction of partially defined data, such as heaplets, which due to the compositionality principle must be regarded as first class semantic units.

Here we have made a step towards reconciling recent extensional monadbased denotational semantic for full-ground store [9] with higher order categorical reasoning frameworks [2] by constructing a suitable intuitionistic BI-hyperdoctrine. Much remains to be done. A highly desirable ingredient, which is currently missing in our logic in Fig. 4 is a construct relating programs and logical assertions, such as the following dynamic logic style modality Γ $ c p : A Γ $ φ : PA Γ $ rpsφ : prop which would allow us e.g. in a standard way to encode Hoare triples {φ}p{ψ} as implications φ ñ rpsψ. This is difficult due to the outlined discrepancy in the semantics for construction and reasoning. The categories of initializations for p and φ and the corresponding hiding monads are technically incompatible. In future work we aim to deeply analyse this phenomenon and develop a semantics for such modalities in a principled fashion.

Orthogonally to these plans we are interested in further study of the full ground store monad and its variants. One interesting research direction is developing algebraic presentations of these monads in terms of operations and equations [17] . Certain generic methods [13] were proposed for the simple store case (Example 3), and it remains to be seen if these can be generalized to the full ground store case.

Intensionality, definability and computation

BI-hyperdoctrines, higher-order separation logic, and abstraction

On models of higher-order separation logic

Program logic and equivalence in the presence of garbage collection

Residuated Lattices: An Algebraic Glimpse at Substructural Logics

Sketches of an elephant: A topos theory compendium

Conditions related to De Morgan's law

Iris from the ground up: A modular foundation for higher-order concurrent separation logic

A monad for full ground reference cells

Adjointness in foundations

Modelling environments in call-by-value programming languages

Categories for the Working Mathematician

A fibrational account of local states

Semantics of local variables. Applications of categories in computer science

A Category-theoretic Approach to the Semantics of Programming Languages

Notions of computation determine monads

Algebraic operations and generic effects

Possible worlds and resources: the semantics of BI

The essence of ALGOL

Intuitionistic reasoning about shared mutable data structure

Separation logic: A logic for shared mutable data structures

Category-theoretic structure for independence and conditional independence

Instances of computational effects: An algebraic perspective

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use

Theorem 16. For every X :Ê Ñ Set,P˝pP Xq is an internally complete Boolean algebra in rW, Sets under f φ : I ÑP˝pP Xq w pj P Jwqfor every f : I Ñ J, and the corresponding Boolean algebra operations are computed as set-theoretic unions, intersections and complements.By Theorem 16, we obtain a hyperdoctrine r--,P˝pPĤqs, which provides us with a model of (classical) higher order logic in rW, Sets. In particular, this allows us to interpret the language from Fig. 4 over rW, Sets excluding the separation logic constructs, in such a way that. .ˆA n for Γ " px 1 : A 1 , . . . , x n : A n q where, additionally to the standard clauses, PA "P˝P pu ‹ AˆĤq. The latter interpretation of predicate types PA is justified by the natural isomorphism:Here, the first and the last transitions are by Φ from Proposition 15 and the middle one is due to the fact that clearly both pû ‹ p--qq X $û ‹ pXˆp--qq and u ‹ pp--qû ‹ X q $û ‹ pXˆp--qq.Since every setĤw models a heaplet in the standard sense [18] , we can equipĤw with a standard pointer model structure.