Talk:Curry-Howard correspondence

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: Start Class Mid Priority  Field: Foundations, logic, and set theory
Please update this rating as the article progresses, or if the rating is inaccurate. Please also add comments to suggest improvements to the article.

This is the talk page for discussing improvements to the Curry-Howard correspondence article.
Article policies

Contents

[edit] A Second Version

I've felt for some time that this article doesn't give a good introduction to the general reader of what the C-H isomorphism is really about. I had started writing an article about the C-H isomorphism when this article was put up. I haven't had an opportunity to finish mine, but perhaps someone would like to take it and use it, perhaps to supplement the article that is here now.

I've placed my partial draft at Curry-Howard isomorphism/Alt. Please consider my version of that article to have been released under the terms of the GNU FDL. I would be delighted if someone would complete it. -- Dominus 17:47, 13 May 2004 (UTC)

I've put this all in; basically it is there now topped-and-tailed with general discussion. Possibly some of the discussion of styles of intuitionistic proof could in time be moved to appropriate logic articles.

Charles Matthews 08:25, 14 May 2004 (UTC)


Again, we have a switch between C <-> B. Changing

DefLog 05:34, 18 May 2004 (UTC)

Yes, I seem to have gotten them mixed up some time in the distant past. At least my confusion is consistent. Thanks for all the corrections. -- Dominus 14:13, 18 May 2004 (UTC)

[edit] To Dos & Name change

I've taken these items from the main body: they shouldn't be public:

  • Proof normalization
  • Pierce's law as call-with-current-continuation cf. continuation
  • Sequent calculus
  • Product and union types analogous to and and or
  • Exception types analogous to false

Also, I've charged in and moved the article from ...isomorphism to ...correspondence: it's my impression the latter is more common in the scientific literature, and it avoids the resulting sillinesses that arise when talking informally about an isomorphism. ---- Charles Stewart 18:29, 25 Aug 2004 (UTC)

My impression was the opposite, and google finds five times as many hits for "isomorphism" as "correspondence". -- Dominus 21:50, 25 Aug 2004 (UTC)
I didn't try that. Since a lot of these are Wikipedia mirros, it's not quite an unbiased test: I added the token "site:citeseer.ist.psu.edu" to the search and got 60 for correspondence and 167 for iso, which is a ratio of about 2.8. Do you think the change should be reversed? I'm running against the Wikipedia popularity policy here, but talking of correspondence rather than iso does relieve some tortured phrases. ---- Charles Stewart 22:41, 25 Aug 2004 (UTC)
Well in a very precise sense it is an isomorphism and therefore all the more remarkable. I've just run across this article and found it really doesn't express the most important part of the isomorphism (that it functions at the level of reductions as well). It needs considerable work. Francis Davey 22:24, 4 Dec 2004 (UTC)

Well, hello Francis. Charles Matthews 23:22, 4 Dec 2004 (UTC)

Hello to you. I mostly post legal articles (having become a lawyer) but I still amuse myself by thinking about logic and programs in my "spare" time. I am sorry to be slightly critical of the article, but it seems to me that one ought to start by explaining the straightforward correspondance between natural deduction normalisation and beta reduction of simply typed lambda calculus (and the other levels of proofs, types etc). Then one can descibe (1) ways of expanding the correspondence; and (2) links with other systems. At the moment we have sequent calculus and not natural deduction, but the isomorphism between cut-elimination and normalisation is itself hard. Francis Davey 15:58, 7 Dec 2004 (UTC)

The ideal WP article on this may be a way off. It should be a survey, initially, and certainly no more prescriptive than typical usage is (for example the Hilbert system business is not my approach, but I have seen in print someone saying it was a revelation etc.). I see there is now a compositionality article, which ought to be a help - but probably isn't right now. I like 'compilation' and Kolmogorov (i.e. that what CH does is to nail down some heuristics about solutions to problems in full gory syntactic detail). I used to think that 'compiler verification' was going to explain why we needed this (Chalst is going to think this all very naive, and others too, no doubt ...) until I realised that no one ever verifies compilers anyway. It's not hard to work out that four people looking at the article have come up with four perspectives; so this is time to knuckle down to some classic wiki editing that deals even-handedly withe everything that gets raised. Charles Matthews 17:14, 7 Dec 2004 (UTC)

[edit] The naming problem

