A comment on ‘Abstract Separation Logic’

Abstract Separation Logic (citation) is based on a partial composition operator, $\circ$, which has the following type: $\circ : \Sigma \times \Sigma \rightharpoonup \Sigma$

We shall concentrate henceforth on the simplest incarnation of this operator: disjoint union. Here are two useful theorems about disjoint union.

Theorem 1. If $a\subseteq a'$ and $b\subseteq b'$ and $a\circ b$ is undefined, then $a'\circ b'$ is undefined too.

Theorem 2. If $a\subseteq a'$ and $b\subseteq b'$ and $a'\circ b' = c'$, then $\exists c\subseteq c'\ldotp a\circ b = c$.

Can we assimilate those two theorems into one?  Our combined theorem should have the following form:

Theorem 3. If $a\subseteq a'$ and $b\subseteq b'$ then $a\circ b \le a'\circ b'$.

All that remains is to interpret the $\le$ comparator: how should ‘undefined’ compare to other values? The standard encoding of a partial function as a total function with a lifted codomain puts ‘undefined’ at the bottom of the ordering, like so: $\circ : \Sigma \times \Sigma \rightarrow \Sigma_\bot$.

Unfortunately, this does not make Theorem 3 entail Theorem 1. My proposed fix is to put ‘undefined’ at the top of the ordering, like so: $\circ : \Sigma \times \Sigma \rightarrow \Sigma^{\top}$.

Theorem 3 now correctly entails both Theorems 1 and 2.

1. Abstract separation logic encodes commands as functions of type $\Sigma \rightarrow (\mathcal P\, \Sigma)^{\top}$. The $\top$ here represents the final state of an ‘aborting’ command. I suspect that this may be the same as the $\top$ that results from an undefined composition operation.