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.

Curry-Howard for Non-Dummies – Part 2

In Part 1, I described the “Curry-Howard” principle in very simple terms. I culminated with the explanation that a program can be seen as a proof of the implication represented by A → B, where A is the type of its inputs and B is the type of its outputs. Moreover, A → B is itself both a type and a proposition in a simple implicational logic.
And that’s all well and good, but now it’s time to see some wrinkles in this idea in preparation for exploring the consequences of Curry-Howard upon mathematics, computer science and logic in Part 3.

What Happens When a Program Doesn’t Terminate?

In Part 1, you may have noticed that I made a bold assumption about my programs. The rationale for considering the program to be a proof of the implication was that I was able to run the program by consuming a thing that met the description of an A and produce a thing that met the description of a B. My program is a proof by construction.

But what happens if I made a mistake and wrote a program that doesn’t terminate for all inputs that meet the description of an A?

Let’s return to the example where the description of A is “a purple unicorn” and the description of B is “a horse-race winner”. Let’s say I decide that what I’ll do is create a new program whose input C has the description “a spy satellite in orbit” and I conceive a program for the implication C → A that says that I’ll have the satellite orbit the Earth, checking every square inch of it until it finds a purple unicorn, at which time it will let me know its location, and I’ll go capture it. Once I have this purple unicorn, I will immediately pass it to my previous program as input and will then be able to produce a horse-race winner. We can think of the composition of these two programs together as a new program that is a proof of the implication C → B. But are we sure this works?
It could be that there is such a thing as a purple unicorn after all, and that it just so happens that no one has ever seen one and that our spy satellite, which is very thorough, will do its job and find a purple unicorn that was previously missed. In this case, we would have a proof of C &arr; B. But maybe there really is no such thing as a purple unicorn (on the surface of the Earth, anyway), and our satellite will just circle the Earth forever.
In this latter case, I have a fully described program that would take a spy-satellite and produce a horse-race winner, but if I try to run it, it basically hangs up on the first step and never completes. So merely having a description of a program is not sufficient to have a proof. What I really need is the description of a program that is guaranteed to terminate for all its allowable inputs.

So does this mean that a potentially non-terminating program has no place in a Curry-Howard view of things? Is there not still some value to having some well-defined program that witnesses an implication, as opposed to having no proof at all of the implication, except perhaps “because I said so?”.
To tackle this, we must expand our repertoire of concepts a bit.

Negation

In Part 1, I covered how we can define the truth of the proposition represented by a type as the existence of a thing that meets its description. If the description of A is “purple unicorn” and I can present a purple unicorn, then A is true, and if there is no purple unicorn to be found, then A is false.
So any type that is false must have no possible members. If you think about this a moment, then you realize that any two types that are false must share the same list of members, i.e. none. This means that they share the same extensional definition. And by the same token, the members of both types will all meet the description “a thing that is impossible”. So they also share an intensional definition.
In this sense, all empty types are equivalent to a single basic empty type, which we will give as a name the symbol ⊥. This symbol can be pronounced a number of ways, but we can continue to think about it as “the empty type”.
Is there a way to use this type in an implication to produce interesting types of programs?
An obvious possibility is to put the empty type on the left side of an implication: ⊥ → A. As a program, this would be a program that takes members of the empty type as input. This is very much like our “purple unicorn produces a horse-race winner” program. It is a program that (if we are correct that there are no such thing as purple unicorns) will never get any input (since there are no instances of the input type to pass to it), and therefore it will never produce its output. This doesn’t mean that the type of its output is necessarily empty, just that this function can’t be used to prove anything definitely, or, looking at it from the other end, you could say that this kind of program could prove anything, since a program that isn’t going to run can promise anything you like, since it will never have to deliver. (Just like a politician who knows he won’t be in the next government…)
The next obvious possibility is to put the empty type on the right side of the implication: A → ⊥ . This one is a little bit trickier to make sense of. At first glance, this one might be a good match for our C → A implication, the “take a spy satellite and find a purple unicorn” program. And that has some interesting possibilities. But normally this form of implication is interpreted to mean ¬A, which is an assertion that A is empty and false. To explain how this works, we need to explain a little bit more about the original formulation of Curry-Howard.

The Original Curry-Howard

