I've been a fan of Spike Lee's movies for a long time, and I still remember seeing his "Malcolm X" in the theater.
Though it may seem like an odd thing for a white guy, I left that theater an admirer of the icon of Black Power who would later choose the name Malik El-Shabazz, and earn the honorific El-Hajj.
And it wasn't just the universalist El-Shabazz I admired, the one who had given up his anger and hatred against me and my kind, but, in part thanks to the brilliance of Lee's movie-making, I also learned to admire, and appreciate the necessity for, his time as "Malcolm X", when he would have been perfectly happy to call me a "white devil" to my face.
When you believe passionately that diversity is a strength and an enhancement to the quality of your life, when you feel that you are "one of the good guys" reaching out in friendship, the venomous rejection that X and the Nation of Islam were spewing out is very hard to take, even if you recognize the justice of the grievances that inspired it. It isn't easy being told "We don't want you here" when you feel you are on the same side.
But I learned through Spike Lee and Malcolm X that the "white devil" message was not about me, and not for me. In a way, it was none of my business.
It was about purging the internalized sense of inferiority, shame, and envy that had been instilled by centuries of domination and abuse. The truth is that equality is not conferred by others: it needs to grow and become firmly established within first. Once it is there, others can accept it or not, but then that is THEIR problem.
Centuries of collective, and decades of personal, anger and hurt had to be vented, processed, and transcended before El-Shabazz could emerge, equal not because someone else (or some document) told him he was, but because he just was, and knew it as surely as he knew his own freely-chosen name.
Another important thing I admired about Malcolm X, and the Nation of Islam, were the discipline and focus they brought to their activities, and while the message may have sounded vitriolic, they stopped short of actual violence. This is not a trivial accomplishment, and it makes all the difference.
Recently, it has come to my attention that I need to relearn the lesson that Mr. Lee and El-Hajj El-Shabazz were kind enough to teach me over twenty years ago.
In my larger professional community of software developers, there are new groups with real historic grievances, and they are getting to the point where they too want to sit at the table without having to apologize for who they are. I've been fortunate to work in environments with a lot of diversity, and I welcome more of it enthusiastically.
But some of these aggrieved groups are working through the anger and hate built up from their long suppression, from the mistreatment they have received from our industry and society at large. And sometimes what they say and do makes me uncomfortable, seems to target me or seems to contravene the values of diversity as I understand them.
As I said, this can be hard to take. But maybe I have to remember the lesson of Malcolm X: it's not about me, and it is not for me. In a way, it's not even my business.
Rather than taking offense, or speaking up, maybe the best thing I can do is LET them hate my male, white, hetero, cis, middle-aged ass.
If it gets too much, I can look away, ignore it, bite my tongue, live my values in some other way. Short of actual violence, or the genuine threat of it, maybe I need to let them express themselves, however they like, until they've worked it through.
Diversity is one of MY most deeply-held values, and no one said that living your values was going to be easy (actually, I'm pretty sure that it being hard and doing it anyway is how you know it really is a value). I will continue living that value, even if sometimes it is rejected by those I'm reaching out to.
Perhaps the best I can do is to continue to be a SILENT ally, and to be ready, when they have worked through all that anger, when they are healed, to welcome them as the friends, colleagues and siblings in the universal family that I already know them to be.
September 21, 2013
September 5, 2012
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
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.
Labels:
Mathematics
November 9, 2011
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.
April 25, 2011
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.
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.
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.
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.
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.
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.
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.
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.
Labels:
Computer Science
Subscribe to:
Posts (Atom)