# Constructive gem: juggling exponentials

Constructive gems are usually not about particular results, because all constructive results can be proved classically as well, but rather about the method and the way of thinking. I demonstrate a constructive proof which can be reused in three different settings (set theory, topology, computability) because constructive mathematics has many different interpretations.

Let me first introduce some notation:

• $1 = \{0\}$ is the singleton set, or the unit.
• $2 = 1 + 1 = \{0,1\}$ is the booleans.
• In general, $[n]= \{0, 1, \ldots, n-1\}$ is the $n$-fold coproduct of singletons. For brevity we will write $n$ instead of $[n]$.
• In general $A + B$ is the disjoint sum of $A$ and $B$.
• The product $A \times B$ is the cartesian product of $A$ and $B$.
• The exponential $B^A$, also written as $A \to B$, is the set of functions from $A$ to $B$.

I should warn you that $2$ is not in general isomorphic to the set of truth values $\Omega$, and consequently $2^A$ is not generally isomorphic to $\Omega^A = P(A)$, the powerset of $A$. Rather, the elements of $2^A$ are the characteristic functions of decidable subsets of $A$.

Now suppose someone asks you to show that $3^\mathbb{N}$ and $5^\mathbb{N}$ are isomorphic. If you are classically trained you might say: “They are isomorphic because they both have the cardinality of continuum.” That’s a quick and dirty proof. But then you are asked to show that $3^\mathbb{N}$ and $5^\mathbb{N}$ are isomorphic as topological spaces, and you have to think again. You could construct an actual homeomorphism, although any self-respecting topologist will notice that both spaces are “compact, countably based, 0-dimensional Hausdorff spaces without isolated points, therefore homeomorphic to the Cantor space by a well-known theorem”. That’s the kind of answer I would expect from my topology friends. And when you are done with that, you will be asked to show that $3^\mathbb{N}$ are $5^\mathbb{N}$ are computably isomorphic, so you will have to think again. Can we not have a single proof which works in all three cases?

To find such a proof, you should forget heavy weapons from set theory and topology, and just look at the sets involved. How they are constructed will tell you what tools to use in your proof. The spaces $3^\mathbb{N}$ and $5^\mathbb{N}$ are exponentials, so we should use $lambda$-calculus! Recall the exponential laws, where I write equality in place of isomorphism,

• $(A \times B)^C = A^C \times B^C$ and
• $(A^B)^C = A^{B \times C}$.

The isomorphism $i : (A \times B)^C \to A^C \times B^C$ and its inverse $j$ may be written down explicitly, for example in Haskell:

i :: (c -> (a,b)) -> (c -> a, c -> b)
i f = (fst . f, snd . f)

j :: (c -> a, c -> b) -> (c -> (a, b))
j (g, h) c = (g c, h c)


I will leave the pair of isomorphisms for the other exponential law as an exercise. There are other isomorphisms which are good to know about (where again we write equality instead of isomorphism):

• $A^0 = 1$, $1^A = 1$, and $A^1 = A$,
• $A^{B+C} = A^B \times A^C$,
• $(A+B) \times C = A \times C + B \times C$,
• $\mathbb{N} = 1 + \mathbb{N} = 2 \times \mathbb{N} = \mathbb{N} \times \mathbb{N} = \mathbb{N} + \mathbb{N}$.

You should write down Haskell functions which witness these. The laws are easy to remember and use because they look like the usual laws of arithmetic. In fact, there is a deep and fascinating connection between the laws of bicartesian closed categories and arithmetic.

Here is how we can compute with exponentials:

$5^\mathbb{N} = 5^{1 + \mathbb{N}} = 5^1 \times 5^\mathbb{N} = 5 \times 5^\mathbb{N} = 4 \times 5^\mathbb{N} + 1 \times 5^\mathbb{N} = 4 \times 5^\mathbb{N} + 5^\mathbb{N}$,

therefore

$5^\mathbb{N} = 4 \times 5^\mathbb{N} + 5^\mathbb{N} =4 \times 5^\mathbb{N} + 5^{1 + \mathbb{N}} = 4 \times 5^\mathbb{N} + 5 \times 5^\mathbb{N} = 9 \times 5^\mathbb{N}$

and now