I've got a long past with this topic, so much so that I probably can't be objective about certain details: my doctorate was on the so-called classical Curry-Howard correspondence and begins with a rant about the misleading way the topic is made use of in many works in the field. While the centre of the topic was Bill Howard's 1969 manuscript, which indeed presented an isomorphism between two formal systems, there are reasons to prefer not to call the topic the Curry-Howard isomorphism, and these are some of mine:

  • Howard's manuscript was called The formulae-as-types notion of construction, the terminology formulae-as-types correspondence is closest to the source;
  • The topic does not consist in the first place of showing an isomosophism, rather it consists of establishing first an intuitive observation of a correlation between certain notions of construction in type theory, and certain patterns of inference in logic; the presentation of an isomorphism is rather a virtuoso flourish that adds force to this observation. To insist on talk of isomorphism obscures the most important part, which is the intuitive and I think necessarily informal part;
  • There are many important aspects of the theory that cannot be put into isomorphism, because what would have to be regarded as the logical counterpart of the type theoretic construction makes no logical sense: the clearest development of this problem is in Zhaohui Luo's Computation and Reasoning, where he discusses the problems applying the formulae-as-types correspondence to the Extended Calculus of Constructions (essentially one cannot mix dependent sum with System F like polymorphism and expect the result to be entirely logic-like);
  • There's something artificial about Howard's isomorphism: while the simply-typed lambda calculus is a calculus of an obviously fundamental nature, there's something forced about the logical end, namely the idea of labelling assumptions and implies elimination rules. The labels are needed for the isomorphism to work, but before the work of Curry and Howard, no-one working with natural deduction thought to keep track of these; instead the assumption was simply that all assumptions matching the implies elimination rule are discharged.

As a last point, if I am convinced that 'Curry-Howard isomorphism' is the more widely used term, the people whose judgement I respect most mostly prefer 'formulae-as-types correspondence'; and at the risk of sounding elitist, I think we should prefer the better term even when it is less popular. My preference for this page are:

  1. Formulae-as-types correspondence;
  2. Curry-Howard correspondence;
  3. Curry-Howard isomorphism;

with the latter only under sufferance; also note that the phrase 'Curry-Howard' is disrespectful to those logicians who contributed fundamental insights; I would particularly single out William Tait in this respect. ---- Charles Stewart 02:26, 7 Dec 2004 (UTC)

My own impression, that there isn't an 'official' isomorphism, is reinforced rather than otherwise by all that. We could of course just call the page 'Curry-Howard' and have done. And the history should be on the page. Charles Matthews 08:30, 7 Dec 2004 (UTC)
Certainly it should have a history section, and as noted above the rewriting aspect is weak. To draw out the properly logical dimension of the rewriting aspect depends on making some account of Prawitz's inversion principle, which is a long put-off task for me. As for the name, what about just formulae-as-types? That actually occurs as a substring of Howard's manuscript title.---- Charles Stewart 11:16, 7 Dec 2004 (UTC)
We're a bit constrained by the principle that the title should be the common name. (Cf. recent hassles with Hausdorff dimension - it is well established here that the article title is not the place to deal with correct attribution.) I don't really like formulae-as-types; I once put it to Martin Hyland that the proofs-as-programs level was more perspicuous, and he said it was much better. Anyway I would prefer C-H in the title, just because that's how the computer scientists habitually refer to it. Charles Matthews 11:53, 7 Dec 2004 (UTC)
In any case, I don't think your suggestion changes anything for the worse, and since it splits the difference between isomorphism/correspondence I guess applying the move is a good thing. If there are no objections, I'll apply the change tomorrow ---- Charles Stewart 12:45, 7 Dec 2004 (UTC)

[edit] Inhabitation not clear

Is the statement that there is no proof of (α → α) → β related to some particular restricted version of lambda calculus? It should probably be explained better why there is no proof. It seems weird. As far as I know, the usual lambda calculus is Touring equivalent, and you can definitely write a program that receives a function of type α → α and returns an arbitrary value of some other type. -- Jirka6

