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 .