Lambda the Ultimate

...but I guess my dissertation qualifies.

The link between Curry-Howard-like correspondences and the kind of philosophical logic that Michael Dummett does have been known for a long time, but have not been commented about much, and for a stupid reason: the link is essentially two hops between three disciplines:

• The literature around the Curry-Howard correspondence links structural proof theory to theoretical computer science, but the literature tends to turn on technicalities of the lambda-calculus that tend to frighten off philosophers;
• Dummett's work links structural proof theory to core theses of philosophical logic and philosophy of language, but his work and the literature around it tends to turn on such deeply metaphysical issues as the relationship of logic to the possibility of our knowing the real nature of the external world, which tends to frighten off computer scientists, theoretical or not.

The first chapter of my dissertation tried to bring together both links in a way that assumed no particular knowledge of structural proof theory, lambda calculus or philosophical logic, but just a general interest in and knowledge of logic. I didn't succeed, but it's probably a better attempt than anything else out there.

Martin-Löf has, of course, been talking about all of this for a long time, but his talks tend to trickle into publications at a glacially slow rate. Goran Sundholm is a good expositor of the link between proof theory and philosophy, but he doesn't really get into why the Curry-Howard correspondence is interesting to at least some computer scientists.

Greg knows what's going on here. Maybe he can say something.

Well, I sort-of-know what's going on maybe, but I'm preparing a talk to give here in a few hours. I'll comment later, but I don't have net access at home while I'm on sabbatical here in Oxford. So my posting/reading online is quite limited.

But I think Neil's take (hi, Neil!) is a nice clear presentation of M-L type theory. As Neil has emphasised (at least in conversation to me, and this is also in line with what I've read from M-L's materials, and from Göran Sundholm) M-L type theory all flows from the view of what judgements are. The same goes for Dummett, too, though the argument is quite different.

I was wondering if someone took the time to analyze the connection, and (just as important) published on the topic...

Hmm... There's Charles' thesis. Perhaps Neil L has written something on the M-L and Dummett connection?

Perhaps surprisingly, the articles in the "25 years of constructive type theory" collection at print.google here don't mention Dummett at all.

...lambda-calculus that tend to frighten off philosophers; metaphysical issues...frighten off computer scientists...

Poor devils, they are just so weak...

... it's the one with the theoretical errors!

Great, than I'll read it once again. It is very nice theory.

Erm, are there errors? I did a quick google and coundn't find any references to error in Lof's theory... Could someone point me to a paper that outlines the shortcommings?

I was talking about the fact that theories can and do (at times) contain errors. Not about M-L.

If you take first order logic and try to build a type theory out of it, you end up with a dependently typed lambda calculus. In fact, the article linked in the main post is an example of just such a calculus.

I am definitely intrigued... will probably read the article soon. do you think there are advantages to reformulating a first order logic theorem into a typed lambda calculus for the purposes of computational analysis, theorem proving, etc? Is this essentially what Prolog does? Does a lambda viewpoint add any expressivity or is it completely equivalent.

There are two advantages, from my perspective. One is critical, and the other is just nice.

The killer advantage is that if you use a type theory, rather than "just" a logic, your theorem prover can construct proof witnesses for the theorems you prove. The theorem or goal will be a type, and the proof will be a lambda term. The reason this is critical is that theorem provers are large pieces of software dealing with problems at the outer limits of complexity that people can handle. They always have bugs. If you generate a proof term, you can easily[*] verify the deduction that the prover did, and use it to a) find bugs in your prover, and b) avoid believing false theorems.

The other nice thing is that having the actual proof in hand can tell you interesting things. For example, linear logic is the logic of resources. Having a "yes" or "no" answer to a goal in linear logic tells you whether or not there is some way to use the available resources to create some result state. If you have the proof term, you can look at it to figure out what the actual plan is -- what to do in what order.

[*] A proof checker is usually a hundred lines of code or so, rather than the hundred thousand for the theorem prover. It's small enough that you can give a hand proof of correctness for it, and it's small enough that other people can verify that proof.

I don't think this is the critical point; any means of deriving theorems needs to construct a proof, or a counterproof of some sort, or more generally a model or countermodel. Such systems don't always externalize this as a certificate (which is important if you want to convince other people that the system is right in some instance), but there is always some internal proof or whatever which could be externalized to certify a theorem.

The critical points are rather that a type theory gives :

1. a constructive proof, and
2. a nontrivial and, sometimes, decidable notion of proof (in)equivalence.

Constructive proofs are important for several reasons: they are usually clearer than pulling a rabbit out of a hat, they state a "cause" for truth, they form programs, and they are required in some instances (as for example Montague semantics).

A notion of proof equivalence is important because it tells you, if someone claims to have found a "new" proof, whether it is genuinely new or just a different perspective on an old proof. It is also important, of course, for programs, because evaluation is a particular method of showing the equivalence of proofs/programs.

Please try to be more constructive and courteous with your criticisms. (Feel free to edit your comment to improve it in that regard.)

Comments like yours could discourage authors of papers from posting here. Note that your comment appeared directly after a comment by the author of the current paper.

Regarding Postscript, if you want to read academic papers, you should make sure you have a good Postscript reader. On Windows, Ghostscript is usually good enough. In any case, that's really off topic here.

But look, these are notes from a talk I gave several years ago. If you don't like them then don't read them. There are plenty of other sources for this material. If you found the notes useful, and I assume that Ehud thought someone might, which is why he posted the link, then that's good, but if you didn't find them useful, why waste your time complainiing about it?

Indeed I did. I still do, by the way...

If you're going to be pedantic, you had better also be correct...