To understand the original formulation of Curry-Howard, you must understand some basic facts about a couple of things, which have been known to get quite complex but for our purposes are extremely simple. The first is the Lambda Calculus, which is really just the world’s simplest programming language. There are basically two “commands” in this programming language. One allows you to define a program that takes an input, and the other allows you to pass input into a program that has been defined by the first “command”. There are some technical details if you are really interested, but seriously, that is all there is to this.
The amazing thing about this simple programming language is that it is as powerful as any other programming language you could invent. The thing that makes this language so powerful is that you are allowed to pass a program to itself as input. Under certain circumstances, if the program gets applied as part of its own execution, the program might never finish. This is exactly like defining a function that contains only a call to itself: it will just go in circles forever.
Now, there is a limited form of the Lambda Calculus known as the Simply Typed Lambda Calculus, which basically works like the implication types we’ve been talking about. The important thing to know about the types in this programming language is that the description of the inputs and outputs of a program must be simpler than the description of the type of the implication itself. This ensures that you can’t pass a program to itself as input, and this means that all programs in this language always terminate.
To illustrate, consider a simple program that has the type A → A. Since its input is of type A, and since its own type is A → A, which is more complex than simply A, it can’t possibly get itself as input.
The amazing thing about this language is that, despite giving up the most important trick of the full Lambda Calculus (recursion), you can still do quite a lot with it, including a significant portion of arithmetic.
Another important attribute of this language is that it is strictly constructive, which is another way of saying that you can only output on the right side of the implication things that are built up from things supplied on the left side. This ensures that we don’t pull any conclusions out of thin air, and that we can always trace the origins of a particular conclusion from what we started with through the well-defined building steps along the way.
A consequence of this fact means that the implication A → ⊥ can only exist if A is in fact an empty type. This means that the only type allowed to have ⊥ on the right is ⊥ → ⊥. This explains why saying A → ⊥ is the same as saying ¬A., i.e. A is empty and false.

We now understand enough about Curry-Howard to think about some of its consequences, which we will explore in Part 3.

Curry-Howard for Non-Dummies – Part 1

(Anyone who wants to learn is not a dummy)

At the risk of alienating the (small) audience who is used to me writing about not-too-technical topics, I would like to take a crack at an important but technical topic in theoretical computer science. This topic is often known as the Curry-Howard Isomorphism, though there are variations on its name. Despite the forbidding name, the principle it represents is useful to understand for anyone who is interested in logic, computation or programming languages, which would obviously include programmers of all skill levels. I hope to provide an introduction that anyone in this wider audience can understand.

Programs are Proofs

The very basic idea of Curry-Howard is that you can think of a program as a proof. A proof of what? A proof that if you provide certain inputs to that program you can produce the corresponding output.
Another way to think about this is to understand that both programs and proofs are series of rule-following steps that allow you to transform what you started with into a new result.
We often take this generating capacity of programs for granted, but the very nature of programming requires a deep understanding of the structure of inputs, the structure of outputs and the details of the relationships between them. This is exactly the same kind of activity as creating a proof in math or science.

Programs are Implications

In logic, the simplest way to state a proposition that captures this inputs-to-outputs behaviour of programs is as an implication: A → B, ( read as “A implies B”). This means that if I already know that A is true then I will also know that B is true.
To see the parallel to a program, I have to understand that “A is true” is equivalent to “I can find a thing which fits the description of A”.
This last step is perhaps not quite so obvious, so let me give an example. Let’s say that A stands for “a purple unicorn” and B is “a horse race winner”, then A → B could mean that “if I had a purple unicorn I would run it in a horse race, and since purple unicorns are magically fast, I would be sure to win”.
You can see that this is a kind of program: give me a purple unicorn as an input, and I can follow a series of steps to produce a horse race winner.
While this may be a good program, it can’t be run, since purple unicorns don’t exist. And since purple unicorns don’t exist A can’t be true.
If I change my program to match C → B, where C is “a well-bred horse”, I’m back in business: my program can now be run again, when I run it (or rather run the well-bred horse in the race) and produce a horse race winner, I will have proved the correctness of the implication.
To return to a slightly more programmatic example, let’s say that A is “a number” and B “a number greater than A”, and my program adds one to its input. I then feed it “1” as input, my program produces “2”, which is indeed greater than 1, and I’ve proven that, given the number “1” I can produce a higher number.

Types are Propositions

However, we aren’t quite done here. I just showed that for a particular thing that met the description of an A (“a number”) I could get a particular B (“a number greater than 1”), but what I really need to do is show that any thing which meets the description of an A can always be used to produce a B using my program. In order to do this, I need to think a bit more about what it means to be a “thing which meets the description of A or B”.
There are basically two ways to define “things that meet the description of A”: by listing all the individuals that meet the description (this is called an extensional definition) or by proposing a rule (typically an inductive rule) that allows me to produce or recognize an A at will (this is called an intensional definition).
It so happens that we already have a concept in programming languages that does this definitional work for us: types. Types can be defined by an exhaustive list. For example, the character type is typically defined by a list of ASCII or Unicode characters that is fully known already. Types can also be defined by a rule. For example, a number type might be defined as any sequence of digits. You wouldn’t have to list all the numbers (there are probably too many) – you just have to check the simple formation rule to determine membership in the type.
Based on this, we can see that any type can be construed as a logical proposition that can be verified by lookup or by rule: just produce an individual item that meets the description and we know that our proposition is “true”.

The Type of Programs

We now have enough machinery to show that our program works for all of its inputs. We showed that A and B are both types and propositions. We now have to see that the implication A → B is also both a type and a proposition. To meet the description of the proposition A → B we have to show that our program will take any A and produce a B. As with our simple propositions, we need either an exhaustive list or a rule that allows us to cover all the bases. The easiest way to do that is to start with our definition of A. When we look at the structure of our program, we will have to see that there is either an exhaustive list of the elements of A or some rule that follows the rule for A to cover all the possible values of A, and then for each path that results from this rule or lookup, show that a B will result.
This can be very complicated for complex programs but it is often possible to break a bigger program up into smaller bits, each of which can be checked in this manner. Generally programming languages and type systems are designed so that the compiler can verify the type of a program automatically.
When we have completed the process of verifying our program, we will know that our program fulfills the description of the proposition A → B, that it conforms to the corresponding type, and that it is also a proof of that proposition.

