De Morgan’s Laws are (Mostly) Constructive!

Most programmers and anybody with a basic knowledge of logic will have heard of De Morgan’s Laws. They provide an easy way to switch back and forth between “or” and “and” in Boolean logic, which is very handy.

When I was first introduced to intuitionistic logic,  I remember being somewhat scared off it by the statement that De Morgan’s Laws don’t hold in it.  This will make any programmer nervous!

So, it came as a surprise to me to learn that in fact three quarters of the propositions that make up De Morgan’s Laws still hold for intuitionistic logic!

It is interesting to examine why.  De Morgan’s Laws can be broken up into four implications:

1)      (¬ P) ∧ (¬ Q) → ¬ (P ∨ Q)

2)      ¬ (P ∨ Q) → (¬ P) ∧  (¬ Q)

3)      (¬ P) ∨ (¬ Q) → ¬ (P ∧ Q)

4)      ¬ (P ∧ Q) → (¬ P) ∨  (¬ Q)

Of these four implications, only the fourth one fails for intuitionistic logic!

Let’s check.

Case 1) If I have a proof that P is false, and a proof that Q is false than I can’t possibly find a proof that either P or Q is true, by the basic definition of ∨.

Case 2) If I have a proof that P ∨ Q can’t be true, then clearly there is no proof for either of P or Q, by the basic definition of ∨.

Case 3) If I have a proof that P is false, or a proof that Q is false, there can’t possibly be a proof that both P and Q are true, again by the basic definition of ∧.

So far so good.  But here is where things go awry.

Case 4) If I have a proof that both P and Q can’t be true at the same time, that doesn’t tell me for sure that I have proof that either one in particular is false.  They just can’t both be true.   So case 4) isn't guaranteed to always be true, and therefore isn't a law after all.


However, if I find a definite proof that one of P or Q is true, I can still conclude that the other is false.  This can be formalized as:

      4')      ¬ (P ∧ Q) → P → ¬ Q

So even this fourth case, with a small caveat, still contains a lot of useful information. Maybe we can say that De Morgan’s Laws are more than three quarters constructive!

The moral of the story is not to be scared away by constructive (i.e. intuitionistic) mathematics: more of the familiar rules still work than you might think, even if you have to be a bit more careful around the edges.

The Intuitive Minority

Many people are skeptical about personality typing systems. Some complain about their over-generality.  Others simply dislike being categorized.  Personally, I have found them very useful for thinking about my own patterns of behaviour. They also help me to understand a person whose style is different from mine, and might otherwise be mystifying.

One of the most commonly used personality typing systems is the Myers-Briggs Type Indicator (MBTI) .  It has four parameters with two settings for each: Extraversion vs Introversion (E vs I), Sensing vs Intuition (S vs N), Thinking vs Feeling (T vs F), and Judging vs Perceiving (J vs P).  Each personality type is composed of four letters, one from each pair.  For example, I am an ENTJ (Extraversion-Intuition-Thinking-Judging).

I want to focus in on one of these pairs, Sensing vs Intuition (S vs N).  If you take a look at MBTI type statistics, you will notice that most of the pairings are pretty close to 50-50, with a little bit of skew for T vs F and J vs P, but that there is a very noticeable bias in the S vs N category: 75% of the population are Sensing (S).

With a majority that big on the other side of the divide, it is pretty much guaranteed that anyone in the N camp is going to be perceived as slightly odd relative to the personality norms of society.  If you add N and T together, you get the NT temperament (sometimes known as “Rationals” ), which make up less than 10% of the population.  It is not surprising that some members of this group (especially the introverts) have sometimes been stigmatized as “nerds” by the majority.

The summary explanation of N vs S characteristics is this: the N is more oriented toward abstract ideas, the big picture, the past, the future and general theories of things.  If you need proof that I’m an N, this blog is proof enough: it is characteristic for an N to lump together superficially disparate areas such as, for example, philosophy, software development, and personality system, while presenting them as a coherent subject matter.

The S is a more concrete thinker, deeply rooted in their own direct experience, present circumstances, the nitty-gritty.  They tend to characterize particular things by visible attributes.   They tend not to like the kind of vague categorizations that Ns prefer.  My experience is that S types don’t think that much of personality type systems, except as a kind of game or as handy stereotypes, since they don’t really think in terms of systems and tend to be annoyed by generalization that goes beyond their experience.

Steve Jobs, whose recent passing has caused such a vast cultural effect, was almost certainly an N.  He saw beyond the current situation, persisted through some difficult times (such as the early days when Macs had a very small market share and his NeXT years) by focusing on what could be.  Ironically, he also now appeals to Ss since his vision has become concrete and present in their lives in an obvious way: an S does not argue with clear and present success.

In some ways, I think it makes sense that most people are S.  Paying attention to the here and now pays off more regularly, even though it has less potential to pay off big the way truly original and disruptive vision can.  Intuition is a high risk/high reward proposition. The conditions that make it pay off are more remote and less certain, but the advantage of being ahead of the game when change comes can be enormous.  A society without N would never progress, but a society with too much N might change too fast or fly off in too many directions.

As an N, I have found that understanding that most people don’t think like I do makes me a more effective communicator in practical situations.  For example, when I detect the tell-tale signs of scepticism or confusion when I’m explaining an idea or plan to someone, I find that giving concrete examples with illustrative detail is often a good place to start. (This can help communicate with Ns as well, since another N might want to detect the patterns for themselves in your data.)  When talking to an S, the trick is to choose examples that aren’t too different, to add in “irrelevant” detail for each, and then point out what the shared relevant details are that make the pattern.

To give an example, let’s say you want to make a point about luxury sports cars.  This is a simple enough abstract category that it likely won’t cause much communicative difficulty, but it would nonetheless be more effective to give a specific example, such as mentioning a Porsche, or even a better, a specific model, such as Porsche 911.  The extra detail, which can seem arbitrary to an N, helps to anchor the idea more concretely for an S.  An N’s instinct is to leave the question open, since the particular model doesn’t matter to the point, but for the S choosing an appropriate example with the right specifics does matter.

The flip side of this technique can be used in rapport building or social conversations when you find that the person you are speaking with is giving a lot of specific detail.  Instead of getting bored and tuning out, it can be helpful to pick out a particular detail that sounds interesting to you and ask for more context about it.  To pick up on our previous example, suppose an S is discussing sports cars, most likely mentioning a specific make, the Porsche 911.  You can ask the S what makes that particular make better/worse/special, depending on the context.  To make this more meaningful, you could provide a different specific make as a comparison example.  This helps to make the detail relevant to the N, while also engaging the S in a mode of conversation that is comfortable.

Careful observation of such interactions will lead to better results and more techniques.  Armed with knowledge of this phenomenon, I hope all Ns will learn to better cope in a world in which they are a minority.

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.