$5^\mathbb{N} = 5^{\mathbb{N} \times \mathbb{N}} = (5^\mathbb{N})^\mathbb{N} = (9 \times 5^\mathbb{N})^\mathbb{N} = 9^\mathbb{N} \times 5^{\mathbb{N} \times \mathbb{N}} = 9^\mathbb{N} \times 5^\mathbb{N} = 45^\mathbb{N}$.

This is fun, but how is it helping us to show that $3^\mathbb{N} = 5^\mathbb{N}$? Well, if we could also show that $3^\mathbb{N} = 45^\mathbb{N}$ we would be done. Indeed,

$3^\mathbb{N} = 3 \times 3^\mathbb{N} = 2 \times 3^\mathbb{N} + 3^\mathbb{N} = 2 \times 3^\mathbb{N} + 3 \times 3^\mathbb{N} = 5 \times 3^\mathbb{N} = 5 \times (3 \times 3^\mathbb{N}) = 15 \times 3^\mathbb{N}$,

and now we finish off the proof:

$3^\mathbb{N} = (3^\mathbb{N})^\mathbb{N} = (15 \times 3^\mathbb{N})^\mathbb{N} = 15^\mathbb{N} \times 3^{\mathbb{N} \times \mathbb{N}} = 15^\mathbb{N} \times 3^\mathbb{N} = 45^\mathbb{N}$.

Because we only used the basic exponential laws which are witnessed by constructive functions (Haskell programs, if you wish) they hold constructively. This immediately tells us that:

• the sets $3^\mathbb{N}$ and $5^\mathbb{N}$ are in bijective correspondence because constructive mathematics is consistent with classical set theory,
• the topological spaces $3^\mathbb{N}$ and $5^\mathbb{N}$ are homeomorphic because constructive mathematics is consistent with the assumption that all maps (hence also the isomorphisms involved) are continuous,
• the isomorphism between $3^\mathbb{N}$ and $5^\mathbb{N}$ are computable simply because they can be written down in Haskell (or any other decent programming language).

I must admit to a little bit of cheating. I chose $3^\mathbb{N}$ and $5^\mathbb{N}$ because they can both be manipulated to $45^\mathbb{N}$. If you try to show $2^\mathbb{N} = 3^\mathbb{N}$ you will be probably get stuck; if not, show me how!

Let us think  about the general question of how to show that $m^\mathbb{N} = n^\mathbb{N}$ for $n, m \geq 2.$ We certainly expect this to hold, but what is the “best” proof? One idea is to first show that $m^\mathbb{N} = m^\mathbb{N} + m^\mathbb{N}$, from which it quickly follows that $m^\mathbb{N} = n \times m^\mathbb{N}$ and $m^\mathbb{N} = (n \times m)^\mathbb{N}$. But what is the slickest way to get $m^\mathbb{N} = m^\mathbb{N} + m^\mathbb{N}$?

For which $m$ and $n$ does my trick work? Observe that

$m^\mathbb{N} = (m-1) \times m^\mathbb{N} + m^\mathbb{N} = (m-1) \times m^\mathbb{N} + m \times m^\mathbb{N} = (2 m – 1) \times m^\mathbb{N} =$
$= (2 m – 2) \times m^\mathbb{N} + m \times m^\mathbb{N} = (3 m – 2) \times m^\mathbb{N}$

and by applying this procedure $k$ times we get

$m^\mathbb{N} = (k m – k + 1) \times m^\mathbb{N}$

from which it follows that

$m^\mathbb{N} = (m^\mathbb{N})^\mathbb{N} = ((k m – k + 1) \times m^\mathbb{N})^\mathbb{N} =$
$= (k m – k + 1)^\mathbb{N} \times m^{\mathbb{N} \times \mathbb{N}} = (m (k m – k + 1))^\mathbb{N}.$

My trick can therefore show that $m^\mathbb{N} = n^\mathbb{N}$ provided there are $k$ and $j$ such that

$m (k m – k + 1) = n (j n – j + 1)$.

This is a linear Diophantine equation in $k$ and $j$:

$m (m – 1) k – n (n – 1) j = n – m$.

It has a solution if, and only if, the greatest common divisor of $m (m – 1)$ and $n (n – 1)$ divides $n – m$. It is easy to find pairs $(m,n)$ for which there is no solution, e.g., $(m=2,n=3)$, $(m=3,n=7)$, $(m=4,n=9)$, etc.

Perhaps someone can come up with a different trick that always works. Remember, you are only supposed to use the general laws that hold in bicartesian closed categories, for details see the paper “Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types” by Marcelo Fiore, Roberto Di Cosmo, and Vincent Balat.

