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.

Advertisements

1 thought on “A comment on ‘Abstract Separation Logic’”

  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.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s