The History of Categorical Logic

I'm currently making my way through Jean-Pierre Marquis and Gonzalo E. Reyes' 116-page-long The History of Categorical Logic, and it is fascinating. Someone needs to make it into a comic book. [HT: This Week's Finds]

What is the logic of ML values?

Before approaching the question, "What is the logic of ML values?", I first want to explain why there is more subtlety to the question than is often assumed.

(Warning: this is a long post on something which most people probably care very little about. On the other hand, there are 19 google hits for "logic changed my life".)

In general, how does one interpret the question, "What is the logic of X?", for some programming language X? A standard response is that the logical theorems are exactly the inhabited types, i.e., types τ such that there is a closed term t:τ. But what are the "terms"? The answer is obvious enough in simple formal systems where there is only one typing judgment, and so we can say things like, "The inhabited types of simply-typed lambda calculus are exactly the theorems of minimal implicational logic". Yet, real programming languages usually have many different typing judgments, since programs are composed out of many different syntactic objects. In ML, in particular, a program includes some let-bound values and expressions, some function definitions, and a result expression (in addition to datatype definitions, module definitions, etc., which are classified by different kinds of "types").

(In this post, "ML" is meant in a slightly fuzzy but essentially unambiguous way, as a call-by-value language with effects. To settle a concrete interpretation, I will be giving examples in Standard ML of NJ, which notably provides the control operator callcc. "Value" is meant in the standard operational sense, i.e., a value is a fully evaluated ML expression. We can similarly ask, "What is the logic of Haskell values?", but that is a different, trickier question, to which I'm still not sure of the answer.)

When answering the question, "What is the logic of ML?" (or "What is the logic of Haskell?"), the standard approach is to gloss over these different syntactic categories, and assume we are talking about expressions. This makes some sense, insofar as this is the largest syntactic category: all values and functions are also expressions. And expressions also have easy-to-understand principles of composition. For example, the rule of application—from two expressions e₁:σ→τ and e₂:σ, we can form the expression (e₁ e₂):τ—witnesses the logical principle of modus ponens. Whereas from two values v₁:σ→τ and v₂:σ, the application (v₁ v₂):τ is no longer a value.

Yet, I believe it is a mistake to define "the" logic of a programming language in this way, without realizing there is finer structure. That is why I phrased the question, "What is the logic of ML values?", rather than full-stop, "What is the logic of ML?" And so how does the logic of ML values differ from the logic of ML expressions?

Well, it is often claimed that ML (and likewise Haskell) defines an inconsistent logic. This is a statement about the logic of expressions. For example, non-terminating expressions such as

fun loop() = loop()

inhabit every type, as do exception-raising expressions, such as

fun fail() = raise (Fail "inconsistent!?")

(Note: the expressions here are loop() and fail(). Here and below, I assign names to expressions by declaring them as thunks.) But none of these are values. Indeed, evaluation of the first expression will never yield a result,

- loop();
(* waiting a long time... *)

whereas the second will return immediately, but with an exception rather than a value:

- fail();
uncaught exception Fail [Fail: inconsistent!?]
raised at: stdIn:2.3-3.5

(There are some additional complaints about the value restriction when evaluating these polymorphic expressions, but for our purposes we can ignore them here.) In fact, the logic of ML values is consistent, as we can see by defining the empty type:

data void = Void of void

There are no values of type void, since the only way to construct one is by already having one. Note, though, that all bets are off "under a lambda"—we can still build a value inhabiting any function type σ→τ, for example

fun fnfail() = fn _ => raise (Fail "inconsistent!?")

Let's try to be a bit more precise about what happens before we reach that point.

Another folk theorem about "the logic of ML" is that insofar as it is consistent (i.e., if you avoid things like unrestricted recursion and exceptions), with the addition of control operators it becomes classical. We can import the relevant SML/NJ library and see what they mean:

- open SMLofNJ.Cont;
opening SMLofNJ.Cont
type 'a cont = 'a ?.cont
val callcc : ('a cont -> 'a) -> 'a
val throw : 'a cont -> 'a -> 'b
val isolate : ('a -> unit) -> 'a cont
(* ... *)

As first observed by Griffin, the type of callcc corresponds logically to the classical principle of Peirce's Law. We can make this a bit easier to see by defining another control operator letcc, which essentially does the same thing as callcc but with first-class ML functions, rather than values of the cont type:

- fun letcc f = callcc (fn k => f (fn x => throw k x));
val letcc = fn : (('a -> 'b) -> 'a) -> 'a

Using letcc, we can derive the law of excluded middle, ∀α.α ∨ ¬α. To represent this type, we first introduce a type constructor for disjunctions:

data ('a,'b) either = Left of 'a | Right of 'b

Now we can witness excluded middle as follows:

fun excluded_middle() : ('a,'a -> void) either =
letcc (fn k => Right (fn x => k (Left x)))

So what happens when we attempt to evaluate this expression? (To avoid complaints about the value restriction, we instantiate the type variable 'a at some arbitrary type a.)

- excluded_middle() : (a,a -> void) either;
val it = Right fn : (a,a -> void) either

And now, in contrast to what happened above with the evaluation of loop() and fail(), here we actually get a value!

So can we say that the logic of ML values really is classical? Well, we evidently can under the "bag of tautologies" view of logic. But that is not necessarily the most useful view.

If we look up at the above ML session, a shockingly anti-classical principle is already staring back down at us. After evaluating excluded_middle(), we got back this value:

val it = Right fn : (a,a -> void) either

That is, not only is this a proof of α ∨ ¬α, but in fact it contains a proof of the right side of the disjunct, ¬α. This is an instance of the intuitionistic disjunction principle, that a proof of a disjunction is a proof of one of the two disjuncts.

The punchline, I would say, is that the logic of ML values is not unsound, and not classical, but simply constructive. What is an ML value of type τ? Just an intuitionistic proof of τ—but in a non-empty context. This context includes the current continuation of type ¬τ, as well as all of the other effects that can be invoked underneath a lambda, i.e., in values of functional type.

Okay, so what have we brushed over here? Well first, the restriction that effects are only invoked underneath lambdas can actually be enforced by CPS translation. Functions σ→τ are interpreted as ¬(σ∧¬τ), where ¬(-) denotes minimal negation, i.e., ¬τ = τ→β, for some fixed parameter β, the return type. Effectful operations are encoded as things that return β. Second, I said that a value of (a CPS translated) type τ is an intuitionistic proof of τ (in a non-empty context of effects), but are all such intuitionstic proofs values? Well, no, because some proofs involve "detours". To be concrete, if M₁ and M₂ are proofs of σ and τ, then π₁(M₁, M₂) is a proof of σ—yet, #1 ("hello", "world") is typically not considered to be a value (it evaluates to "hello"). (Some people like to call expressions like #1 ("hello", "world") "valuable".) Third, to say that there is a "logic" of ML values, we really do have to explain what its composition principles are, and not just which principles fail. I might revisit some of these points in another post.

Finally, the whole idea of a "logic of ML values" is very close to the idea of the realizability interpretation of ML. Some people believe that realizability is a distinct and very different alternative to Curry-Howard as a constructive interpretation of logic. My point with this post was mainly to suggest that Curry-Howard need not exclude realizability-like interpretations, once we realize (so to speak) that there is more than one syntactic category of proofs.

Big-Step Normalisation

I realized that the idea of the previous post of factoring normalization as a translation to and from a syntactic model of normal forms is explored very nicely in a JFP article by Altenkirch and Chapman, indeed with a concrete environment semantics, albeit without a connection to focusing:

"Big-Step Normalisation"
Thorsten Altenkirch and James Chapman
pdf
Abstract:
Traditionally, decidability of conversion for typed λ-calculi is established by showing that small-step reduction is confluent and strongly normalising. Here we investigate an alternative approach employing a recursively defined normalisation function which we show to be terminating and which reflects and preserves conversion. We apply our approach to the simply-typed λ-calculus with explicit substitutions and βη-equality, a system which is not strongly normalising. We also show how the construction can be extended to System T with the usual β-rules for the recursion combinator. Our approach is practical, since it does verify an actual implementation of normalisation which, unlike normalisation by evaluation, is first order. An important feature of our approach is that we are using logical relations to establish equational soundness (identity of normal forms reflects the equational theory), instead of the usual syntactic reasoning using the Church-Rosser property of a term rewriting system.

Normalization-By-Evaluation, Normalization-By-Focusing

So I've moved to Paris. I finally arrived here last week (after a bit of a summer vacation), to begin a post-doc at Université Paris 7. In addition to my host Paul-André Melliès, there is a ridiculous number of people based here doing exciting work in programming and proof theory, and also quite a few visitors. So I'm excited.

One of my goals with this post-doc is to better connect the general approach to logic and programming that I was trained in at CMU, which could be called a "syntactic" approach, to the more semantic approach prevalent in Europe. "Syntactic" is in scare quotes because it is sometimes used as a derogatory term, slightly gentler than the epithet "symbol-pushing", and I don't think it is really appropriate. Of course I wouldn't think so! But there's a burden of proof in explaining how this thing that looks like symbol-pushing to the outside world is actually just another way (and a useful way) of manipulating semantic content.

So this post is in that vein, and was prompted by hearing Danko Ilik (one of Hugo Herbelin's students) give a talk two days ago about Normalization-By-Evaluation (NBE), and its apparently well-known (but I guess not well-known enough, since I hadn't seen it before) connection to Kripke semantics for intuitionistic logic. The connection is extremely easy to state:

NBE = completeness ○ soundness

That is, constructively speaking, NBE for the lambda calculus (a.k.a. a proof system for intuitionistic logic) corresponds to applying the soundness theorem (if something is provable it is true in every Kripke model) followed by the completeness theorem (if something is true in every Kripke model then it is provable). More precisely, the soundness theorem is applied to bring a lambda term into the universal model of contexts ordered by inclusion, and then the completeness theorem takes it back into the lambda calculus, now in normal form. Darin Morrison recently posted some elegant code to the Agda mailing list, demonstrating this explicitly.

Okay, that's neat, now let's talk about something else: focusing. If you are reading this blog you have probably heard something about it. (If not, you can learn about it here or here or here or here or here or here.) Originally, focusing was conceived as a search strategy for linear logic sequent calculus, achieving efficiency by severely restricting when you could apply the different rules, based on the polarity of connectives (positive ⊗, ⊕, !, ∃, versus negative ⅋, &, ?, ∀). The surprising and important result was that this strategy is complete, i.e.:

THEOREM (Completeness of focusing) [Andreoli]: If the sequent Γ ⊢ Δ is provable in linear logic, then it has a focusing proof.

The converse, soundness, is of course also important, but was obvious in Andreoli's original formulation, where focusing was seen as a search strategy, and a focusing proof was just a special sort of sequent proof.

Nonetheless, we have soundness and completeness theorems. Great! Can we compose them?

Well, let's not go there quite yet...

First, let's move away from linear logic, which may seem exotic, to something more mundane: classical propositional logic. Is there a notion of focusing proofs in classical logic? In fact, there are too many. Whereas the polarities of the connectives of linear logic are all somehow fixed by their inference rules, in classical logic there are many different, equally valid possibilities for inference rules, and as a result the propositional connectives are fundamentally bipolar. The flip side is that the classical connectives can be explicitly polarized, e.g.., we can choose whether to treat conjunction ∧ positively as ⊗, or negatively as &, and similarly with disjunction, negation, and implication. And this act of disambiguation endows the classical connectives with constructive content.

How so?

Well, let's take another look at the soundness and completeness theorems for focusing. Since focusing proofs deal with explicitly polarized propositions, and ordinary (classical) proofs don't, we will relate the two notions via an operation |-| that "forgets" polarity, i.e., collapses ⊗ and & both to plain conjunction, ⅋ and & both to plain disjunction, etc. Then we can state the following:

THEOREM (Classical soundness of focusing): If the sequent Γ ⊢ Δ has a focusing proof, then |Γ| ⊢ |Δ| has an ordinary classical proof.

THEOREM (Classical completeness of focusing): If the sequent |Γ| ⊢ |Δ| has an ordinary classical proof, then Γ ⊢ Δ has focusing proof.

So now can we compose?

Again speaking more constructively, suppose we take as our starting point some version of classical natural deduction, e.g., natural deduction adjoined with reductio ad absurdum, or with Peirce's law, a.k.a. lambda calculus with control operators. And suppose we have a proof (program) establishing (inhabiting) some proposition (type). Now, to apply the completeness theorem to obtain a focusing proof/program, crucially, we must choose some polarization of the connectives. What we obtain by applying the completeness theorem can and will depend on the particular polarization. But then, once we have a focusing derivation, we can again obtain a classical derivation in a deterministic way, by applying the soundness theorem.

And what do we get as a result? Well, we can make two observations:

1. The result is in normal form. I.e., it corresponds to a β-reduced, η-expanded lambda term (or a sequent calculus proof without cuts and with only atomic initial axioms).
2. The result is in continuation-passing style (CPS).

And in fact, the choice we made when applying the completeness theorem—the way we polarized the connectives—is precisely the way we choose among the many different CPS translations, call-by-value vs call-by-name, etc.

[Aside: it is well-known that different CPS transformations correspond to different double-negation translations, proof-theoretically. This may seem at odds with the above statement, since the result of applying completeness followed by soundness is still a proof of the original sequent, not a double-negated sequent. But we can make the connection to double-negation translation more transparent by factoring the soundness theorem by way of minimal logic, i.e, the fragment of intuitionistic logic where negation is defined by ¬A = A ⊃ #, for some distinguished atom #. The soundness theorem is then stated as follows:

THEOREM (Minimal soundness of focusing): If the sequent Γ ⊢ Δ has a focusing proof, then Γ^t, Δ^f ⊢ # has an ordinary minimal proof.

Here, -^t is the operation that interprets positive connectives "directly" (i.e., conjunction as conjunction, disjunction as disjunction, etc.) and interprets negative connectives as the negation of their De Morgan duals, while -^f interprets negative connectives as their duals, and positive connectives as their negations. Now, the result of applying the classical completeness theorem followed by minimal soundness, followed by the inclusion of minimal logic into classical logic, is not necessarily the original sequent, but a (classically) equivalent one. For more details, see Chapters 3 and 4 of my thesis.]

In short, by composing the soundness and completeness theorems for focusing, we obtain a normalization procedure for a proof system/programming language, that moreover fixes an evaluation order based on the polarization. We could call this "Normalization-By-Focusing":

NBF = soundness ○ completeness

So how does this compare to the original equation, NBE = completeness ○ soundness? First, observe that the fact that the positions of soundness and completeness are swapped is purely a historical convention! Since focusing was originally conceived as a search strategy for sequent calculus, it made sense to ask that it be complete. But in any case, it is clear that the focusing completeness theorem is playing a role analogous to the Kripke soundness theorem, and the focusing soundness theorem a role analogous to the Kripke completeness theorem. In other words, in both cases we are going out of a formal system with some arbitrary collection of rules, into a very well-behaved system, and then back into a canonical fragment of the original system.

In other words, I think it is entirely accurate to say that focusing provides a semantics of proofs. And a proof-theoretic semantics at that.

But how does it really relate to other semantic approaches? Again, that's what I'm here to find out. I suspect, though, that there's more than a superficial resemblance between the NBE and NBF equations, and there might be a deeper connection between focusing and the technique of forcing in proof theory.

More on LOGICOMIX, from Richard Zach

Richard Zach of LogBlog also wrote a review of Logicomix last week, and today followed up specifically addressing the novel's theme of Logic and Madness. This was something I left out of my review, but like Zach, I was similarly turned off by the novel's insinuations of a positive correlation. Both posts by Zach point out several historical inaccuracies in Logicomix, where the novel overstates the "madness" of various logicians—important to keep in mind when reading Logicomix (which you should, nonetheless...).

Review of LOGICOMIX

I was in New York City yesterday visiting the French consulate, on a mission to obtain a scientific visa (my second attempt). The bus from Rochester got into Chinatown around 7:45am, so I made it to the consulate by 9am, got in line, handed in my documents, had a few pictures/fingerprints taken, and was told to come back at 3pm to pick up a visa. With a few hours to kill in the city, I set out on another mission: to find a copy of Logicomix!

LOGICOMIX: an Epic Search for Truth
Apostolos Doxiadis and Christos H. Papadimitriou
art by Alecos Papadatos and Annie di Donna
http://www.logicomix.com/

First, a note on availability. This book was just released to the public in English, I believe a little over a week ago. The UK edition is currently sold out, and the US edition is only available for pre-order on Amazon. So the odds of my finding a copy were perhaps not so good. On the other hand, New York City has the Strand Bookstore. With a bit of luck and perserverance, I managed to track down their only copy, which they received two [sic!] days ago (they are ordering more). I finished reading it on the train ride back to Rochester.

Second, a disclaimer: I had ridiculously high expectations for this book. It has been at the top of my wishlist for years. Anticipation for Logicomix has been floating around the net since the first half of the decade, based on its basic premise: a comic book about logic and logicians. For example, you can find Philip Wadler drooling about the idea back in the summer of 2005. I don't remember when I first found out about Logicomix, but it was a while before that (looking back at old email archives, it seems to have been May 2004), sometime after I heard about Papadimitriou's first work of fiction, Turing: a novel about computation (which is a very fun book, by the way, basically a sci-fi thriller with some computer science lessons thrown in, and some pretty hot sex scenes).

Given all this anticipation built on the idea of Logicomix, reading the actual Logicomix was bound to be somewhat of a let-down. In a word, I was hoping for something impossibly EPIC. Let me say, though, that I still think Logicomix is a revolutionary book, with a brilliant premise that is very well executed but for a few flaws. The premise is basically this: to convey the drama of the late 19th-/early 20th-century upheavals in mathematics and logic, focusing on the people involved, but also giving a sense of their ideas, and of the passion behind the debate. The driving plot force is the life story of Bertrand Russell, and his (at times fictitious) interactions with some of logic's other major and minor figures.

Logicomix is epic in ambition. In some form or another, the book looks at topics including: Euclid's Elements, Cantor's set theory, Boolean algebra, Leibniz's calculus ratiocinator, the 1900 International Congress of Mathematicians and Hilbert's problems, the Epimenides paradox and Russell's paradox, Frege's Begriffsschrift and the Foundations of Arithmetic, Principia Mathematica, simple and ramified type theory, Wittgenstein's Tractatus and the picture theory of language, the Vienna Circle, logical positivism, and the murder of Moritz Schlick, Godel's first incompleteness theorem, algorithms, atheism, World Wars I and II, pacifism, pedagogy, the connection between logic and madness, Aeschylus, street crime in Athens, and free love. And it tries to examine all this as a graphic novel, taking full advantage of the genre's literary/artistic conventions, such as flashbacks and self-reference. The latter fits in well with the subject matter (e.g., Papadamitriou's character asks in the book, "Suppose now you make a complete catalogue of all books that are *not* self-referential"...), but also, more significantly, gives rise to a parallel story relating the intellectual process of writing the book, showing how Logicomix grew through the authors' own debates and discoveries. Finally, a brief appendix at the end tries to fill in some of the historical/mathematical background for the story with a few traditional but well-written articles.

Now, please stop.

Go find a copy of Logicomix (don't worry, they're out there), and read it! You will enjoy it.

I do think the book has flaws, though. I was hoping for Logicomix to do more, but I think in reality it tries to do too much, leaving too much unresolved. There is no doubt something intentional here on the part of the authors, in reference to their subject matter. A chunk of the story revolves around the arduous task of writing the Principia, and how Whitehead after ten years finally convinces Russell to publish their manuscript, even in its unfinished, very imperfect state. Through the self-referential segments of Logicomix, it is strongly implied that the authors had similar discussions of their own. But of course that's not an excuse! I would have liked to have seen some of the historical characters fleshed out more, and could have used less of the "behind the scenes" with the writers. The latter had the feeling of unedited transcripts—again, this was certainly intentional, but I felt it took away from the intensity of the main story. Similarly, I didn't like the overall framing device of having Bertrand Russell relate his life story at a public lecture on "The Role of Logic in Human Affairs": again, because it dilutes the action through another level of indirection, and also because it is a completely implausible lecture. (There are a few other moments where the authors take artistic license with history, which can be a bit grating if you are familiar with the history.) Finally, it seems that the authors didn't know how to end the novel; Logicomix fades away in a highly unsatisfying way.

That said, I am very very happy that Logicomix is finally in print. I am waiting for the sequel.

Defunctionalizing proofs (revised + extended edition)

I wrote a paper that elaborates and improves upon the basic idea I talked sketchily about some months ago, of applying defunctionalization towards a formal representation of "Ω-rules" in Twelf, with applications to pattern-matching and cut-elimination. The paper was accepted to Proof Search in Type Theory, next month in Montreal.

Text: pdf
Code: twelf
Abstract:
In previous work, the author gave a higher-order analysis of focusing proofs (in the sense of Andreoli’s search strategy), with a role for infinitary rules very similar in structure to Buchholz’s Ω-rule. Among other benefits, this “pattern-based” description of focusing simplifies the cut-elimination procedure, allowing cuts to be eliminated in a connective-generic way. However, interpreted literally, it is problematic as a representation technique for proofs, because of the difficulty of inspecting and/or exhaustively searching over these infinite objects. In the spirit of infinitary proof theory, this paper explores a view of pattern-based focusing proofs as façons de parler, describing how to compile them down to first-order derivations through defunctionalization, Reynolds’ program transformation. Our main result is a representation of pattern-based focusing in the Twelf logical framework, whose core type theory is too weak to directly encode infinitary rules—although this weakness directly enables so-called “higher-order abstract syntax” encodings. By applying the systematic defunctionalization transform, not only do we retain the benefits of the higher-order focusing analysis, but we can also take advantage of HOAS within Twelf, ultimately arriving at a proof representation with surprisingly little bureaucracy.


This is very much work in progress—comments much appreciated!

The Value of the Free Man

I found this political lecture by Albert Einstein (delivered before "The Friends of Europe" in London) in an old magazine (World Digest, April 1934), while sorting through piles and piles of books. As far as I can tell it does not exist online, so I transcribed it and am placing it here (and here):

---

The Value of the Free Man

Modern life is worth while because the individual guaranteed the possibility of free development, free communication, free religion, and, as far as the well-being of human society permits, free initiative of action.

Nobody can deny that to-day this foundation of a worthy existence is in considerable danger. Forces are at work which are attempting to destroy the European inheritance of freedom, tolerance, and human dignity. The danger is characterised as Hitlerism, Militarism, and Communism which, while indicating different conditions, all lead to the subjugation and enslavement of the individual by the State, and bring tolerance and personal liberty to an end.

When I speak of Europe, I do not mean the geographical conception of Europe, but a certain attitude of life and to society which has grown up in Europe and is characteristic of our civilisation.

I mean the spirit which was born in ancient Greece and, more than a thousand years later, at the time of the Renaissance, spread from Italy: the spirit of personal liberty and regard for the individual.

If to-day our knowledge of natural laws and the technical possibilities for the advancement of our lives have reached such perfection as never before in the known history of mankind, we owe this to the fact that only the individual can really create what is new and worthwhile.

Without such freedom there would have been no Shakespeare, no Goethe, no Newton, no Faraday, no Pasteur, and no Lister.

There would be no comfortable houses for the mass of the people, no railway, no wireless, no protection against epidemics, no cheap books, no culture and no enjoyment of art for all.

There would be no machines to relieve the people from the arduous labour needed for the production of the necessities of life.

It cannot be my task to act as judge of the conduct of a nation from the point of view of statesmen or as one who is immersed in the responsibilities and the details of the daily life of politics.

Yet everyone who loves the subtler manifestations and the beauty of the human spirit, and who believes himself able to diagnose the deeper causes of the present situation, has the duty of raising his voice in warning.

For if we do not make energetic resistance, we shall sink back into a way of life which is indistinguishable from that of the subjects of the old Asiatic despotisms.

It will be worse than theirs, for the modern despots, while not disposing of more brains than their former colleagues, own the arm---and it is a long and strong arm---of a mighty technical apparatus for the exercise of physical power, and in their schools, radio, and press they possess an instrument of mental and moral influence which ordinary mortals cannot resist.

It is of the essence of despotism not only that one individual with practically unlimited authority is at the head, but that society itself becomes the tool of the enslavement of the individual.

I would therefore much rather call the enemy of the European spirit "Servitude to the State."

This servitude exists when the State is not an instrument in the hands of the citizens, as it ought to be, but when the citizens are in practice unconditionally delivered over to the power of the State. This condition is expressed in the German language by speaking of the population as "human material" (Menschenmaterial).

What is it that converts the free European into a slave of the State? My simple answer is: the necessity of military organisation on the part of each separate State. In other words, the cause is international juridical anarchy. I believe that the German has become the complete victim of the State because his country, by its geographical condition, is most exposed to attack, and was therefore most dependent on rigid military organisation.

But military organisation means degradation of the individual to an obedient tool, void of will. It demands the training of youth into an automatic and uncritical obedience towards a superior.

In short, it implies the renunciation of personality and human worth.

The petty persons who to-day govern Germany owe their power mainly to the education of former generations in a spirit of submissiveness and servility, a state of mind which is diametrically opposed to the consciousness of personal responsibility of the true European man.

If it be true that individuality as the basis of the European ideal is gravely menaced by the necessity for military organisation of the several separate States, there can be no doubt as to how the danger may, and must be, overcome.

The separate State must be offered an effective guarantee for its security in relation to neighbouring States.

Disarmament according to a fixed plan without guarantee of security by the entire community of States is impossible, if for no other reason than that to-day war is not a society-game where one can be sure that everything will go according to rule.

On this main issue of how to win through to civilisation, therefore, I share entirely the French point of view.

I am also convinced that a universal collective guarantee for the security of individual States is in itself by no means enough.

The military organisations of the separate States ought to be internationalised, that is, transformed into an international police force subject to a super-national authority.

If the reader thinks this Utopian, he may, for comparison, imagine a State in which there are no police and no courts. In their place a law exists which makes it compulsory for every citizen to help his fellow-citizen with whom a third citizen dares to interfere. Do you believe that the citizens of such a State would desist from carrying their own weapons about with them? I doubt it.

The serious efforts of the Governments which have led to the Disarmament Conference show that there exists a general awareness of the danger in which we live. In the light of the foregoing, lack of success is not difficult to understand. There are problems which cannot be brought to solution by small steps and stages.

Either the security of States is guaranteed internationally, in which case the separate State needs no military organisation at all, or this guarantee is not achieved, in which case the State must arm as effectively and completely as possible.

Nationalism in my opinion is, in this respect, no more than an idealistic basis for the militarist and aggressive mental condition of a people.

Hitlerism is a form of State thoroughly adapted to military purposes. This is so true that a "leader" can only hold himself in power by behaving aggressively, at least in appearance, in foreign relations, for he must always hold before the eyes of his people the real or imaginary purpose for which they are asked to sacrifice their freedom.

Only through perils and upheavals can nations be brought to further developments. It is in times of economic distress such as are experienced everywhere to-day, that one sees very clearly the strength of the moral forces which reside in a people.

Let us hope that a historian, delivering judgment in some future period when Europe is politically and economically united, will be able to say that in our days the liberty and honour of this Continent were saved by its Western nations.

Let him be able to say they stood fast together against the temptations of hatred and oppression, and that the Western world defended successfully the liberty of the individual, without which life to a self-respecting man is not worth living.

The leading statesmen are burdened with tremendous responsibilities to-day as they were twenty years ago.

May they succeed through timely agreement in establishing a condition of unity and clarity of international obligations in Europe, so that to every State a war-like adventure must appear foredoomed as utterly hopeless.

But we are concerned not merely with the technical problem of securing and maintaining peace, but also with the important task of education and enlightenment. If we want to resist the powers which threaten to suppress intellectual and individual freedom, we must keep clearly before us what is at stake, and what we owe to that freedom which our ancestors won for us after hard struggles.

Thus, the work of statesmen can succeed only if it is supported by the serious and determined will of the peoples. And the essence of that will is the creative adventure of free citizens.

I know very many people who are willing to approve in principle opinions such as have been expressed here, but who will fall back the next moment into the ruts of ordinary political action.

But he who is seriously convinced that the future growth of our civilisation is bound up with the preservation and development of the human personality, must be prepared to make sacrifices for his convictions.

The sacrifice I am thinking of is the partial abandonment of State sovereignty by the separate States, and the yielding of the principle of egoism in favour of international security.

Here lies the hope of Europe and the Western world.

The Proofs of Life After Death: a 20th Century Symposium

Browsing in the local history section of the Central Library in Rochester, NY, I stumbled on this curious book from 1902:

Wonderfully, the full text is available online through google books. The book is a collection of responses by various thoughtful people to the following request:

Dear Sir:

The Author of this letter, inspired by the untimely decease of a dear friend, and in contemplation of the numerous philosophical and logical theories leading to a belief in the continued existence of the soul, or personal identity after death, begs of you the great favor of a letter, setting out as briefly, or at such length as may be convenient, what you consider to be the strongest reason, or argument, advanced by science or philosophy, or by common sense, in favor of an affirmative answer to this mighty question; or preferably, a statement of your own deductions thereon.

It is our desire to obtain from thinkers and educators of the world, an expression—a twentieth century bulletin, on this subject.

Our request will impress you doubtless as an unusual one, but none the less will you see the force of it, and its possibilities. Who can measure the impetus such a compilation may have upon the inquiring human mind?

May I not have your co-operation in this matter?

Thanking you now in advance for the courtesy of a reply, I am

Fraternally yours,
ROBERT J. THOMPSON.

Wellington Ave., Chicago, U. S. A.
October, 1901.

I had fun skimming through the first collection of responses, from "The Scientists". The variety of responses is interesting. Although there's the usual bloviation on the cosmological and teleological arguments, as well as some self-citations to studies confirming the existence of telepathy and other paranormal phenomena, there's also some healthy scientific modesty. E.g., E. Ducleaux writes,

Excuse me for not being able to help you in your investigation. I have no scientific opinion regarding the questions you put. I mean, no opinion that rests on anything but personal beliefs. Besides, I think that everybody is in about the same position and that any reasons that may be brought forth in favor of one's opinion are only good for the person that brings them forth, and that they cannot impress the listener; they are therefore not scientific reasons.

D. I. Mendélieff's response begins similarly, although he ends by arguing for the immortality of the soul by analogy with the laws of conservation of mass and energy (an analogy I was surprised to see repeated very often in the other responses!):

The question as to the continuance of the existence of the soul or personal identity after death, mentioned in your letter of August, 1901, I, as a natural philosopher, consider to be an hypothesis which cannot be proved by evidence of real facts. But as a man educated in a religious sense, I prefer to remain in the belief of the immortality of the soul. It is my opinion that the philosophical side of the question consists in the relation between the soul, the natural forces, and matter; and if it were possible to clear up to some extent this feature of the problem---the relation between force and matter---then also the relation between the soul and natural forces would be forwarded to a great extent.

The unquestionable existence of reason, will and consciousness compels us to acknowledge the existence of a special world of relations of this kind, and any rational conclusion in relation to this special world cannot be accepted as proved quite in the same manner. Knowledge of physics and mechanics does not give anything in relation to chemistry or in relation to the existence of celestial bodies.

We must simply confess that it is impossible to comprehend this question in a general way, but it would also be sheer nonsense to ignore the physical world; and as matter and natural forces must be acknowledged as eternal, it is also probable that the soul is eternal.

But my favorite response was by James R. Nichols, marveling at the modern-day wonders of Web 2.0 the telephone:

Do we not every day converse with unseen friends long distances away; do we not recognize their familiar voices, in homes separated from us by rivers, woods, and mountains? These voices come out of the darkness, guided by a frail wire which science provides as a pathway.
[...]
If our friends in this life, dead to us (hidden as they are by the shroud of space), can be seen, and we can hear their voices, their shouts of laughter, the words of the hymns they sing, the cries of the little ones in the mother's arms, is it very absurd to anticipate a time when those dead to us by the dissolution of the body may, by some unknown telephony, send to us voices from a realm close at hand, but hidden from mortal vision?

The Logical Basis of Evaluation Order and Pattern-Matching

The Logical Basis of Evaluation Order and Pattern-Matching

An old and celebrated analogy says that writing programs is like proving theorems. This analogy has been productive in both directions, but in particular has demonstrated remarkable utility in driving progress in programming languages, for example leading towards a better understanding of concepts such as abstract data types and polymorphism. One of the best known instances of the analogy actually rises to the level of an isomorphism: between Gentzen's natural deduction and Church's lambda calculus. However, as has been recognized for a while, lambda calculus fails to capture some of the important features of modern programming languages. Notably, it does not have an inherent notion of evaluation order, needed to make sense of programs with side effects. Instead, the historical descendents of lambda calculus (languages like Lisp, ML, Haskell, etc.) impose evaluation order in an ad hoc way.

This thesis aims to give a fresh take on the proofs-as-programs analogy---one which better accounts for features of modern programming languages---by starting from a different logical foundation. Inspired by Andreoli's focusing proofs for linear logic, we explain how to axiomatize certain canonical forms of logical reasoning through a notion of pattern. Propositions come with an intrinsic polarity, based on whether they are defined by patterns of proof, or by patterns of refutation. Applying the analogy, we then obtain a programming language with built-in support for pattern-matching, in which evaluation order is explicitly reflected at the level of types---and hence can be controlled locally, rather than being an ad hoc, global policy decision. As we show, different forms of continuation-passing style (one of the historical tools for analyzing evaluation order) can be described in terms of different polarizations. This language provides an elegant, uniform account of both untyped and intrinsically-typed computation (incorporating ideas from infinitary proof theory), and additionally, can be provided an extrinsic type system to express and statically enforce more refined properties of programs. We conclude by using this framework to explore the theory of typing and subtyping for intersection and union types in the presence of effects, giving a simplified explanation of some of the unusual artifacts of existing systems.

Successfully defended April 17, 2009!

On the meaning of logical completeness

I would really like to have time to read this paper by Michele Basaldella and Kazushige Terui, as well as many of Terui's other highly interesting recent papers.

Defunctionalizing Proofs (and how to define a pattern-matching, CPS language in Twelf)

I drove back from Savannah and POPL/PLPV/TLDI yesterday. It was a long and exciting drive (in part because of the snow and frozen windshield washer fluid driving through West Virginia, god I hate that stretch of highway), and a long and exciting week at the conference. My favorite talk was an invited one by Chris Barker on Wild Control Operators, in the sense of "continuations in the wild". Chris is a linguist who for several years (I think since around 2000) has been advocating the use of continuations to analyze apparently non-compositional phenomena in natural language. He collaborates with brilliant computer scientist Ken Shan, who wrote his PhD thesis on "Linguistic Side Effects".

In this post I want to introduce some Twelf code I wrote after getting back to Pittsburgh. At the PLPV workshop I presented my paper on Refinement Types and Computational Duality. I didn't exactly time the talk well, and ended up going through about half my slides in ten minutes past the allotted time. (Luckily, I didn't run into Obama's talk, which was better prepared.) The paper itself is similar in that respect, trying to rush through too much material in too short a space. One of the ideas it describes probably too briefly is that of defunctionalizing proofs. Defunctionalization is a trick due to John Reynolds, from his paper on Definitional Interpreters for Higher-Order Programming Languages. It allows you to take a program with higher-order functions and convert it into one with only first-order functions. Essentially, it boils down to giving a unique tag to every function definition in your program, and then defining a separate "apply" function that tells you how to apply the function denoted by a tag to an argument. (A complication is that function bodies may reference escaping variables, so defunctionalization has to be preceded by closure conversion.)

Why would proofs contain functions in the first place? For the same reason programs do: sometimes they are a useful abstraction. An old example from proof theory comes in the work of Paul Lorenzen and Kurt Schütte, who in the 1950s began revisiting Gerhard Gentzen's work via infinitary methods (see "Lieber Herr Bernays!, Lieber Herr Gödel!" by Feferman for an interesting history). Schütte simplified Gentzen's proof of cut-elimination for Peano arithmetic by replacing the usual schema of induction by the so-called ω-rule, which says, "To prove ∀x:ℕ.A(x), prove A(0), A(1), A(2), ...". At first glance, the ω-rule seems silly: how can we ever apply a rule with infinitely many premises? But a different way of looking at the ω-rule is that it demands a single function, mapping natural numbers n to proofs of A(n). And this function can certainly have a finite representation, for example as a C program.

In some other papers, I described how to view Andreoli's "focusing" proofs as higher-order in this sense, containing functions that map proof patterns (or refutation patterns) to other sorts of proof objects. For example, to refute a proposition of positive polarity, we build a function from proof patterns to proofs of contradiction. This has a simple Curry-Howard interpretation: we can define call-by-value continuations by functions from value patterns to expressions. In other words, we actually represent the syntax of a programming language using computation.

Dependently-typed functional languages such as Agda and Coq turn out to be very convenient platforms for embedding such higher-order language definitions. In the dependently-typed setting of Twelf, frustratingly, it seems impossible! This is surprising, at least in a superficial way, because Twelf is well-known for allowing language definition via "higher-order abstract syntax" (HOAS). But HOAS is a different idea from the above technique (which I've taken to calling AHOS). Essentially, the problem is that the function space of LF (the type-theoretic core of Twelf) is very weak: abstractly, a function A→B is just a B with a hole for an A, or in other words, A→B represents a substitution function, something into which you can plug in an A to obtain a B. This weakness is in fact crucial for doing HOAS. But it means we absolutely cannot use the LF function space to do AHOS. (Think, for example, what that would mean for the ω-rule: to prove ∀x:ℕ.A(x), we would have to give a proof of A(n) that works the same way for every n. But the predicate A might hold for different n for different reasons, so such a rule would be woefully incomplete.) On the other hand, that we can't define languages using AHOS in Twelf is frustrating, because HOAS is rather nice for other parts of a language definition.

Fortunately, it turns out we can have our AHOS and eat HOAS too! And it all boils down to Reynolds' trick. You can check out the code here.