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.