There is no proof of (α → α) → β. (And a good thing, since this sentence is false.) I'm not sure why you think Turing-equivalence is relevant. If you think that a lambda-calculus program can be written that has type (α → α) → β, perhaps you should try to write one and present it here. -- Dominus 18:09, 11 March 2007 (UTC)
I am no expert on lambda calculus (that's why I am reading this :). Since there is no error, the section should probably be a little bit clearer so that novices like me have an easier time. Are there some implicit limitations on the lambda calculus in question? I was bringing up the Turing equivalence, because I can definitely write a program for TM, or equivalently in Java or Haskell, that does that. For example, the following simple function does exist and has the type (α → α) → β:
fnc :: (int -> int) -> String
fnc f = "abc"
So apparently I am missing something.--Jirka6 01:23, 12 March 2007 (UTC)


That function does not have type (α → α) → β; it has type (int → int) → String. Actually its most general type is α → String, but that is not what you were looking for, right? -- Dominus 02:12, 12 March 2007 (UTC)


Are α and β some distinguished types? According to section Types, α and β are type variables, so when I set α = int and β = String, the typing of the function fnc corresponds to (α → α) → β. Anyway, how about if I write (using explicit typing) λxα → α . c where c is a constant of type β. Such function accepts objects of type α → α and returns an object of type β, so it should have type (α → α) → β --Jirka6 04:45, 12 March 2007 (UTC)
The type of fnc is not (α → α) → β, any more than the type of (λx → x+1) is (α → α); rather, it is (int → int). You seem to know Haskell, so you should know that the type (α → α) is not the same as the type (int → int). As for your constant of type β, there is no such constant. (We seem to be back to where we started: if you really think there is such a constant, can you exhibit one?) -- Dominus 04:58, 12 March 2007 (UTC)
I'm not trying to be unhelpful, but I'm not sure yet where your difficulty lies. Have you tried reading Type inference? Have you tried giving expressions to your Haskell interpreter and then asking it what types they have? -- Dominus 04:58, 12 March 2007 (UTC)
Thanks. I think that from your comment about the constant I got one thing. The section talks in the main article talks about a pure system without any non-logical axioms. Right? It is probably obvious, but maybe it should be stated explicitly. Moreover, I thought there are three possibilities: (i) a formula is a theorem - it is provable from axioms (one can find a term of that type); (ii) a formula is a contradiction, and (iii) the third possibility you cannot prove the formula is correct, but you can add some axiom that will enable to prove that formula without making the system inconsistent. Based on the wording of the section, I thought (α → α) → β is case (ii), which sounds weird, but it is just case (iii).
Re (λx → x+1) isn't of type (α → α) - I thought α just stands for an arbitrary type, that's why I asked if it is some distinguished type (I know that say Ty2 has only two types). —The preceding unsigned comment was added by Jirka6 (talk • contribs) 15:05, 12 March 2007 (UTC).
No, it's case (iii) that holds. If (α → α) → β were a theorem of logic, then the system would be inconsistent, and absolutely anything would be provable. (α → α) is a theorem, so β would follow by modus ponens, and then by substitution, you have anything you want.
In the programs-as-types side of the isomorphism, if you had a function `f` of type (α → α) → β, then you could get absolutely any type you wanted out, by calculating something like (f (λx → x)). But that makes no sense, because there is no such function f that would do that.
α really stands for stands for the type ∀α.α. Int is an instance of ∀α.α, but not vice versa. Similarly (int → int) is an instance of ∀α.(α → α), but not vice versa.
There is a function of type ∀α.(α → α), and there is a function of type ∀α.(α → Int), and this latter function also is an instance of a function of type ∀αβ.((α → β) → Int). But there is no function of type ∀αβ.(α → α) → β, which is what you were asking about in the first place.
I don't know if this helps much. I'm hoping to understand where your confusion lies, so that we can fix up the article, if that is warranted. -- Dominus 18:13, 12 March 2007 (UTC)
Thanks a lot for the clarification.
First, regarding universally quantified types: First I was not sure what you mean by that because as far as I know, simply typed calculus is not polymorphic. However, should I think of the quantification as meta-quantification? In other words, when searching for terms of α → α, should I see α → α not as a particular type with α being a base type, but instead as a type schema "schema"? And search for an untyped term that could be assigned all types consistent with that schema? (I think this view was inaccessible for me since I was thinking in terms of Church's explicit typing). IF this is true, it seems logical since in propositional logic, by claiming "α → α is a theorem" one means that it is true for any α (even though prop. logic also does not have quantifiers). I think this should be made explicit, because the first sentence of the section talks about λ-expression with any given type without mentioning universal quantification or any schemata.
Second, Based on this discussion, I would suggest the following changes to the section:
  1. add closed to the first occurrence of lambda-expression with explanation in parenthesis (I know it is in the next para, but it is easy to overlook - I did overlook it).
  2. stress that we are talking about a purely logical system without any non-logical axioms, in other words there are no (non-logical) constants.
  3. replace the ξ in the typing of the first mentioned function with α. Otherwise, the reader might wonder if there is some reason for using ξ's in this place but α's in the next paragraphs.
  4. clarification about the universally quantified types
Jirka6 00:44, 13 March 2007 (UTC)

[edit] Proposal for revising the article

I'd like to propose a significant revision of the article. Stricto sensu, the Curry-Howard correspondance is the observation in Curry and Feys's book that typed combinatory logic coincided with the axioms for implication in Hilbert-Bernays logic, and the observation by Howard that the proofs of Gentzen's natural deduction could be seen as the terms of a typed lambda-calculus. In my opinion, the article should then be primarily built around these two observations and I would rather suggest the following structure:

  • Introduction
  • Minimal Hilbert-style logic and typed combinatory logic
    • A table for the correspondence
    • Some examples (such as the ones in current section Programs are proofs)
  • Minimal Natural deduction and simply-typed lambda-calculus
    • A table for the correspondence,
    • Some examples
  • Other aspects of the correspondence
    • Other connectives (and, or, quantifiers, absurd type)
    • Classical logic
    • Sequent calculus
  • Discussion
    • Other contributions to the correspondence: use of lambda-notation in Automath
    • Related works: realisability, BHK interpretation
    • Socio-mathematical stimulus: Martin-Löf type theory, Pure Type Sytems, linear logic, category theory
    • "Philosophical" or cultural issues: proving is the same as programming, validating a formula is the same as exhibiting an inhabitant in a type, ...

Especially, I would suggest

  • to remove the section Types of which the contents is already present in page Simply typed lambda calculus,
  • to move the contents of section The type inhabitation problem to the page Type inhabitation problem,
  • to remove the section Intuitionistic logic: its contents is mainly in page Intuitionistic logic,
  • to insert the section Programs are proofs in proposed section Minimal Hilbert-style logic and typed combinatory logic,
  • to rename the section Natural deduction in proposed section Minimal Natural deduction and simply-typed lambda-calculus,
  • to move the sections Classical logic and Sequent calculus as subsections in proposed section Extensions

I don't know what to suggest with the section Point of view of category theory. Did it provide some insights on the proofs-as-programs correspondence before Curry and Howard did (in which case it would typically go to section related works) or has it rather to be seen as a domain which benefited from the correspondence to investigate new topics (in which case it would typically go to section socio-mathematical stimulus). Hugo Herbelin (talk) 20:14, 18 December 2007 (UTC)

I think that all sounds superb, and I hope you go ahead with your plan and see it through to completion. My suggestion about the Point of view of category theory section would be to delete it. Ever since it was put in it has always seemed to me that it was more like "point of view of the one person who put it in". -- Dominus (talk) 14:38, 19 December 2007 (UTC)
I agree. At its narrowest (the combinatory logic / Hilbert system and the minimal logic / ND equivalence) can be constructed so that the word "isomorphism" is useful in context. That is less true the further away from these you move (eg the correspondence between sequent calculi and natural deduction systems is very subtle and not straightforward at all). Francis Davey (talk) 18:04, 19 December 2007 (UTC)
Yes, when moving from Hilbert system (and its correspondence with combinatory logic) and from ND (and its correspondence with typed lambda calculus) to sequent calculus, there is no longer an exact correspondence (in the sense of a matching of structures) between sequent calculus and a pre-existing notion of computation. However this is an active field of research to find such an appealing computational counterpart to sequent calculus and some progresses have already been made. Being personally involved in this field of research, I would however advance only with precaution to avoid any risk of undue subjectivity. 62.212.105.93 (talk) 17:04, 24 December 2007 (UTC)
Interesting, who are you and what are you doing? I spent a lot of time trying to use graphs (i.e. interaction nets/proof nets to do just this but resources are difficult). Really the problem with sequents is that they have a lot of bookkeeping information that is uninteresting logically and computationally so one wants to factor it out. Francis Davey (talk) 17:56, 24 December 2007 (UTC)
I'm a researcher in proof theory, lambda-calculus, etc. The extra bookkeeping information in sequent calculus (if I understand correctly what you mean by bookkeeping information) can be explained by the "fact" that sequent calculus has the potentiality to interpret both a call-by-name and a call-by-value lambda-calculus while ordinary natural deduction only contains a call-by-name lambda-calculus. More precisely, classical sequent calculus contains two dual subsystems called LKT and LKQ that respectively correspond (in the sense of the Curry-Howard correspondence) to a call-by-name and a call-by-value lambda-calculus. Hugo Herbelin (talk) 21:27, 24 December 2007 (UTC)
Finally I did not find anything really relevant to the Type inhabitation problem page in the Type inhabitation problem. The section had examples of inhabited and non inhabited types/propositions that were relevant for the current article but, for inhabitation, it was I, K and S which are already mentioned in the article, while for non inhabitation there were no convincing explanation of why they were non inhabited so I renounce to do anything with the examples. I deleted the section and the only reference to inhabitation is now in the main table of correspondences.
The section Point of view of category theory is very difficult to evaluate. It could not understand the relation between Curry-Howard and "compilation" mentioned in the section. Can the author or somebody else explain? Paragraph 3 was just general ideas about BHK interpretation and CCC and I did not see the link with Curry-Howard. Paragraph 4 suggested that Lambek contributed to the proof-as-program and formula-as-type correspondence. I followed the suggestion of Dominus and removed the section Point of view of category theory but I added in the related works section a subsection on the so-called Curry-Howard-Lambek correspondence that is referred to in some papers. Hugo Herbelin (talk) 21:29, 24 December 2007 (UTC)

I completed my process of revision. There are still many things to say and to improve but I believe I now have a consistent article and I stop here. I hope to have correctly preserved the significant informations that were present in the version of 21 December 2007 before I started the revision. I'm not fully satisfied by the typography of formulas and inference rules. I find the <math> environment not very elegant. I would have prefered to move everything to unicode but I have been told that some can't see symbols like ⊢ (the same using math mode: \vdash) in IE on Windows (by the way, a few of these unicode ⊢ are still in the article). Hugo Herbelin (talk) 17:48, 28 December 2007 (UTC)

Thanks very much. I printed it out a couple of days ago and was reading it over this morning. It is very clear and coherent, and I think it is a big improvement on what went before.
I marked up my printout with minor corrections to grammar and wording, and I will put these changes in when the opportunity arises.
Thanks again for your work on this article. -- Dominus (talk) 20:56, 28 December 2007 (UTC)

[edit] Article name

I moved from an en-dash that was in the article title, which is very unusual, to a hyphen as is used throughout it. Why was the en-dash in there, anyone know?

Now, I see above that there have been arguments about whether to name this "Curry-Howard isomorphism" or "Curry-Howard correspondence" -- but is "Curry-Howard" alone superior to either of those? Unless anyone has a good reason not to, I would like to have this moved back to "Curry-Howard isomorphism" (of the two, that gets by far the most google hits.) MilesAgain (talk) 12:32, 29 December 2007 (UTC)

I agree. -- Dominus (talk) 15:09, 29 December 2007 (UTC)
There were already a discussion about this question and I agree with Charles Stewart that it is more common to use the word correspondence in the scientific community than to use the word isomorphism. I think that the reason is double:
  • Curry-Howard is an isomorphism. But Curry-Howard is more than an isomorphism as it says that proofs and typed programs are identical. Otherwise said, if we care about formalizing them properly, we would define them exactly the same way. Hence, from the mathematical point of view, saying that Curry-Howard is an isomorphism is the same as saying that a square is a rectangle. A square is a rectangle, but you lose information when you say that a square is a rectangle.
  • At the beginning, Curry-Howard was a surprising and unexpected result. For logicians, proofs and programs were really thought as different at that time, and that's why, I think, the correspondence has been often thought as an isomorphism, i.e. as the property that two different kinds of objects had the same structure (but they are not different!).
Now that Curry-Howard is widely accepted and that logicians design calculi that are both proof systems and programming languages, it makes more sense IMHO to call it a correspondence rather than an isomorphism.
Then, if correspondence is, I think, better than, say identity (which would still be mathematically accurate), it is because even if they are mathematically the same, they are not exactly the same in the way we think about it. For proofs, the meaningful part is the proved formula while for typed programs, the meaningful part is the program. And more generally, there are still two distinct vocabulary.
Coming back to the primary question, whether the page should be called Curry-Howard or Curry-Howard correspondence, I have no serious opinion. The full name is a bit long to type in so I would prefer the short form but the long form is (again IMHO) more precise and could be preferable too.
I know that, even if I give arguments to lay my point of view, there is still a part of subjectivity in it, and I would be interesting to hear arguments in the other direction. Hugo Herbelin (talk) 18:38, 29 December 2007 (UTC)
You have convinced me that "Curry-Howard correspondence" is the right choice, but "Curry-Howard" alone is terrible because it's just a pair of names, not a noun phrase. Please understand that there will always be a redirect from Curry-Howard to this article, just as Curry-Howard correspondence redirects here now. I requested "Curry-Howard correspondence" at WP:RM. MilesAgain (talk) 05:04, 30 December 2007 (UTC)

[edit] Relationship with logic programming

The basic idea of logic programming is that axioms are programs and proofs are program executions, i.e. computations. As far as I know, there has been no correspondence shown between these different ideas.Logperson (talk) 12:39, 26 February 2008 (UTC)