# A star operator for functions

If $f$ and $g$ are functions, what does $f*g$ mean?

Definition 1. A separation algebra (citation) is a triple $(M, \circ, u)$, where $M$ is a set, $\circ$ has type $M \times M \rightharpoonup M$ and is commutative, associative and cancellative, and $u\in M$ is the unit of $\circ$. From any separation algebra we can induce a preorder defined by $m_1\preceq m_2 = \exists m'\ldotp m_1 \circ m' = m_2$.

Definition 2. A complete separation algebra is a separation algebra $(M, \circ, u)$ for which unique meets and joins (with respect to $\preceq$) exist for arbitrary subsets of $M$.

Definition 3 (‘Star’ for sets). The standard ‘star’ operator, of type $\mathop{\mathcal{P}}(M) \times \mathop{\mathcal{P}}(M) \rightarrow \mathop{\mathcal{P}}(M)$, is defined by:

$\displaystyle P * Q \ =\ \{m \mid \exists m_1, m_2\ldotp m_1 \circ m_2 = m \wedge m_1 \in P \wedge m_2 \in Q\}$

Through the standard sets/predicates correspondence, we can see $*$ as an operator on functions of type $M\rightarrow\mathbb{B}$. It is natural to ask if we can generalise to functions of type $M\rightarrow N$, for arbitrary separation algebras $(M,\circ_M, u_M)$ and $(N,\circ_N, u_N)$. Here is one attempt to do so:

Definition 4 (‘Star’ for functions).

$\displaystyle f * g \ =\ \lambda m\ldotp \bigsqcup\{n\mid \exists m_1, m_2\ldotp m_1 \circ_M m_2 = m \wedge f(m_1) \circ_N g(m_2) = n\}$

Note that because we’re taking an arbitrary join here, we require $(N, \circ_N, u_N)$ to be a complete separation algebra.

Lemma 1. There is exactly one 2-element complete separation algebra: $(\mathbb{B}, \circ_\mathbb{B}, {\sf true})$, where meet corresponds to boolean AND, join corresponds to boolean OR, and $\circ_\mathbb{B}$ is the following ‘partial AND’ operation:

$\displaystyle \begin{array}{ccc} b_1 & b_2 & b_1 \circ_{\mathbb{B}} b_2 \\\hline {\sf false} & {\sf false} & {\rm (undefined)} \\ {\sf false} & {\sf true} & {\sf false} \\ {\sf true} & {\sf false} & {\sf false} \\ {\sf true} & {\sf true} & {\sf true} \end{array}$

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 $N$ to $(\mathbb{B},\circ_{\mathbb{B}},{\sf true})$.

Proof. Note that for any predicate $\Phi:\mathbb{B}\rightarrow\mathbb{B}$, we have $\bigsqcup\{n\mid\Phi(n)\} = \Phi({\sf true})$. (This is because $\bigsqcup X$ returns ${\sf true}$ iff $X$ contains ${\sf true}$.) From this observation and Defn. 4, it follows that for any $f,g:M\rightarrow\mathbb{B}$:

$\displaystyle f*g\ =\ \lambda m\ldotp \exists m_1,m_2\ldotp m_1\circ_M m_2 = m \wedge f(m_1) \circ_{\mathbb{B}} g(m_2) = {\sf true}$

We complete the proof by noting that $f(m_1) \circ_{\mathbb{B}} g(m_2) = {\sf true}$ iff $f(m_1)={\sf true}$ and $g(m_2) = {\sf true}$.