Wet Sidewalks and Odd Numbers

Phil Crissman explains Propositions as Types with a dialogue between Achilles and the Tortoise, in the style of Douglas Hofstadter (who in turn was inspired by Lewis Carrol). Lambda Man makes an appearance.

Gödel, Animated

 

A five-minute primer on Gödel and incompleteness, courtesy of Marcus du Sautoy and TED-Ed. While not named, the fellow in the hat disgruntled by the discovery is clearly Hilbert.

Reading list

 

Kevin Doran wrote to me requesting a reading list on logic. He recommends an introductory guide to logic by Peter Smith. Smith's appendix lists several textbooks on logic, but misses my two favourites.

• Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. CUP, 1989. The master logician (discoverer of System F and linear logic), aided by two superb computer scientists, covers the basics. Explains additive and multiplicative proof rules, and the fundamentals of propositions as types.
  
• Jean van Heijenoort, From Frege to Gödel A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, 1967. My favourite entry is the correspondence between Russell and Frege---it is only a few pages long and so a quick read; don't skip van Heijenoort's introduction. See also Anita Feferman's biography of van Heijenoort, who lived quite a life: he served as Trotsky's secretary and was shot to death by a jealous lover.
  
  

Five stages of accepting constructive mathematics

 

From a psychological point of view, learning constructive mathematics is agonizing, for it requires one to first unlearn certain deeply ingrained intuitions and habits acquired during classical mathematical training. In her book On Death and Dying psychologist Elisabeth Kubler-Ross identified five stages through which people reach acceptance of life’s traumatizing events: denial, anger, bargaining, depression, and acceptance. We shall follow her path.

Five stages of accepting constructive mathematics is a nifty introduction to constructive mathematics by Andrej Bauer. Mentioned by Martin Escardo on the Agda mailing list. 

Every Proof Assistant

Andrej Bauer writes:

For a while now I have been contemplating a series of seminars titled "Every proof assistant" that would be devoted to all the different proof assistants out there. Apart from the established ones (Isabelle/HOL, Coq, Agda, Lean), there are other interesting experimental proof assistants, and some that are still under development, or just proofs of concept. I would like to know more about them, and I suspect I am not the only one. 

Getting the authors of proof assistants to travel to Ljubljana and giving talks at our Foundations of mathematics and theoretical computer science seminar has largely become impossible. But luckily research seminars world-wide are rapidly moving online, and so is our Foundations seminar. I am therefore delighted to announce the first "Every proof assistant" seminar. ... 

I have a couple more in the pipeline, so follow this blog, the Foundations seminar announcements or my Twitter account @andrejbauer.

A Profound Pun

My attempt to explain Propositions as Types to a general audience. Recorded at Bright Club, The Stand, Edinburgh, 23 September 2019.

Toki Pona

At Haskell Exchange, Stephan Schneider introduced me to Toki Pona, an extremely simple artificial language, based on 120 symbols. You can read more on Wikipedia.

Programming Language Foundations in Agda

Wen Kokke and I are pleased to announce the availability of the textbook:

  Programming Language Foundations in Agda
  plfa.inf.ed.ac.uk
  github.com/plfa/plfa.github.io/

It is written as a literate script in Agda, and available at the above URLs. The books has so far been used for teaching at the Universities of Edinburgh and Vermont, and at Google Seattle. Please send your comments and pull requests!

The book was presented in a paper (of the same title) at the XXI Brazilian Symposium on Formal Methods, 28--30 Nov 2018, and is available here:

  http://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf

The paper won the SBMF 2018 Best Paper Award, 1st Place.

RADICAL 2017

Please submit to RADICAL 2017, Recent Advances in Concurrency and Logic, a workshop co-located with QONFEST (CONCUR, QEST, FORMATS, and EPEW), Berlin (Germany), September 4, 2017.