If you have followed this far, you have grasped the basic idea of Curry-Howard. It is, I hope, a surprisingly simple idea, but with profound consequences for logic, mathematics and computer science. In Part 2, I hope to expand a bit on some of the elementary consequences.

Why proving that P ≠ NP is hard

A while ago I spent the time to “audit” online a Cambridge University course given by Tim Gowers on computational complexity.

In this course, Gowers takes the students through a proof by Razborov that there is no “natural proof”, for a particular form of the problem, that P ≠ NP, which I found very interesting.

This got me thinking about why this is a hard problem to solve, and I thought it might be useful to explain the intuitive reasons behind it.

So let’s think about this by looking at the Traveling Salesman Problem, since it is a fairly intuitive example of one of the hardest problems in the NP complexity class, known as NP-complete.

In this problem, you have to find the shortest path through a number of cities, visiting each city once and only once. This is a typical NP problem, where the naïve approach to solving the problem would be to just work through all the combinations possible, check the value of that combination (in this case the length), and pick the shortest one.

The problem with that is that the number of combinations gets very large very fast, so it really isn’t practical to do this.

Let me show you what I mean. Let’s take the case where there are 5 cities: A, B, C, D, E. Any path through these cities can be described by a sequence of these letters. For example, CDEAB would be the sequence starting at city C, then going on to city D, etc. To figure out how many combinations there are, I have to use each of the letters once and only once, so there are 5 possible choices for the first slot, four for the second, and so on. This gives me 5x4x3x2x1=5!=120.

In general, this brute force approach to solving the problem, which represents the worst case scenario among solutions, will take n! steps, where n is the number of cities we are considering. This gets very big, very fast. For example 10! is equal to 3628800, so you can see that as you add cities it becomes vastly harder to solve the problem this way.

Now it is very important to realize that this is the worst-case scenario only, or as it is described in mathematics, an “upper bound” on how hard the problem is. For example, if all the cities are in a straight line, you can solve the problem in many fewer steps: just start on one end and move to the next in line and so on
This works because we know that on a straight line, the shortest path will be on that line, so that if the cities are aligned ABCDE, we know right away that we aren’t going to have to consider any of the combinations that don’t follow the sequence on the line. In other words, there is a pattern to the data that allows us to ignore a number of combinations (in this case, all but the two, which are of equal length: ABCDE, and EDCBA).

But to say that some problem is in the class NP (and not in P) is essentially to say that there will always be some collection of cities you could choose that would require you to go through the worst case scenario to find the shortest one. (Technically, the actual worst case scenario for this problem is only exponential in complexity, but that is still pretty bad and doesn’t affect my argument here.)

That is, unless someone can prove that P=NP. This would mean that there was always a shortcut that allowed you to find the solution without having to work through the majority of the possible combinations. And this shortcut would almost certainly involve being able to consistently find some pattern in the data, just as we did with the straight line example, that simplifies the data down to a smaller number of cases.

So in a sense, it should be much easier to prove P=NP than that P ≠ NP. (That no one has proven the former yet is a pretty good reason to suspect that the latter is true, even though no one has proved it either.)

The reason is that to prove P=NP, you just need to show that there is always a pattern in the data that will simplify it, whereas to prove P ≠ NP, you would have to show that there can’t be such a pattern for some scenarios in the problem set.

Why is it easier to show that there is a pattern than that there can’t be a pattern? Well, if you have a pattern, you have a relatively small number of steps needed to describe that pattern, and it is much easer to work through those steps and convince yourself that you have covered all the bases. You can also try your pattern on all the hairiest known instances of the problem and show that they work.

In a sense, having a pattern simplifies the search space required for the proof in exactly the same way that having the pattern simplifies the search space to find the answer to the problem.

But how do you show that there is no possible pattern for some set of data?

Let’s say that I give you a list of digits and tell you that one of two scenarios generated these digits: either I am generating them randomly for each digit as you ask for them, or I am using some relatively simple-to-genarate pattern to generate them. Here is a sample list:

15926535897932384626433832795…

Can you see a pattern? You could do a statistical test on the digits to see if they show the properties of randomness, and in this case, I think you would find that they do show those properties.

So, can you then conclude that they are random?

No, unfortunately not, since there is a pattern here: these are the digits of pi after the well-known first three 3.14…
So the challenge is that you can never really be sure that there is no pattern to some data set; it could just be a really, really unobvious pattern that you haven’t thought of yet.

So you can see how very hard it would be to prove that there is always some configuration of cities that can’t be simplified by some pattern, which is only part of what you would have to do to prove that P ≠ NP.

This is why it is unlikely that anyone will find such a proof unless they can develop some hard-to-imagine technique that allows us to detect when there aren’t any patterns in a set of data.