"A proposition is something of which we can understand an arbitrary (direct) proof." That just doens't parse at all well. At least say "for which...".

I think the quoted sentence is just fine, and it didn't trip me up for a second when I was reading the paper. We have proofs of propositions, not for them.

(And yes, I realize that this is equally pedantic. I'm mostly kidding...)

Quite fair enough, my apologies.

In an attempt to make amends for my lack of being constructive, I simply ran ps2pdf on my linux machine and produced a perfectly readable PDF of the original PS file, with properly scaling and smoothing fonts & the images intact. Please feel free to check it out.

I read the comments above as asserting either:

1. Some type theories have errors, but this one does not ("theoretical errors"=="they have not been shown to exist"), or else
2. There is some notion of a type theory which can "contain" errors -- represent erroneous program states in some way? And this one can do so?

I lean to (1), but it may be (2): I know very little about this field. In any case, I have not seen any indication here that there are any errors of fact in this particular presentation.

Just to clarify, a little history: Per Martin-Löf's original, extensional presentation of his type theory was not shown in that work to be consistent, and Jean-Yves Girard investigated PML's theory and found a contradiction in it. Years later, PML proposed a new, intensional formulation of the theory that involves things like arities, which is easily shown to be consistent and whose metamathematics is well understood. Neil Leslie presents a simplified version of the latter.

On the off chance that anyone here is inspired to read my DPhil, the theory presented in chapter two is "more intensional than the intensional version" since the judgements there are to be understood as straight claims about beta equality in the type lambda calculus, rather than any claims made in any more-or-less sophisticated logical framework. One of the points of so doing is to avoid the kind of circumlocutions the use of the logical framework leads PML to: the framework is to be interprated "pragmatically" while the proper theory is to beinterpreted "verificationistically". The scare quotes indicate involved topics in Dummettology.

Pure Type Systems are a generalization of the lambda cube, and are generally impredicative. Basically, impredicativity means that when you have a polymorphic type of the form forall a:type. T(a), you can instantiate the variable a with another polymorphic type. (System F is also impredicative.)

In these systems, you can define sum types without anything but functions and universal quantification -- basically you can use the Church encoding of sums. In fact, you can use this method to code up pretty much any algebraic data structure.

The method you note using booleans and sums also works, but many implementations of the Calculus of Constructions and related systems leave out dependent sum on purpose. This is because adding an unrestricted dependent sum makes the logic inconsistent -- you can use it to type a Y combinator, and use that to show that every type is inhabited. Obviously, this is bad if you're using the type theory to do theorem proving! You have to limit yourself to "small" sigma-types to preserve strong normalization, and this is sufficiently unaesthetic that they often just leave 'em out.

Martin-L\"{o}f type theory very carefully avoids this, because he's a constructivist, and constructivists don't like impredicative systems. If you try to give a semantics for types in System F, you'll find -- when you hit the universal quantifier -- that you have to quantify over the meanings of all types to give a meaning to the universal type. This is "morally dubious", since one of the type meanings you are quantifying is the one you're currently trying to define! To avoid this potential circularity, constructivists like to ensure that you can only quantify over things that have already been completely defined.

I'm pretty sure this rules out using a System F-style Church encodings to get all possible sums, but I'm not 100% sure. (There could be a really clever trick I'm missing.)

I also think, but am not certain, that dependent types are basically independent of predicativity. If you look at the lambda cube, you can add type operators, dependent types, and polymorphism independently of each other.

I've only skirted the edges of this sort of thing, so I tend to forget about little matters like predicativity and consistency.

Martin-Löf type theory very carefully avoids this, because he's a constructivist, and constructivists don't like impredicative systems.

So, I guess constructivists also don't care for the Calculus of Constructions?

Actually, the paper on Henk has some discussion of extending the Lambda cube to create a predicative variant of F_ω.

Even without Σ, I guess you can come pretty close to dependent sums using dependent types. Something like:

Sigma  : Πa:*. (a → *) → *
DepSum : Πa:*. Πb:a → *. Πx:a. b x → Sigma a b

(Assuming that's valid.)

neelk wrote: I'm pretty sure this rules out using a System F-style Church encodings to get all possible sums, but I'm not 100% sure.

In fact it doesn't, and the Girard system of encoding is based upon a technique by Martin-Löf, which IIRC he gives credit for in Proofs and Types. You do need much more machinery to carry out the encoding in ML type theory, though: you need predicative universes. Then the well-founded ordering induction (WFOI) type schema essentially gives you the Girard encoding. Note the actual WFOI schema gives you, for the naturals, something a bit more complex than the regular presentation of the natural numbers in ML type theory.

Thanks for the correction.

Since you seem knowledgeable about ML type theory, maybe you can clarify a puzzle for me. Whenever I read about W-types, I see mysterious comments to the effect that there are problems with their induction principles due to too much "junk" being around. Can you explain what people are referring to, and maybe a pointer to some literature about it?

I guess the problem is that you need to talk about universes in order to formulate the rules, which seems like too much machinery. But to formulate inductive elimination rules in a general way you need to be able to talk about the space of inferences that can quantify over the eliminated type, which doesn't seem too problematic to me.

The bigger problem with predicative universes is that they take so much offputting synactic overhead to define, when they are essentially a quite simple concept.

I figured this means: if x is of type T then C(x) is a type. But I'm also confused what C means.

ML type theory is a dependent type theory, so the result type C can depend on x. The C(x) just means that x may appear in the type expression C. The thing in the brackets is a hypothesis. In more familiar context notation, this would look like:

\Gamma, x:T |- C(x) type