## 28 thoughts on “Constructive gem: juggling exponentials”

1. It’s a bit hard to write the $A^0 = 1$ isomorphism in Haskell, since there’s no empty type. What would you use in its place?

2. Here’s a little presentational suggestion. It sounds rather technical and boring to phrase things as “whatever implies law of the excluded middle”, because few of those you’re trying to reach know or care what the “law of the excluded middle” is, or maybe even think it’s trivially valid (because of the usual truth table interpretation). It might be more informative to re-state this ever so slightly as “whatever implies that all propositions are decidable”, which is more self-evidently meaningful, because it avoids jargon, and is more self-evidently absurd, because obviously not all propositions are decidable. The point is that LEM involves both disjunction and negation, which have decidedly different meaning constructively than classically, so the formula itself is misleading. Instead, express the semantics of it directly.

3. augustss says:

You can define an empty type in Haskell. Of course, it’s not really empty since there’s always bottom. But, e.g., the () type also has an extra bottom element. For this kind of reasoning it’s convenient to ignore bottom.

4. Chris, that’s a good point. In fact, there is a problem with disjoint sums, too. In Haskell not every element of $A + B$, or Either A B as it is written in Haskell, is of the form Left x or Right y, because the diverging value is from neither. Haskell does not really have disjoint sums in the sense of category theory.

There are several options. The cleanest one is to switch from Haskell to Agda, which has the empty type.

Another one is to limit attention just to the total elements of types, and just ignore the diverging programs. And I thought there was a way to declare an empty type using the “-XEmptyDataDecls”. Of course, the empty type will not be empty, as it will still contain the diverging program, but that’s ok since we’ll just ignore it.

5. Bob (2): Thanks for the idea. I suppose computer scientists really do understand “all propositions are decidable” better than “the law of excluded middle”. On the other hand, this really is just terminology, since the law of excluded middle states exactly that all propositions are decidable: $\forall p \in \Omega, p \lor \lnot p$.

6. Ryan Ingram says:

$\mathbb{N} \times \mathbb{N} = \mathbb{N}$ is a non-trivial function to write. I assume you use the usual diagonalization for the pair?

7. Ryan Ingram says:

Chris: I did this:

