The boolean isomorphism between sets and characteristic functions

Note: This is just for fun.

We have seen that both sets (over a universe \(E\)) and their characteristic functions (from \(E\) to \(\{\textbf{True},\textbf{False}\}\)) are boolean algebras.

Their lattice structure is easy to compute, with meet and join over sets being intersection and union, and over functions being pointwise conjunction and disjunction.

instance Lattice (Set a) where
  meet = intersect
  join = union
instance Lattice (a -> Bool) where
  f `meet` g = \x -> f && g
  f `join` g = \x -> f || g

Their boolean structure is more difficult to compute, however, because one cannot in general enumerate all the elements of a type, which would be necessary to define the top element of the set algebra.

instance Boolean (Set a) where
  top = undefined -- list all elements of type 'a'
  bot = empty
  cmp s = top `difference` s
instance Boolean (a -> Bool) where
  top = \_ -> True
  bot = \_ -> False
  cmp f = \x -> not (f x)

This is not a problem for functions, as a function needn’t enumerate objects, only be prepared to produce an output for any object given.

If we assume that the universe is finite, and that we may therefore enumerate its elements, we can give a proper implementation of the boolean structure of sets:

instance (Bounded a,Enum a) => Boolean (Set a) where
  top = fromList [minBound..maxBound]
  bot = empty
  cmp s = top `difference` s

The concept of an isomorphism allows us to give voice to the idea that two structures are identical with respect to everything that matters, or ‘equivalent’. From the perspective of University bureaucrats, two courses are identical if they have the same numbers of enrolled students.¹ The individuals in the courses are irrelevant, all that matters is their numerosity. One way of conceptualizing this is that two courses are equivalent for the bureaucrat if the students can be put into a one to one correspondence, leaving no one out. In other words, if we can give a function associating students in the one course with students in the other course, which is injective (different students are mapped to different students) and surjective (all students are accounted for).

If it also mattered in what semester each student in a course was, the notion of equivalence would have to take this into account: an isomorphism would be required to map students of each semester to students of the same semester, in addition to being in- and surjective.

A homomorphism is a function from one set to another that respects structure. Unlike an isomorphism, it is not required to be in- or surjective. It expresses the idea that one structure is similar (but not necessarily equivalent) to another. Continuing our last example, a homomorphism between classes respecting the semester-age of students would be a function from one class to the other mapping a student in the first class to one with the same semester-age in the other. Crucially, two different students could be mapped onto the same student. The existence of a homomorphism would tell us that every student-age in the first class was represented in the second class. It wouldn’t tell us anything else about the number of the students in the classes, or about whether there were student ages in the second class not represented in the first.

It is often easier to give an isomorphism between structures \(A\) and \(B\) indirectly, by giving two homomorphisms, one from \(A\) to \(B\) and the other from \(B\) to \(A\), which are inverses of each other.

homAB (homBA b) == b
homBA (homAB a) == a

In other words, structure \(A\) is isomorphic to structure \(B\) if each is homomorphic to the other, and both homomorphisms are injective.² This property, that two functions ‘cancel out’ (i.e. their composition is the identity function), is called being an inverse (on the left/right). For example, if f . g == id, then f is a left inverse for g, and g is a right inverse for f. If f is both a left and a right inverse for g, then f is just called an inverse for g.

Lattice isomorphisms

A lattice-homomorphism is a function lhom between lattices that respects the operations of meet and join. In other words, for any objects a1 and a2 in one lattice, their meet is mapped to the meet of lhom a1 and lhom a2 in the other lattice.

lhom :: (Lattice a, Lattice b) => a -> b
lhom (a1 `meet` a2) == lhom a1 `meet` lhom a2
lhom (a1 `join` a2) == lhom a1 `join` lhom a2

We can exhibit a lattice isomorphism between Set a and a -> Bool by giving homomorphisms in both directions, and showing that they are inverses.

The homomorphism from sets to functions is simply the operation assigning its characteristic function to a set.

homSetFunc :: Set a -> (a -> Bool)
homSetFunc s = \x -> x `member` s

We can verify that it is indeed a lattice homomorphism by unfolding definitions, and replacing likes with likes.

homSetFunc (s `meet` t)
  -- by the definition of 'homSetFunc'
  == \x -> x `member` (s `meet` t)
  -- by the definition of set intersection
  == \x -> x `member` s && x `member` t
  -- by the definition of 'meet' over functions
  == (\x -> x `member s`) `meet` (\x -> x `member` t)
  -- by the definition of 'homSetFunc'
  == homSetFunc s `meet` homSetFunc t