As you know, submissions to RADICAL could be, for instance:- reports of an ongoing work and/or preliminary results;- summaries of an already published paper (even at CONCUR'17 - see below);- overviews of (recent) PhD theses;- descriptions of research projects and consortia;- manifestos, calls to action, personal views on current and future challenges;- overviews of interesting yet underrepresented problems.
...
Many thanks for your cooperation!Julian and Jorge

A busy summer

I'll be speaking at the following events.

• Joy of Coding, 17 June 2016, De Doelen, Rotterdam; keynote speaker.
• ACSD, 22—24 June 2016, Torun; keynote speaker.
• BETTY Summer School, 27 June—1 July 2016, Limassol, Cyprus; lecturer.
• International Summer School on Metaprogramming, 8—12 August 2016, Cambridge; lecturer.
• Lambda World, 1 October 2016, Cadiz; keynote speaker.

Hope to see you at one of these!

Strange Loop: "Propositions as Types" by Philip Wadler

And for the last of my selection from Strange Loop 2015, here is "Propositions as Types" by Philip Wadler, based on my paper of the same name, which I am told will soon appear in Communications of the ACM. I received more compliments on this talk than for any other, which I take as one benefit of the friendliness and fun of the Strange Loop crowd. Thanks to Alex Miller and the crew for assembling a great conference!

Philosophers

This may come in handy next time I need to lecture on Russell's Paradox. From SMBC.

Propositions as Types, with Howard on Curry-Howard

Propositions as Types has been updated, again. Thanks again to all the readers and reviewers who helped me improve the paper. This version includes an appendix, Howard on Curry-Howard, including additional correspondence with Howard not previously published.

Propositions as Types
Philip Wadler
Draft, 29 November 2014

The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.

Comments still solicited!

Howard on Curry-Howard

When writing Propositions as Types, I realised I was unclear on parts of the history. Below is a letter I wrote to William Howard and his response (with corrections he provided after I asked to publish it). I believe it is a useful historical document, and am grateful to Howard for his permission to publish.

Update. References to Figures 5 and 6 in the following are to Propositions as Types. Thanks to Ezra Cooper for pointing out this was unclear.

Here is my original request.

Subject: The Formulae-as-Types Notion of Construction

Dear Prof Howard,

My research has been greatly influenced by your own, particularly the paper cited in my subject. I am now writing a paper on the field of work that grew out of that paper, which was solicited for publications by the Communications of the ACM (the flagship of the professional organisation for computer scientists). A draft of the paper is attached.

I would like to portray the history of the subject accurately. I have read your interview with Shell-Gallasch, but a few questions remain, which I hope you will be kind enough to answer.

Your paper breaks into two halves. The first describes the correspondence between propositional logic and simple types, the second introduces the correspondence between predicate logic and dependent types. Did you consider the first half to be new material or merely a reprise of what was known? To what extent do you consider your work draws on or was anticipated by the work of Heyting and Kolmogorov, and Kleene's realisability? To what extent did your work influence the subsequent work of de Bruijn and Martin Lof? What was the history of your mimeograph on the subject, and why was it not published until the Curry Festschrift in 1980?

Many thanks for your consideration, not to mention for founding my field! Yours, -- P

And here is his response: 

Dear Prof. Wadler,

As mentioned in the interview with Shell-Gellasch, my work on propositions as types (p-a-t) originated from my correspondence with Kreisel, who was very interested in getting a mathematical notion (i.e., in ordinary mathematics) for Brouwer's idea of a construction (as explained by Heyting). I was not familiar with the work of Brouwer or Heyting, let alone Kolmogorov, but, from what Kreisel had to say, the idea was clear enough: a construction of  alpha - > beta was to be a construction F which, acting on a construction A of alpha, gives a construction B of beta. So we have constructions acting on constructions, rather like functionals acting on functionals. So, as an approximation,

(1)   let's take "construction" to mean "functional".

But what kind of functionals? In constructive mathematics, a functional is not given as a set of ordered pairs. Rather,

(2)   to give a functional is to give not only the action or process it performs but also to give its type (domain and counterdomain).

Clearly, the type structure is going to be complicated. I set myself the project of finding a suitable notation for the type symbols. So one needs a suitable type symbol for the functional F, above. Well, just take it to be alpha itself (at this point, I was thinking of propositional logic). Suddenly I remembered something that Curry had talked about in the logic seminar during my time at Penn State. If we consider typed combinators, and look at the structure of the type symbols of the basic combinators (e.g., S, K, I), we see that each of the type symbols corresponds to (is isomorphic to) one of the axioms of pure implicative logic. Well! This was just what I needed!

How do we formulate the following notion?

(3)   F is a construction of phi.

Consider the case in which phi has the form alpha - > beta. The temptation is to define "F is a construction of alpha - > beta" to mean "for all A: if A is a construction of alpha, then FA is a construction of beta". Well, that is circular, because we have used if ... then ... to define implication. This is what you call "Zeno’s paradox of logic". I avoided this circularity by taking (3) to mean:

(4)   F is assigned the type phi according to the way F is built up; i.e., the way in which F is constructed.

Thus F is a construction of phi {\em by construction}. Your figure 6 illustrates precisely what I meant by this. (I did not have that beautiful notation at the time but it conveys what I meant.)

To summarize: My basic insight consisted simultaneously of the thoughts (2) and (4) plus the thought that Curry's observation provided the means to implement (2), (4). Let me say this in a different way. The thought (2) was not new. I had had the thought (2) for many years, ever since I had begun to study primitive recursive functionals of finite type. What was new was the thought (4) plus the recognition that Curry's idea provided the way to implement (4). I got this basic insight in the summer of 1966. Once I saw how to do it with combinators, I wondered what it would look like from the vewpoint of the lambda calculus, and saw, to my delight, that this corresponded to the intuitionistic version of Gentzen's sequent calculus.

Incidentally, Curry's observation concerning the types of the basic combinators is presented in his book with Feys (Curry-Feys), but I was unaware of this, though I had owned a copy for several years (since 1959, when I was hired at Penn State). After working out the details of p-a-t over a period of several months, I began to think about writing it up, so I thought I had better see if it is in the book. Well, it is easy enough to find if you know what you are looking for. On looking at it, I got a shock: not only had they extended the ideas to Gentzen's sequent calculus, but they had the connection between elimination of cuts from a derivation and normalization of the corresponding lambda term. But, on a closer look, I concluded that they had {\em a} connection but not {\em the} connection. It turns out that I was not quite right about that either. See my remark about their Theorem 5, below. Not that it would have mattered much for anything I might have published: even if they had the connection between Gentzen's sequent calculus and the lambda calculus, I had a far-reaching generalization (i.e., to Heyting arithmetic).

The above is more detailed than would be required to answer your questions, but I needed to write this out to clarify my thoughts about the matter; so I may as well include the above, since I think it will interest you. It answers one of your questions, "To what extent do you consider your work draws on or was anticipated by the work of Heyting and Kolmogorov, and Kleene's realisability?" Namely, my work draws on the work of Heyting and Brouwer, via Kreisel's explanation of that work to me. None of it was anticipated by the work of Heyting, Kolmogorov or Kleene: they were not thinking of functionals of finite type. Though I was familiar with Kleene's recursive realizability, I was not thinking about it at the time. Admittedly, it touches on ideas about Brouwer's constructions but is far from capturing the notion of a construction (actually, Kleene once made remarks to this effect, I forget where). Because of the relation between constructions and Kleene's recursive realizability, there could have been some unconscious influence; but, in any case, not a significant influence.

"did your work influence the subsequent work of de Bruijn and Martin Lof? " As far as I know, my work had no influence on the work of de Bruijn. His work appears to be completely independent of mine. I do recall that he once sent me a package of Automath material. The project of a computer program for checking existing proofs did not appear very interesting and I did not reply. What I would have been interested in is a program for finding proofs of results that had not yet been proved! Even a proof-assistant would have been fine. Why did he send me the Automath material? I don't recall what year it was. Sometime in the 1970s. Whatever the accompanying letter, it was not informative; merely something like: "Dear Professor Howard, you may be interested in the following material ...". Since that time, I have seen two or three articles by him, and I have a more favorable impression. It is good, solid work. Obviously original. He discovered the idea of derivations as terms, and the accompanying idea of formulae-as-types, on his own. He uses lambda terms but, I think, only for purposes of description. In other words, I don't think that he has the connection between normalization and cut-elimination, but I have not made an extensive examination of his work. In fact, does he use a Gentzen system at all? I just don't know. The latter two questions would easily be answered by anyone familiar with his work. In any case, give him credit where credit is due. There are enough goodies for everyone!

My influence on Martin-Löf? No problem there. I met him at the Buffalo 1968 conference and I told him my ideas. His instant reaction was: "Now, why didn't I think of that?" He had a visiting appointment at UIC for the academic year 1968-1969, so we had lot's of opportunity to talk, and he started developing his own approach to the ideas. In Jan. 1969, mainly to make sure that we were both clear on who had discovered what, I wrote up my own ideas in the form of handwritten notes. By then, Xerox machines were prevalent, so I sent a copy to Kreisel, and he gave copies to various people, including Girard. At least, I think that is how Girard got a copy, or maybe Martin-Löf gave him one. I like Martin-Löf's work. I could say more about this, but the short answer to your question is: Martin-Löf's work originated from mine. He has always given me credit and we are good friends.

On further thought, I need to mention that, in that first conversation, Martin-Löf suggested that the derivations-as-terms idea would work particularly well in connection with Prawitz's theory of natural deduction. I thought: okay, but no big deal. Actually, at that time, I was not familiar with Prawitz's results (or, if at all, then only vaguely). But it was a bigger deal than I had thought, because Prawitz's reductions steps for a deduction correspond direcly to reduction steps for the associated lambda term! Actually, for most purposes, I like the sequent formulation of natural deduction as given in pages 33 and 88 of Sorensen and Urzyczyn (2006). In fact, if we add left-implication-introduction to this (let's confine ourselves to pure implicative logic), the resulting system P# is pretty interesting. All occurrences of modus ponens can be eliminated, not just those which are preceded by left-implication-introduction. This is what I am up to in my JSL 1980 paper, "Ordinal analysis of terms of finite type." Also, the cut rule is easy to derive in P# (just consider, for typed lambda terms: a well-formed term substituted into a well-formed term results in a well-formed term); hence P# is is a conservative extension of the system P* in Part I of my little paper in the Curry Festschrift.

