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.

bipolarism theory

Another interesting conference, on Bi-Polarism Theory and Mathematics is Inconsistent. And while you're in the holiday spirit, check out The Twelf Days of Christmas.