Curry-Howard for Non-Dummies – Part 3

In Part 2, we considered the implication A → ⊥, saw that in the logic of the original formulation of Curry-Howard (known as Intuitionistic Logic for those who care) it was equivalent to asserting that A had to be an empty type. We also speculated that in some other interpretation, A → ⊥ might be the type of a program that never terminates. We’ll see if we can make this idea useful in a moment.

Double Negation

But first, let’s consider the type ¬¬A, which, using the formulation described in Part 2, expands out to (A → ⊥) → ⊥.

In the normal Boolean logic that most programmers will be familiar with, if you negate a false value, you get a true value. (This kind of logic is Classical Logic.) One way to define this property is to say that there is a program with this type: ¬¬A → A in whatever programming language corresponds to Classical Logic.

But in the logic we have been using so far this won’t quite work. As mentioned at the end of Part 2, we need to show that A comes from some place on the left side of the arrows. Since it isn’t made clear in this type, it won’t work for us. We can fix this by rearranging the expression so that A appears on the left side, which means that we can build a program of the type A → (A → ⊥) → ⊥.
To see that this is so, there are two cases to consider.
The first is if A is an empty type. Then we are back to a case like ⊥ → B;, where the program is never going to get any input and so it doesn’t really matter what is on the right side. If A is a type with members, then we already know that the type A → ⊥ is empty, so the second part of the program is just the same as the ⊥ → B; case. So either way, we can build this program using the rules we were already using.
Now let’s consider what we need to add in order to make the Classical Logic rule work.

Classical Logic

In order to get the behaviour we expect from Classical Logic, we need to be able to do something that we just showed is not possible for our previous programming rules. We need to be able to build a program that fits the description of the proposition type ¬¬A → A, which expands to ((A → ⊥) → ⊥) → A.
To be able to build such a program, we need to have a typing scheme that is a little bit less strict than the one we’ve been using – one that is willing to “wait and see how things turn out” before fully assigning type. It needs to be able to risk that the program might not terminate and, to really fulfill the proposition type, it needs to be able to make sure that we always end up with a definite value regardless of what actually happens.
In this sense, Classical Logic is the logic of perfect information, where you always have enough knowledge to see what is true and what is false, and you can always stop things when they go awry to make sure they turn out in the end.
There are two ways to ensure that you have this kind of knowledge and power: the first is to always deal with a world that is “small enough,” so that you can always find out the truth of things in a reasonable amount of time. For example, if we restrict our purple unicorn-finding program to looking for it in the room we happen to be in at the moment, then we can be sure that we will either find a purple unicorn or definitely not find a purple unicorn in a finite amount of time.
The second way to ensure the Classical Logic rule is to work in a “arbitrarily big world” with “magic powers” that allow you to find out the truth of things even when they are impossible. An example of this would be to have a “Halting Oracle”, a magic detector that will tell us whether our program will eventually terminate or not.
It turns out that there is a particular type of program that meets the description of the proposition type ¬¬A → A. It falls somewhere between the “small enough” and “magic power” solutions and is known as a “continuation”. This kind of program basically allows you to abort a program and return a value anyway. You can think of a “return” statement or an exception as a poor-man’s continuation. In principle, the program that you abort could have been non-terminating, but you get to see this and abort it to make sure it turns out anyway. The “seeing this” part is outside of the system itself, so it is sort of a magic power, but in practice we rely on the fact that we are working with a small enough world that the programmer can see what would happen and choose to abort the computation.

Searching for Purple Unicorns

Let’s return to our program that uses a spy satellite to search for purple unicorns.
Will it run forever or will it terminate? If we stick with our constructive method of building facts, then it will only terminate if in fact purple unicorns exists and it finds one. Unfortunately, there are ways that purple unicorns could in fact exist, but our program still won’t terminate: for example, if during the day purple unicorns hide in caves and at night when they come out it is too dark for our satellite to spot their particular shade of purple. Unfortunately, in this case our program doesn’t really fulfill its type and it doesn’t really prove anything at all, one way or the other.
If we avail ourselves of the Classical approach to things, we can make our program terminate even if there aren’t any unicorns by, say, allowing the satellite to do one orbit and then just assume that we were right to begin with that they don’t exist and abort the program with a negative result. This basically forces truth into a box we find convenient and doesn’t really prove anything either. It is just a fancy form of axiom.
Another option is to not worry about being able to reify our ideas and proofs as programs, assume that purple unicorns exist and develop elaborate theories about their habitat, physiology and behaviour. These might be interesting theories and some of them might be true and consistent with the real world because, by the way we have defined them, we know quite a lot about them. For example, we know that unicorns very horse-like, so many things that are true about horses can be comfortably said to also be true about purple unicorns. We can also assume that their characteristic purple is a known shade of purple. In this way, theories of purple unicorns might we’ll be perfectly compatible with existing zoological studies, or colour theory. Assuming the impossible does not necessarily produce inconsistency.
Medieval scholastics were able to do some good logic, rhetoric and philosophy by contemplating things that most of us think are impossible, such as angels dancing on the head of a pin.

Implications for Mathematics

Curry-Howard gives us a possible definition for truth in mathematics linked to computation. At this point in time, most mathematicians don’t seem all that interested in this possibility, since they are fond of studying purple unicorns, such as the kind known as “uncountable sets”. I don’t really want to dissuade them from this study, anyway. Purple unicorns are fun to think about, and can sometimes provide inspiration for useful things. (See continuations above.)
However, both mathematicians who work with computer science and computer scientists who have Classical mathematical training need to be very careful how they think about computational truth: it doesn’t work the way they are used to.

Implications for Logic

Curry-Howard gives us a reason to explore logics that are subtler or more complex than Classical logic. Computation requires us to incorporate a notion of uncertainty into our thinking, and logics that can handle this might offer new vistas of useful thought to explore. Lots of great work has been done this way.

Implications for Computer Science

Curry-Howard reminds computer scientists that we are not afforded the luxury of either believing in purple unicorns or being too certain that purple unicorns don’t exist. Infinity is a big place after all, and our programs can’t explore all of it.
Curry-Howard also gives us a tool to draw inspiration from what logicians and mathematicians are doing to better understand how to think about computation. We need all the tools we can get.

I hope that any brave soul who worked all the way through to the end of this has gleaned an understanding of Curry-Howard, and an appreciation for the rich, cross-pollination of disciplines that it enables.