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.
No comments:
Post a Comment