The phrase formulae-as-types was coined by Kreisel in order that we would have a name for the subject matter in our correspondence back and forth. I would assume that the phrase "propositions as types" was coined by Martin-Löf; at least, during our first conversation at the Buffalo 1968 meeting, he suggested that one could think of a type as a proposition, according to the idea that, in intuitionistic mathematics, the meaning of a proposition phi is given by the species of "all" proofs of phi. I use quotes here because we are not talking about a set-theoretic, completed infinity.

"the second [part] intrudes the correspondence between predicate logic and dependent types." I was not thinking about it in that way at all. I wanted to provided an interpretation of the notion of construction to some nontrivial part of intuitionistic mathematics (Heyting arithmetic). Part I of the paper was just the preliminaries for this. Actually, what you say in the pdf is consistent with this. No need for change here.

"Did you consider the first half to be new material or merely a reprise of what was known?" New. But in January of last year I had occasion to take a really hard look at the material in Curry-Feys, pp. 313-314; and I now see that there is a much closer relationship between my Theorem 2 in Part I and their Theorem 5, page 326, than I had thought. The issues here are quite interesting. I can provide a discussion if you want.

In the introduction to my little paper, I mention that Tait had influenced me. Let me say a few words about that. In the summer of 1963 we had conversations in which he explained to me that he had developed a theory of infinite terms in analogy to Schütte's theory of infinite proofs, where normalization (via lambda reductions) of an infinite terms corresponds to cut elimination of the corresponding proof. He did not know what to make of it. He thought of his theory of infinite terms as a sort of pun on Schütte's theory of infinite proofs. But we both agreed that  there must be a deep connection between normalization of lambda terms and Gentzen's cut elimination. We puzzled over this during two or three of our conversations but could not come up with an answer.

