Abstract Separation Logic (citation) is based on a partial composition operator, , which has the following type:

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

**Theorem 1.** If and and is undefined, then is undefined too.

**Theorem 2. ** If and and , then .

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

**Theorem 3.** If and then .

All that remains is to interpret the 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:

.

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:

.

Theorem 3 now correctly entails both Theorems 1 and 2.

### Like this:

Like Loading...

Abstract separation logic encodes commands as functions of type . The here represents the final state of an ‘aborting’ command. I suspect that this may be the same as the that results from an undefined composition operation.