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}.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s