{-# LANGAUGE EmptyDataDecls #-}

data Zero
zero_elim :: Zero -> a
zero_elim _ = error "zero_elim"

Then use zero_elim where necessary:

exp_0 :: (a :^ Zero) :=: One
exp_0 = Bi (const ()) (\() -> zero_elim)

8. Ryan Ingram says:

I ended up using the bitwise pairing function described here: since it is easy to implement using the $\mathbb{N}=2 \times \mathbb{N}$ equality that strips off the bottom bit.

9. david karapetyan says:

This is pretty cool.

10. Pseudonym says:

You can also construct set isomorphisms such as this in lambda calculus with the fixpoint operator using the proof of the Cantor-Bernstein-Schroeder theorem, but unfortunately you can’t use it as a proof (because of nontermination).

11. Here’s another way to represent the empty datatype:

data Zero = Zero (forall a. a)

In this way it is still not possible to construct values but at least you can use Zero’s field as absurd pattern when pattern matching on it:

zero_elim :: Zero -> a
zero_elim (Zero x) = x

I like this one better, partly because you don’t need to use undefined (or error).

12. Colin McQuillan says:

Perhaps your construction provides the only relations (and any other homeomorphisms that can be derived, for example $7^\mathbb{N} = 55^\mathbb{N} = 5^\mathbb{N} \times 11^\mathbb{N} = 3^\mathbb{N} \times 3^\mathbb{N} = 3^\mathbb{N}$. None of the allowed operations seem to provide a way to get from $2^\mathbb{N}$ to an odd number.

What is the abstract motivation for not allowing recursive definitions? If you just want to show that $2^\mathbb{N}$ is computationally isomorphic to $3^\mathbb{N}$, you could use Huffman encoding. It is interesting as a puzzle, and computationally the homeomorphisms could provide a base-3 infinite array given infinite binary random-access memory with $O(1)$ reads and writes.

13. The motivation for not allowing recursive definitions is that a proof which only uses the exponential laws and the laws for products and disjoint sums holds in any bicartesian closed category.

There is the option to use coalgebras, since the exponentials are also final coalgebras. That would probably get us further.

14. Pseudonym says:

Andrej, the Cantor-Bernstein-Schroeder theorem states that if there is an injection from A to B and an injection from B to A, then there is a bijection between A and B. The proof is completely constructive.

15. Pseudonym, I am pretty sure this is not the case, please provide a reference. For example, the proof on Wikipedia is not constructive because it tacitly assumes that A = C \cup (A \\ C), see the proof for details. Beware, classical mathematicians sometimes use the phrase “constructive” when they mean “no use of the axiom of choice”.

16. “2^A is not generally isomorphic to Omega^A=P(A), the powerset of A.”

Does this mean that the powerset of {0} has more than 2 elements? If yes, this should be another stone….

17. Sridhar Ramesh says:

In response to Pseudonym, the Cantor-Schroeder-Bernstein theorem cannot be constructive in the relevant sense (e.g., provable in impredicative higher-order intuitionistic logic, the internal logic of topoi): it’s possible to construct topoi in which all functions from reals (suitably constructed) to reals are continuous, but clearly the intervals (0, 1) and [0, 1] both admit injections into each other, while there can be no continuous bijection between them. [A similar argument could be made using a suitable subset of N and the intuitionistic consistency of the principle that all functions from N to N are computable].

18. Sridhar Ramesh says:

(Also, you could use the more sophisticated example from the more recent post on this very blog: in one of those non-trivial topoi where all functions are continuous [in a suitable sense], we have that $\mathbb{N}$ is isomorphic to $2^{2^\mathbb{N}}$, and thus the injections from $\mathbb{N}$ into $2^\mathbb{N}$ and back into $2^{2^\mathbb{N}} = \mathbb{N}$ present a counter-example to Cantor-Schroeder-Bernstein [$\mathbb{N}$ continuing, by Cantor’s Theorem, to be non-isomorphic to $2^\mathbb{N}$].

19. Sridrah, why is it “clear” that there can be no continuous bijection between (0,1) and [0,1]? I think it’s not clear at all. After all, in the effective topos there is a continuous surjection from [0,1] onto (0,1)…

20. Sridhar Ramesh says:

Sorry, I should not have said “continuous bijection”, but rather, continuous functions which are inverse to each other; i.e., a homeomorphism. Is it not true that there can be no homeomorphism between [0, 1] and (0, 1)?

21. Showing that [0,1] and (0,1) are not homeomorphic does seem easier than showing there is no continuous bijection from one to the other. We’re constructive here, so we just have to make sure we don’t use a classical fact. I don’t see a very easy argument at the moment.

22. Sridhar Ramesh says:

Of course, in a topos where all functions are continuous, the two (bijection and homeomorphism) amount to the same thing. Anyway, that (0, 1) and [0, 1] are non-homeomorphic should follow from the fact that every point in (0, 1) is a cut-point, while the two endpoints of [0, 1] are not. [In satisfying myself of the last line, I invoke near-trichotomy principles like (p != q) => (p < q or p > q) whose validity I suppose could vary from particular construction/notion of reals to particular construction of reals, but I’d be shocked if the argument couldn’t be ultimately made to go through for any natural notion of reals or real-like quantities].

Anyway, going back to what this was all originally being used for, the specific example of (0, 1) and [0, 1] isn’t essential; I gave other, non-topological examples above of how to make the same ultimate point (about intuitionistic failure of Cantor-Schroeder-Bernstein), but even sticking to the topological approach, we can use (0, 1) and (0, 1) U (2, 3) instead, if it makes life easier. Clearly, each of these injects into the other, and clearly, they cannot be homeomorphic (the former is connected, the latter is not).

23. I took the liberty to edit your post and fixed the broken math. Yes, I agree that ultimately we can show that [0,1] and (0,1) are not homeomorphic, constructively, but for our purposes it is easier to just take your example (0,1) vs (0,1) union (2,3). By the way, it is interesting to think about what “connected” means constructively, and which of the several notions of connectedness (0,1) satisfies.

24. Sridhar Ramesh says:

(One tiny comment just for the sake of not leaving errors unremarked upon: I did make one mistake above in post #21: I asserted that the situations where N is isomorphic to 2^(2^N) were another class of intuitionistic counterexamples to CSB. But in doing so, I invoked an injection from 2^N into 2^(2^N), which needn’t exist intuitionistically; indeed, in the relevant cases, it generally won’t)