As explained in the first paragraph of this e-mail, my work originated with a problem posed by Kreisel; so, at the start of this work, certainly I was not thinking of those conversations with Tait. But, as mentioned above, as soon as I got the basic insight about the relevance of Curry's combinators, I considered how it would work for lambda terms. At that point, I remembered my conversations with Tait. In other words, when I verified that

(5)   cut elimination for a derivation corresponds to normalization for the term,

the conversations with Tait were very much on my mind. Most likely I would have noticed (5) without having had the conversations with Tait. But who knows? In any case, he deserves credit for having noticed the correspondence between derivations and terms. What he did not have was the associated correspondence between propositions and types. In fact, he was not using a general enough notion of type for this. By hindsight we can see that in his system there is a homomorphism, not an isomorphism, from propositions to types.

I need to say a bit more about Tait and types. Since Schütte had extended his system of proofs to transfinite orders, Tait extended his system of terms to transfinite type levels. I already had my own system of primitive recursive functionals of transfinite type. In our very first conversation, we compared out ideas on this topic. This topic requires that one think very hard about the notion of type. Certainly, I had already thought extensively about the notion of type (because of (2), above) before I ever met Tait, but my conversations with him reinforced this tendency. Thoughts about types were very much on my mind when I began to consider (1), (2), above.

