[Agda] Re: Classical Mathematics for a Constructive World

wren ng thornton wren at freegeek.org
Mon Dec 3 01:35:14 CET 2012

As Ramana Kumar mentioned (offlist?), in separation logic the _*_
connector is for separating conjunction. That is, P*Q is true of some
heap h just in case we can partition h into subheaps h1 and h2 such that
P is true of h1 and Q is true of h2:

h \in P*Q \iff
\exists h1, h2. dom(h1) \disjoint dom(h2) /\ h1 . h2 = h /\
h1 \in P /\ h2 \in Q

This partitioning is crucial to the whole idea of separation logic.
Notably, neither weakening nor contraction are sound for _*_. There's
also a notion of separating implication, but that's not relevant for the
point I was making. If you're interested in more, check out, e.g.,
<http://www.cs.cmu.edu/~jcr/seplogic.pdf>

The interpretation of a Hoare triple over separation-logic predicates is
(basically):

{P}C{Q} \iff
\forall p. p \in P =>
\forall q. (p,C) --->* (q,skip) =>
q \in Q

where (h,C) is a program state, namely a pair of the current heap and
the remaining program; where --->* is the reflexive transitive closure
of the program evaluation function; and where skip is the empty program.
The actual definition must, of course, deal with issues like programs
that don't terminate or which segfault (i.e., dereference an unbound
address). And it may be desirable for the definition to compose on a
disjoint heap in order to make \top an identity element for _*_. But the
basic idea is the same.

The side condition for the frame rule is, as Ramana Kumar said, that the
additional R does not mention variables assigned in C.

The point I was making by this example is that, even though we often
think of P and Q as "heaps", they are not heaps themselves but rather
are predicates over heaps (or sets of heaps). And because of this,
together with the fact that we're quantifying over those sets, even if
the existence of a heap satisfying Q is preserved by the frame rule,
that does not mean it preserves the particular witness to that
existence. This ties into the failure of GMP because there too the fact
of there always existing a witness does not mean that the particular
witness is uniform/stable across all preconditions.

--
Live well,
~wren