If and are functions, what does mean?
Definition 1. A separation algebra (citation) is a triple , where is a set, has type and is commutative, associative and cancellative, and is the unit of . From any separation algebra we can induce a preorder defined by .
Definition 2. A complete separation algebra is a separation algebra for which unique meets and joins (with respect to ) exist for arbitrary subsets of .
Definition 3 (‘Star’ for sets). The standard ‘star’ operator, of type , is defined by:
Through the standard sets/predicates correspondence, we can see as an operator on functions of type . It is natural to ask if we can generalise to functions of type , for arbitrary separation algebras and . Here is one attempt to do so:
Definition 4 (‘Star’ for functions).
Note that because we’re taking an arbitrary join here, we require to be a complete separation algebra.
Lemma 1. There is exactly one 2-element complete separation algebra: , where meet corresponds to boolean AND, join corresponds to boolean OR, and is the following ‘partial AND’ operation:
The following theorem justifies Defn. 4 by showing that Defn. 3 can be derived.
Theorem 1. Defn. 3 is a special case of Defn. 4, obtained by instantiating to .
Proof. Note that for any predicate , we have . (This is because returns iff contains .) From this observation and Defn. 4, it follows that for any :
We complete the proof by noting that iff and .