[Agda] Re: Classical Mathematics for a Constructive World

[wren ng thornton]

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