As already mentioned, the notes were handwritten and xeroxed; no mimeographs. "why [were they] not published until the Curry Festschrift in 1980?" First let me mention why they got published in the Curry Festschrift. Selden was bringing out the Festschrift for Curry's 80th birthday. He asked me to contribute the notes. I said: "Sure. I'll write up an improved version. I can now do much better." He replied: "No, I want the original notes. It is a historical document." In other words, by that time various copies had been passed around and there were a number of references to them in the literature. So I had them typed up and I sent them in.

Why didn't I publish them before that? Simply because they did not solve the original problem. That was Kreisel's and Gödel’s verdict (Kreisel had shown or described the work to Gödel). In fact, even before communicating the work to Kreisel, I knew that I had gotten only an approximation to the notion of construction, and that more work had to be done. Essentially, the criticism is as follows. In my little paper, I do not provide axioms and rules of inference for proving statements of the form

(3)   F is a construction of phi.

Remember, we have to avoid "Zeno’s paradox of logic"! The answer is that the proofs will look like what you have in Figure 6. In other words, Figure 6 is not only a program; it is also a proof (or: it can be reinterpreted as a proof). But Figure 6 can also be interpreted as an explanation of how a construction (blue) is to be built up in order to have a given type (red). In other words, figures such as Figure 6 implements the idea (4) mentioned near the beginning of this e-mail; i.e., F is assigned the type phi according to the way F is built up.

I hope this tickles you; it certainly tickles me. Of course, the rules of inference are as in Figure 5. So these simple ideas provide the missing theory of constructions; or, at the very least, provide a significant step in that direction.

In Jan. 2013, I exchanged a few e-mails with Tait and Constable on the history of p-a-t. This caused me to take a really careful look at the Curry-Feys book. Here is something I found that really made me laugh: the required theory, whose inferences are of the form given in Figure 5 is already in Curry-Feys. Admittedly, to see this you first have to erase all the turnstyles ( |-- ); Curry seems to have some kind of obsession with them. In particular, erase the turnstiles from the proof tree on page 281. The result is exactly a proof tree of the general form given in your Figure 6. (Hint: (...)X is to be read "X has type (...)". In other words, rewrite (...)X as X : (...).) What does Fbc mean, where F is boldface? Just rewrite Fbc as b -> c. You see? I am an expert. I could probably make money writing a translation manual. In summary, the required theory is essentially just Curry's theory of functionality (more precisely, the appropriate variant of Curry's theory). So, did I miss the boat here? Might I have seen all this in 1969 if only I had had the determination to take a hard look at Curry-Feys? I don't know. It may require the clarity of mind represented by the notation of Figure 5. Do you have any idea when and where this notation came into use?

One more remark concerning my reason for not publishing. Didn't I feel that I had made an important breakthrough, in spite of Kreisel's and Gödel’s criticisms? On the one hand, yes. On the other hand, I had reservations. Except for Martin-Löf, Prawitz, Tait and Girard, very few people showed an interest in the ideas. But maybe Martin-Löf, Prawitz, Tait and Girard should have been enough. You say: "Certainly Howard was proud of the connection he drew, citing it as one of the two great achievements of his career [43]." Should we let that passage stand? Sure. The interview occurred in the spring of 2000. By that time, I was getting lots of praise from the computer science community. So, pride is a peculiar thing. Let me end this on a positive note. In 1969 Prawitz was in the US and came to UIC to give a talk. When he entered the room, he made a beeline for me, looked me in the eye and shook my hand. The message was: Well done! THAT made me proud.

There is more to say; but this answers your questions, I think; so I'll send it to avoid further delay. 

Your pdf, Propositions as Types, is very readable.

Bill

Propositions as Types, updated

Propositions as Types has been updated. Thanks to all the readers and reviewers who helped me improve the paper.

Propositions as Types
Philip Wadler
Draft, 26 June 2014

The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.

Comments still solicited!

Propositions as Types

Propositions as Types
Philip Wadler
Draft, March 2014

The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.

Comments solicited!

A formative day for Georg Cantor

From Saturday Morning Breakfast Cereal.

Off the Beaten Track 3: Proofs as Stories

A third talk of note at Off the Beaten Track was Languages for Computational Creativity: Generative Art and Interactive Worlds, by Chris Martens. Her talk included the most inventive application of Propositions of Types that I ever heard: Proofs as Stories. Later, she provided a citation to a longer work, Linear Logic for Non-Linear Storytelling, by some of her collaborators, which uses proofs in linear logic to describe alternative storylines for Madame Bovary. Thanks, Chris!