A Monadic Model for Set Theory, Part 2

\(\newcommand{\fcd}{\leadsto}\)

Last time, we discussed funcads, which are a generalization of functions that can have multiple or no values for each element in their input.

Composition of Funcads

The composition of funcads is defined to be compatible with the composition of functions, and it takes a fairly similar form:

\[f :: Y \fcd Z \wedge f :: X \fcd Y \implies \exists (f \odot g :: X \fcd Z), (f \odot g)(x) = \bigcup_{\forall y \in g(x)} f(y)\]

In other words, map the second function over the result of the first and take the union. If you’re a Haskell programmer, you probably were expecting this from the title and the name “funcad”: the funcad composition rule is just Haskell’s >=>.

Anyway, here are a few examples of funcad compositions (originals in blue, red. output in green.):

Two functional, total funcads

These compose like regular functions

Composing a funcad with its inverse

We can represent the operator:

\[\star :: (A \fcd B) \to (A \fcd A)\] \[\star f = f^{-1} \odot f\]

Examples

\[f(x) = {x^2}\]

\[f(x) = \sqrt x\]

\[f(x) = \{y | x-1 \leq y \leq x + 1 \}\] \[f^{-1}(x) = \{y | x \in f(y)\} = \{y | y - 1 \leq x \leq y + 1 \}\] \[\star f (x) = \{y | y - 1 \leq z \leq y + 1, z \in \{t | x - 1 \leq t \leq x + 1\}\} \] \[\star f (x) = \{y | y - 1 \leq z \wedge z \leq y + 1, x - 1 \leq z \leq x + 1\} \] \[\star f (x) = \{y | y \leq z + 1 \wedge z - 1 \leq y, x - 1 \leq z \leq x + 1\} \] \[\star f (x) = \{y | y \leq x + 2 \wedge x - 2 \leq y\} \] \[\star f (x) = \{y | x - 2 \leq y \leq x + 2\} \]

General Characterization

In general, \(\star\) represents the well-behavedness of the given funcad under under iversion.

We can find that

\[\star f(x) = f^{-1} \odot f (x) = \bigcup_{\forall y \in f(x)} f^{-1}(y)\] \[\star f (x) = \bigcup_{\forall y \in f(x)} f^{-1}(y)\]

Basically, \(\star f\) represents how one-to-one \(f\) is.

For any isomorphism \(f\), we have \(\star f(x) = x\).

For any one-to-one and functional funcad, we have

\[\star f(x) = \bigcup_{\forall y \in f(x)} f^{-1}(y) = \bigcup_{\forall y \in f(x), |f(x)| = 1, |f^{-1}(y)| = 1} f^{-1}(y)=\left\{\begin{array}{cc} \{x\} & \text{if \(|f(x)| = 1\)}\\ \{\} & \text{otherwise} \end{array}\right.\]

For example, for \(f(t) = \{t^2 - 2t\}, 0 \leq t \leq 1\), \(\star f(t) = t, 0 \leq t \leq 1\):

For a more complex funcad, such as \(f(x) = \pm \sqrt{1-x^2}\), we have \[\star f(x) = f^{-1}(\sqrt{1 - x^2}) \cup f^{-1}(-\sqrt{1-x^2}) = \pm x, -1 \leq x \leq 1\]

A Quick Coding Sample

So, we now know a few things about funcads. How about we put this knowledge into effect?

So, Funcads are Monads, and the typical set-like monad used in Haskell is a list where we don’t care about order or duplication. Therefore, we can define:

import Prelude hiding ((.))
import Control.Category

data Funcad a b = Funcad (a -> [b])
instance Category Funcad where
    id = Funcad return
    Funcad a . Funcad b = Funcad $ \x -> b x >>= a