With apologies to Lewis Carroll What the Tortoise said to Achilles , Douglas Hofstadter Douglas Hofstadter is the author of Gödel, Escher, Back, a book which features many dialogues between Achilles, the Tortoise, and other characters, to illustrate the ideas in the book. , and Philip Wadler Philip Wadler is a Professor of Theoretical Computer Science at the University of Edinburgh.
(Achilles, while walking through the park, approaches the Tortoise, who is sitting on a rock in the sun, near the sidewalk, apparently deep in thought.)
Achilles: Why, hello, Mr. T! It’s so good to see you again!
Tortoise: Achilles! Indeed, it’s wonderful to meet you at random in the park, just as we’d planned not too long ago!
Achilles: I always do my best to keep such appointments. But, how are you? You seem to be deep in thought! Are you contemplating how to destroy new types of phonograph machine?
Tortoise: Not today, Achilles. I am contemplating implications.
Achilles: Hm. I’m not sure I know what you mean.
Tortoise: Well, if you are interested…
Achilles: Always!
Tortoise: Suppose, for example, that we have a proposition, which we’ll call $P$. And we know that if $P$ is true, then $Q$ will be true. We could say that $P$ implies $Q$, which we could write down as $P \to Q$.
Achilles: I’m afraid I’m not much for abstract logic. Can we make this more concrete, somehow?
Tortoise: Why, certainly. Let’s take the concrete of this nearby sidewalk, for example. We could say that if it’s true that the sidewalk is wet, then it is true that it was recently raining.
Achilles: But there could be a sprinkler system in the park, which was recently operating, which made the sidewalk wet…
Tortoise: Well… yes, but let’s assume that there is not, or that if there is, it has been arranged efficiently such that the sprinklers only apply water to the grass, not to the sidewalk.
Achilles: (thoughtfully) Someone may have recently passed by carrying a full bucket of water, which they spilled along the sidewalk…
Tortoise: For the sake of my example, let’s assume that the only way in which the sidewalk could become wet is if it were raining.
Achilles: That’s a very constraining theory. But, very well. If the only way the sidewalk could become wet is if it were raining, I can see that the state of the sidewalk being wet must necessarily imply that it has been raining.
Tortoise: Thank you! Now, surely you might also concede that if it were raining, this implies that there must necessarily be clouds in the sky?
Achilles: That seems a much more sound implication. Yes, if it were raining, I don’t see any way this could have happened without clouds in the sky. (After a thoughtful pause) Unless some sort of specially designed airplane…
Tortoise: (hurriedly) So, in this case, let’s call the proposition the sidewalk is wet, $P$, and it has been raining, $Q$. In turn we will call the proposition it was cloudy, $R$.
Achilles: This is an awkward way to talk about things, but certainly, we could label your propositions that way.
Tortoise: Then we would write our first implication as $P \to Q$, and the second as $Q \to R$.
Achilles: Aha. Now I see better what you were going for with your original talk of implications. Certainly. The sidewalk being wet implies that it has been raining, and it having recently rained implies that it was cloudy.
Tortoise: Exactly! Now, what I have been contemplating is that, from this, we could create a new implication, $P \to R$, that is, if the sidewalk is wet, then it was cloudy recently.
Achilles: (thoughtfully) …Yes… Yes, I see what you are saying. This reminds me, somehow, of something I’ve been thinking about recently, but I’m not quite certain how it relates…
Tortoise: …to finish up, what I’ve been contemplating is that $(P \to Q \land Q \to R) \to (P \to R)$.
Achilles: Fascinating! Again, I feel an uncomfortable feeling of déjà vu.
Tortoise: Perhaps we can figure out why. By the way, I have often heard people talk of this feeling of “déjà vu,” but I have never really felt it myself; how would you describe it?
Achilles: That’s a tough one… It has a certain je ne sais quoi, but I don’t know what it is.
Tortoise: Ah well. Perhaps one day I will be lucky enough to notice it myself. In the meantime, what have you been doing recently?
Achilles: Ah! Well. I would love to talk about that, in fact. I have recently been working out expressions in the simply typed lambda calculus.
Tortoise: Oh my goodness! That sounds terribly esoteric, I’m sure I wouldn’t understand it at all.
Achilles: On the contrary, nothing could be simpler. For example, a lambda, λ, is a function that takes in some argument, and returns a result.
Tortoise: Could you provide an example?
Achilles: Certainly… let’s say we have a function $f$, which can only take in an odd number, such as 1, 3, 5, and so on… $f$ will always multiply this number by two, and so will always return an even number. So if we think of all odd numbers as being some type $P$, and all even numbers as being type $Q$, then we would say $f$ is a function from $P$ to $Q$… we would write down something like $f : P \to Q$.
Tortoise: That’s a nice simple example. Although, it seems to me that such a function should be able to take in any sort of number, but if you say it can only use odd numbers, I will go along with you.
Achilles: It only gets more interesting! We might also imagine we have a function $g$, and that $g$ can only take in even numbers, and its calculation is to square that number by multiplying it by itself, such that it always returns a perfect square, which we might denote by the type $R$.
Tortoise: It seems an odd restriction to have a square function that can only accept even numbers.
Achilles: The world is full of such odd constraints! Similar to your sidewalk which can only become wet when it is raining, let’s assume our square function $g$ can only square even numbers.
Tortoise: Fair enough! What then?
Achilles: Well, what I have been working out is that, if I compose these two functions—$f : P \to Q$, and $g : Q \to R$—I will effectively have a function which accepts a $P$, and returns an $R$.
Tortoise: It seems that your function g will not only always return a perfect square, but specifically the perfect square of an even number.
Achilles: True, but the perfect square of an even number is still in the set of all perfect squares: so the type of $g$ will still be $g : Q \to R$.
Tortoise: That is interesting. And now that you mention it, something about your lambda composition seems somehow familiar to me as well… It’s a sort of… je ne sais quoi…
Achilles: Why, that is strange! I wonder what it could be. Say… what is that, up over there?
Tortoise: (looking over his shoulder) Over there? Why, I think that must be a bird of some kind.
Achilles: I’m not so sure about that. I think it must be a plane. It’s a good thing the sidewalk is not wet, or I wouldn’t be able to see it, due to the clouds!
Tortoise: (still looking, and squinting slightly) I don’t believe it is a bird or a plane.
Achilles: (excitedly) You’re right! It isn’t either—it’s Lambda Man!
Tortoise: … Who in the world is Lambda Man? In several of his conference talks, Philip Wadler has made use of the character “Lambda Man”, a superhero whose costume is reminiscent of Superman, but with a Lambda in the chest logo.
(Lambda Man lands, directly on the path next to the Tortoise and Achilles.)
Lambda Man: I am, indeed, Lambda Man! I was pulled here by the incredible gravity of your conversation!
Tortoise: … I thought it quite a light-hearted little chat, myself.
Lambda Man: Light of heart, yes! But heavy of significance.
Achilles: What do you mean, Lambda Man? Is it my composition of functions in the lambda calculus?
Tortoise: Or perhaps it is my contemplation about implications?
Lambda Man: Yes! Or, rather: it is both! In a manner of speaking. You see, you are both talking about the same thing.
Tortoise: I’m really not sure I see how that’s possible.
Achilles: I don’t think that I see it, either. Unless you are suggesting that wet sidewalks are the same thing as odd numbers, which, while a fascinating proposition on its own, I’m not sure…
Lambda Man: (waving his hand) It’s nothing to do with either wet sidewalks or odd numbers, per se. Tortoise, you began with an implication: $P \to Q$.
Tortoise: That’s quite right.
Lambda Man: And Achilles, you begin with a function $f : P \to Q$.
Achilles: Yes, I do, indeed.
Lambda Man: And, good Tortoise, you then have a second implication: $Q \to R$. And you, Achilles, have a second function: $g : Q \to R$.
Achilles: (brow deeply furrowed) That’s true. Hmmm. That is…
Lambda Man: Tortoise, you then surmised, that if, and only if, you actually had a wet sidewalk—I mean, a $P$—you could then conclude that you also have recently had clouds in the sky. That is, an $R$.
Tortoise: (sitting up a little straighter) Oh. Oh…! Say, you can’t possibly mean…
Lambda Man: And you, Achilles! Once you have composed your functions, say like $λx. f(g(x))$, if you give this new function as an $x$ an actual $P$, that is, an odd number…
Achilles: I will get out a perfect square… I mean, an $R$! Why, it’s really quite similar to—
Lambda Man: “Similar”! My good man, it is much more than similar! It is isomorphic. That is to say, it is in fact the same thing. The propositions of the Tortoise’s implications are the types of your lambda calculus functions! Propositions as types is a paper by Philip Wadler, providing history and several examples of the Curry-Howard isomorphism, and some other correspondences between logic, and programming language and type theory. And the proof of the Tortoise’s implications is the program or implementation of your function composition!
Tortoise: My goodness. If I weren’t already sitting down, I think I would need to sit down now.
Achilles: This is astounding! Do you mean to say that, other than the differences of wet sidewalks, rain clouds, and different types of numbers, we were, in fact, working on the same problem?
Lambda Man: Quite correct!
Achilles: Amazing! This correspondence seems very significant. Why: I think it should have a name. I propose the Achilles-Tortoise Isomorphism!
Tortoise: Indeed! Though I would say that the Tortoise-Achilles Isomorphism also has a nice ring to it.
Lambda Man: I regret to inform you that it already has a name: it is known as the Curry-Howard Isomorphism.
Tortoise: I’m not sure I see the connection between these ideas, the flavorful dishes of the Indian subcontinent, and the actor who portrayed Richie Cunningham on Happy Days, but…
Lambda Man: Different Curry, different Howard! However: that must wait for another time. I sense, not far away, that there is a complex expression in need of normalization! Up, up… and away!
(Lambda Man departs.)
Achilles: (staring in wonder as Lambda Man flies away) …Well. That was quite the encounter. I’m going to have to spend some time contemplating this correspondence between wet sidewalks and odd numbers. I mean, between propositions and types…
Tortoise: …And between proofs and programs. Indeed, that sounds very intriguing… let’s meet again at random in the near future to talk more about this!
Achilles: It’s a date! Do you suppose we will hear from Lambda Man again?
Tortoise: I imagine he must be very busy. But I suppose anything is possible! Until next time, Achilles!