homSetFunc (s `join` t)
  -- by the definition of 'homSetFunc'
  == \x -> x `member` (s `join` t)
  -- by the definition of set union
  == \x -> x `member` s || x `member` t
  -- by the definition of 'join' over functions
  == (\x -> x `member s`) `join` (\x -> x `member` t)
  -- by the definition of 'homSetFunc'
  == homSetFunc s `join` homSetFunc t

The homomorphism from functions to sets requires us to be able to enumerate all elements of the domain, so as to determine which of them belong to the set we are trying to construct.

homFuncSet :: (Bounded a, Enum a) => (a -> Bool) -> Set a
homFuncSet f = fromList [x | x <- top, f x]

Again, we must verify that this function is indeed a lattice homomorphism.

homFuncSet (f `meet` g)
  -- by the definition of 'homFuncSet'
  == fromList [x | x <- top, (f `meet` g) x]
  -- by the definition of 'meet' over functions
  == fromList [x | x <- top, f x && g x]
  -- by the definition of set intersection
  == fromList [x | x <- top, f x] `meet` fromList [x | x <- top, g x]
  -- by the definition of 'homFuncSet'
  == homFuncSet f `meet` homFuncSet g

homFuncSet (f `join` g)
  -- by the definition of 'homFuncSet'
  == fromList [x | x <- top, (f `join` g) x]
  -- by the definition of 'join' over functions
  == fromList [x | x <- top, f x || g x]
  -- by the definition of set union
  == fromList [x | x <- top, f x] `join` fromList [x | x <- top, g x]
  -- by the definition of 'homFuncSet'
  == homFuncSet f `join` homFuncSet g

We first show that homFuncSet is a left inverse for homSetFunc, in other words, that for any set s, homFuncSet (homSetFunc s) == s. Recall that two sets are equal iff they have the same elements. Let the input set s be given. We calculate:

homFuncSet (homSetFunc s)
  -- by the definition of 'homFuncSet'
  == fromList [x | x <- top, homSetFunc s x]
  -- by the definition of 'homSetFunc'
  == fromList [x | x <- top, x `member` s]
  -- sets which have the same members are the same
  == s

We see then that homFuncSet (homSetFunc s) is the set of all elements of the domain x, which are members of the set s. As sets are individuated by their members, this is the same set as s.

Now we can show that homFuncSet is also a right inverse for homSetFunc, in other words, that for any function f, homSetFunc (homFuncSet f) == f. We have to specify what we mean by equality of functions. Two functions are identical just in case they map the same inputs to the same outputs:³

instance (Bounded a, Enum a) => Eq (a -> Bool) where
  f == g = all (\x -> f x == g x) [minBound..maxBound]

Now we let f be arbitrary, and we calculate:

homSetFunc (homFuncSet f)
  -- by the definition of 'homSetFunc'
  == \x -> x `member` homFuncSet f
  -- by the definition of 'homFuncSet'
  == \x -> x `member` fromList [x | x <- top, f x]
  -- an element is a member of a set iff it satisfies the conditions
  -- for belonging to the set
  == \x -> f x
  -- by the definition of equality of functions
  == f

An object x is a member of a set fromList [x | g x] just in case x has property g x. We see therefore that homFuncSet is a right inverse of homSetFunc.

In conjunction with our previous result, these functions are inverses of one another, and therefore are lattice isomorphisms.

Boolean isomorphisms

A boolean-homomorphism is a homomorphism between boolean lattices that maps top and bot elements to top and bot elements respectively, and respects the operation cmp. In other words, for any object a in lattice A, its complement is mapped to the complement of h(a) lattice B. In symbols:

bhom :: (Boolean a, Boolean b) => a -> b
bhom top == top
bhom bot == bot
bhom (cmp a) == cmp (bhom a)

A boolean-isomorphism consists of a pair of boolean-homomorphisms bhomAB :: a -> b and bhomBA :: b -> a which are inverse to one another.

We can exhibit a boolean isomorphism between Set a and a -> Bool by giving homomorphisms in both directions, and showing that they are inverses. We take as our homomorphisms the lattice homomorphisms from before, which we have already shown to be inverses.

We verify that they are indeed boolean homomorphisms, in addition to mere lattice homomorphisms. We begin with the homomorphism from sets to functions.

homSetFunc top
  -- by the definition of 'homSetFunc'
  == \x -> x `member` top
  -- everything is an element of 'top'
  == \x -> True
  -- by the definition of 'top'
  == top

