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.