homSetFunc bot
  -- by the definition of 'homSetFunc'
  == \x -> x `member` bot
  -- nothing is an element of 'bot'
  == \x -> False
  -- by the definition of 'bot'
  == bot

homSetFunc (cmp s)
  -- by the definition of 'homSetFunc'
  == \x -> x `member` (cmp s)
  -- by the definition of 'cmp'
  == \x -> x `member` (top `difference` s)
  -- by the definition of set difference
  == \x -> x `member` top && not (x `member` s)
  -- everything is an element of 'top'
  == \x -> True && not (x `member` s)
  -- Logic: True && phi == phi
  == \x -> not (x `member` s)
  -- by the definition of 'cmp' over functions
  == cmp (\x -> x `member` s)
  -- by the definition of 'homSetFunc'
  == cmp (homSetFunc s)

Now we verify that the map from functions to sets is also a boolean homomorphism.

homFuncSet top
  -- by the definition of 'homFuncSet'
  == fromList [x | x <- top, top x]
  -- by the definition of 'top'
  == fromList [x | x <- top, (\y -> True) x]
  -- '(\y -> True) x' is always true
  == fromList [x | x <- top]
  -- sets which have the same elements are the same
  == top

homFuncSet bot
  -- by the definition of 'homFuncSet'
  == fromList [x | x <- top, bot x]
  -- by the definition of 'bot'
  == fromList [x | x <- top, (\y -> False) x]
  -- nothing satisfies '(\y -> False)'
  == fromList []
  -- sets which have the same elements are the same
  == bot

homFuncSet (cmp f)
  -- by the definition of 'homFuncSet'
  == fromList [x | x <- top, cmp f x]
  -- by the definition of 'cmp' over functions
  == fromList [x | x <- top, not (f x)]
  -- by the definition of set difference
  == fromList [x | x <- top] `difference` fromList [x | x<- top, f x]
  -- by the definition of 'top'
  == top `difference` fromList [x | x<- top, f x]
  -- by the definition of 'homFuncSet'
  == top `difference` homFuncSet f
  -- by the definition of 'cmp' over sets
  == cmp (homFuncSet f)

Ordering functions

We have seen that, for any set \(A\), the power set of \(A\) (\(\wp(A) = \{B : B \subseteq A\}\)) is isomorphic as a boolean algebra to the set of boolean valued functions over \(A\) (\([A \rightarrow \{\mathbf{True},\mathbf{False}\}]\)). We know, however, that every boolean algebra has a partial order definable over its elements, and that this partial order is a crucial part of its structure. In a powerset algebra, the partial order coincides with the subset relation. What is this partial order in the boolean algebra of boolean valued functions?

In the world of sets, we have that set s1 is a subset of s2 iff every element of s1 is contained in s2.

s1 `subset` s2 = all (\x -> x `member` s2) s1

We express talk about the partial order relationship in a boolean algebra in terms of the Haskell class Ord:

instance Ord a => Ord (Set a) where
  s1 <= s2 = s1 `subset` s2

instance Ord Bool where
  a <= b = if a then b

Since sets and functions are booleanly equivalent, we can define an ordering over functions by translating them into sets and using the subset ordering.

f <= g = homFuncSet f `subset` homFuncSet g

We can unfold definitions to get a direct characterization of the ordering over functions without the detour into the world of sets.

f <= g
  -- by the definition of '<=' over functions
  == homFuncSet f `subset` homFuncSet g
  -- by the definition of 'subset'
  == all (\y -> y `member` homFuncSet g) (homFuncSet f)
  -- by the definition of 'homFuncSet'
  == all (\y -> y `member` fromList [x | x <- top, g x]) (homFuncSet f)
  -- by the definition of membership
  == all (\y -> g y) (homFuncSet f)
  -- by the definition of 'homFuncSet'
  == all (\y -> g y) (fromList [x | x <- top, f x])
  -- everything which is P is Q just in case everything is (if P then Q)
  == all (\y -> if f y then g y) top

We observe that if b then c is the boolean order over truth values, and generalize the characterization of the boolean order over boolean-valued functions to function to an arbitrary boolean algebra:

instance (Enum a, Bounded a, Boolean b, Ord b) => Ord (a -> b) where
  f <= g = all (\x -> f x <= g x) (homFuncSet top)

In plain English, one boolean algebra valued function is less than or equal to another just in case for each input, their outputs are less than or equal to one another. This definition is pointwise, as a property of functions is defined in terms of the property holding of each of its outputs.