Talk:Curry–Howard correspondence

Curry-Howard-Lambek

I have removed the term "Curry-Howard-Lambek" from the article as well as some weasel words "Some people refer to the Curry-Howard-Lambek" correspondence. The only place I am able to find the term Curry-Howard-Lambek is the nlab article on "computational trinitarianism" which makes some dramatic and sensational claims about how higher category theory, proof theory and programming language theory are but three perspectives on a single fundamental unifying phenomenon relating computation, logic and space. The hyperbolic language raises red flags for me as I think that it looks bad when Wikipedia articles are uncritical of sensationalist rhetoric. A second problem is that categorical treatments of type theory generally do not capture either beta reduction of programming languages or cut elimination in logics which are both central to the Curry-Howard correspondence. — Preceding unsigned comment added by 100.11.110.225 (talk) 02:41, 13 October 2023 (UTC)

An Error

In the section Curry-Howard-Lambek correspondence there's a remark at the very end:

"Now, there exists $t$ such that $t:\!\!-~\alpha _{1}\times \ldots \times \alpha _{n}\vdash \beta$ iff $\alpha _{1},\ldots ,\alpha _{n}\vdash \beta$ is provable in implicational intuitionistic logic,."

No citation is offered. This is incorrect -- to see why, just notice that $\alpha _{1}\times \alpha _{2}\vdash \alpha _{1}\times \alpha _{2}$ is true in a CCC but its not true that $\alpha _{1},\alpha _{2}\vdash \alpha _{1}\times \alpha _{2}$ in implicational intuitionistic logic. The latter sentence is not even grammatical in implicational intuitionistic logic.

The relationship to intuitionistic logic is complicated; the logic provided corresponds to the fragment of intuitionistic logic with $\top$ and $\wedge$, but not $\bot$ and $\vee$. Full intuitionistic logic corresponds to a calculus similar to the one presented, but for bicartesian categories. I know this from folklore among logicians and independent research. I will work on a citation. -- Negacthulhu 10:04, 5 July 2010 (UTC) —Preceding unsigned comment added by 207.224.51.38 (talk)

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)

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)

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)

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)

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)

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)

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)

Of course, as you already (or probably should) know: the relations between the two fall under the header of the Automath project and all other endeavors related to or inspired by it. So, your request is really an implicit request to include a link in the main article to Automath. — Preceding unsigned comment added by 129.89.251.51 (talk) 21:49, 7 October 2011 (UTC)

Who is the audience?

I'm having a pretty hard time reading this article. I have only a vague idea of what intuitionistic logic is, I don't know what "Hilbert-style" logic is, and I only know what "the empty type" and "the singleton type" are from the discussion later in the article that explains that they are bottom and unit, which I have vague ideas about from ⓐ trying to read papers on formal logic and ⓑ using OCaml.

The simplest remedy for this is to simply link everything up to Intuitionistic_logic, Heyting_algebra, Complete_heyting_algebra (which is the same thing as a "locale", which in turn is the type of lattice the Open_sets of a Topological_space form; also see Birkhoff's_representation_theorem, Pointless_toplogy and Stone_duality), Typed_lambda_calculus, Categorical_abstract_machine, Category_theory, Categorical_logic, Topos, Proof_theory, Sequent_calculus, Natural_deduction and Gentzen. There's never a reason, opportunity (or excuse) to say "I don't know" when you're in the middle of the an Encyclopedia(!)

But I know what the lambda-calculus is, I have some experience programming in OCaml, and I've proved simple theorems in first-order predicate logic textbook exercises, although I don't know which first-order predicate logic. Last year I wrote a λ-calculus interpreter that works by reducing λ-expressions to combinator graphs (although I had forgotten this was called "abstraction elimination") and then performing combinator-graph reduction to evaluate them.

So I have the idea, perhaps unreasonable, that I ought to be able to read an article introducing the Curry-Howard isomorphism. A friend of mine explained some of the basics to me some years ago: that you can write functions with type α × β → α, or α × β → β, or α → β → α, or α → β → β, or α × (α → β) → β, but not functions of type, say, α → β, because then what would type β be? Nor can you write a function of type α × (β → α) → β, because that function doesn't have any way to come up with any particular value of type β; all it has is an input that could transform some value of type β to a value of type α, if you had a β to start with. And that this corresponds pretty much exactly to the

But the article doesn't seem to be written with people like me in mind. It assumes a lot of background knowledge that I don't have, and without which I am unable to make much sense of the article. I have tried to read papers on the application of symbolic logic to programming occasionally for ten years now, without success.

On the perhaps vain hope that this is merely an oversight, rather than that the article is intended for people who already know a lot about symbolic logic, I am listing the things that I wish were explained in the article:

• What are "product types" (tuple types?), "sum types" (discriminated unions?), "the empty type" (an empty set, i.e. the absence of a result for programs that crash or hang?) and "the singleton type"?
• What are "dependent product" and "dependent sum"?
• Are the formulas "α → (β → α)" and "(α → (β → γ)) → ((α → β) → (α → γ))" the only possible axiom schemes? ("schemas"?)
• Is "Γ₁, α, Γ₂ ⊢ α" supposed to be parsed as "(Γ₁, α, Γ₂) ⊢ α" or as "Γ₁, α, (Γ₂ ⊢ α)"? Do the commas mean "and"? If so, why are there two Γs?
• In the table of inference rules, I am guessing that the things above the line are the sufficient conditions from which we can derive the things below the line? But I thought the things on the left side of the ⊢ were the sufficient conditions for deriving the thing on the right side of the ⊢? Are the horizontal line and ⊢ just different notations for the same thing?
• What does "Γ₁, x : α, Γ₂ ⊢ x : α" mean? I guess the colon indicates that what comes before it is of the type that follows it? Does this mean that we can deduce that x is of type α, or something else? Or does it represent that we can compute the value of x itself, given its value? I have the impression, perhaps false, that even if my other confusions about notation would be obvious to anyone who knew anything about logic, that the meaning of this side of the table is likely to only be comprehensible to someone who already understands the correspondence.
• I assume the "constructor" under "Programming side" refers to things like Just and Nothing, which construct a value of some type, and not the meaning of "constructor" from C++? What is a "destructor" in that context, just any function that pattern-matches on values of such a type?
• In the example of proving α → α, in the first step, where do the formulas α, β → α, and α come from? They clearly aren't the types of S, K, and K.

I am restricting my complaints to sections that I feel I would have some hope of understanding if the notation and vocabulary were explained. Perhaps placing some examples earlier in the article, before explaining the general principles, would help too.

If there is another article that explains this stuff, or if it is felt peripheral to the point of this article, maybe there could be a link early in the article saying, "The symbolic logic notation used in this article is briefly explained in some thousand-word-or-less article explaining the basics of the notation"?

I think that, in general, one of the things that makes an article encyclopedic is that it is accessible to the lay public.

I hope this is helpful, and I am grateful for the work of the article's many editors over the years in attempting to bring the Curry-Howard light to us unenlightened peons, even though their work has not been able to penetrate my thick skull.

Kragen Javier Sitaker (talk) 10:54, 22 December 2008 (UTC)

I think these are all good criticisms that should be addressed... One quick fix: it might help to read section 4 on natural deduction<->lambda calculus before reading section 3 on Hilbert-style deduction<->combinatory logic. It seems section 4 explains some of the notation used in section 3, such as the list notation for contexts...and in general lambda calculus/ND make a lot more sense than combinatory logic/Hilbert-style deduction ;) Perhaps section 4 was written first, and the order was reversed to reflect the chronological order? From an expository point-of-view, I think it would be best to explain ND<->λ first, since both sides (or at least the right-) are most familiar. Noamz (talk) 08:39, 30 September 2009 (UTC)

Minor question on Origin, scope, and consequences

The second paragraph of the first section ends with, "This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run." This seems like a non sequitur. What is a "form of logic programming" supposed to mean? Functional programming? Noamz (talk) 08:15, 30 September 2009 (UTC)

Church vs Curry in General Formulation

I'm not sure it's a good idea to talk about Church vs Curry and intersection/union types so soon. Currently the article states only that there is a choice of how to interpret the universal and existential quantification, but this applies just as well in the binary case of conjunction and disjunction. So I think it would be better to discuss intersection and union types (both binary & infinitary versions) either in a later section, or perhaps leave them out of the article entirely (because I don't think there is a well-established answer as to what they correspond on the logic side). Noamz (talk) 08:26, 30 September 2009 (UTC)

Agreed. I've just read that part of the article for the first time, and I think at best it is confusing, at worst it is wrong. The links to "intersection types" and "union types" don't help, because they only talk about binary intersections and unions, which is the normal meaning of the term. It seems that what is meant is intersection (or union) indexed by an element of a type - which seems like a dependent type to me, and that's what I'm used to seeing them called even when they are curry-style. Church vs curry affects what kinds of expressions are in the language, but it doesn't affect the structure of the types. I think leaving out this distinction is best unless someone has a good reference for why it's important to make it. —Preceding unsigned RowanD (talk) 07:33, 19 July 2010 (UTC)

What is the interest in using of The curry-howard correspondence for proof assistant for instance Coq?

Hi, Thank you if you can answer!

I'm living in France and try to learn mathematical logic on french and english wikipedia ,because mathematics fascinate me and I got interested in Automated theorem proving ...The question may appear to be stupid, but I don't understand what does it permit to use such a correspondence in proof assistant? From what I understood, it can be useful for normalisation of deductions ( changing deduction to one which is nicer), but I don't understand how it can permit to more easily prove that a statement is true or false?

I'll be very grateful if you can answer me! Thank you for all of you for having written this page.

--Nicobzz (talk) 16:28, 23 December 2010 (UTC)

It means you can have a computer do the proof for you, instead of doing it by hand. It also means that when you have a proof, then you also have an algorithm, and so maybe you can use that algorithm to compute something useful. You can also automatically search for proofs, using, for example, genetic algorithms. More generally, simply being aware of the correspondence makes it easier to think clearly about what one is actually doing. 99.153.64.179 (talk) 21:24, 26 June 2013 (UTC)

Homotopy type theory

At the risk of making this article longer, there should be some quick review of homotopy type theory which, one could say, is version 2.0 of the ideas here. After reviewing a bunch of basic type-theory articles at WP (e.g. product type, dependent type) its woefully clear that these are lacking as compared to what can be found in e.g. chapter 1 of the HoTT book. The ncatlab website one-ups the HoTT book in these areas, e.g. dependent+sum+type at the nLab by not only defining terms but also showing how category theory models some of these ideas from type theory. So, I guess I'm saying that each one of these correspondences could be worked up into a full-fledged article: e.g. how a dependent product type is like an universal quantifier, worked out in detail. This correspondence goes even further: John Baez has an article "Rosetta Stone" which notes that cartesian-closed cats are generalized by symmetric monoidal categorys; that the internal language of CCC's being simply typed lambda calc is similarly generalized by linear logic, and that both of these correspond in turn to cobordisms. (The mind-bender is, of course, that cobordisms underlie string theory, and homotopy underlies K-theory so the connections/equivalences/etc are... fascinating?) So basically, the correspondence described here is broader/deeper/wider than this article lets on, and even the basics here can certainly be articulated in much greater detail. 99.153.64.179 (talk) 21:18, 26 June 2013 (UTC)

I just now added a tame version of above to the end of the article. Much work is still needed on many other articles; besides the many different basic type articles, but also these red links: equality type identity type which eventually should lead to univalence axiom, but also more simply judgement (type theory) judgement (logic) judgement (sequent calculus) to discuss the internal/external split of reasoning about logic. And inhabited type is a redlink. 99.153.64.179 (talk) 22:17, 26 June 2013 (UTC)

Curry-Howard or BHK?

The article gives no references that Curry and Howard first discovered this, and Robert Harper (computer scientist) writes (also without references):

Neither Curry nor Howard discovered the principle (Howard himself disclaims credit for it), though they both did make contributions to it. Moreover, this unfortunate name deprives credit to those who did the real work in inventing the concept, including Brouwer, Heyting, Kolmogorov, deBruijn, and Martin-Löf. (Indeed, it is sometimes called the BHK Correspondence, which is both more accurate and less grandiose.) (from "Extensionality, Intensionality, and Brouwer’s Dictum")

75.15.115.75 (talk) 06:43, 1 August 2013 (UTC)

A Google search reveals an Elsevier logic vol 149 Lectures on the Curry-Howard Isomorphism which probably documents reasons for denoting the isomorphism this way. Philip Wadler's notes on The Curry-Howard Isomorphism include Howard's 1980 "The formulae-as-types notion of construction" I am reminded of how Richard Feynman could never quite utter the word "Feynman" in connection with his Feynman Diagrams. He would not vocalize his name in this context. This similarity points to Howard as the originator of the isomorphism, even if Howard never took credit. The community of researchers has already awarded the credit. __Ancheta Wis   (talk | contribs) 11:31, 1 August 2013 (UTC)

On a related note, I've always wondered why we have a separate article on the BHK interpretation. The reference there (Troelstra, A. (1991). "History of Constructivism in the Twentieth Century" (PDF). {{cite journal}}: Cite journal requires |journal= (help) Section 5.5.) does give some additional detail on both their histories. —Ruud 09:09, 1 August 2013 (UTC)

Wadler has documented the history in Propositions as Types:

This reading of proofs goes back to the intuitionists, and is often called the BHK interpretation, named for Brouwer, Heyting, and Kolmogorov. Brouwer founded intuitionism, and Heyting and Kolmogorov formalised intuitionistic logic, and developed the interpretation above, in the 1920s and 1930s. Realisability, introduced by Kleene in the 1940s, is based on a similar interpretation.

Given the intuitionistic reading of proofs, it hardly seems surprising that intuitionistic natural deduction and lambda calculus should correspond so closely. But recall that Gentzen invented Sequent Calculus because he could not find a direct proof of the Subformula Property for Natural Deduction, and the direct proof was not published until three decades later, by Prawitz. As pointed out to Howard by Martin Löf, Prawitz’s technique for normalising a proof corresponds exactly to reduction of lambda terms. Gentzen, Church, and Prawitz never drew these parallels. Certainly Howard was proud of the connection he drew, citing it as one of the two great achievements of his career [43]. While the connection may be obvious in retrospect, it was far from obvious in prospect!

Howard’s paper divides into two halves. The first half explains a correspondence between two well-understood concepts, the propositional connectives &, ∨, ⊃ on the one hand and the computational types ×, +, → on the other hand. The second half extends this analogy, and for well-understood concepts from logic proposes new concepts for types that correspond to them. In particular, Howard proposes that the predicate quantifiers ∀ and ∃ corresponds to new types that we now call dependent types.

His sources include Howard himself Howard on Curry-Howard.

I have tried to format this, because I can not read it, but I gave up

                                     a:β → α, b:γ → β, g:γ ⊢ b : γ → β    a:β → α, b:γ → β, g:γ ⊢ g : γ
———————————————————————————————————  ————————————————————————————————————————————————————————————————————
a:β → α, b:γ → β, g:γ ⊢ a : β → α      a:β → α, b:γ → β, g:γ ⊢ b g : β
————————————————————————————————————————————————————————————————————————
               a:β → α, b:γ → β, g:γ ⊢ a (b g) : α
               ————————————————————————————————————
               a:β → α, b:γ → β ⊢ λ g. a (b g) : γ → α
               ————————————————————————————————————————
                        a:β → α ⊢ λ b. λ g. a (b g) : (γ → β) -> γ → α
                        ————————————————————————————————————
                                ⊢ λ a. λ b. λ g. a (b g) : (β → α) -> (γ → β) -> γ → α

Started to format with LaTeX, but I failed.

${\frac {a:\beta \to \alpha ,\ b:\gamma \to \beta ,\ g:\gamma \mathop {\ \vdash \ } b:\gamma \to \beta \qquad \qquad a:\beta \to \alpha ,\ b:\gamma \to \beta \mathop {\ \vdash \ } g:\gamma }{\frac {a:\beta \to \alpha \mathop {\ \vdash \ } }{\mathop {\ \vdash \ } }}}$

I do not know how to do this without the \infer macro

I also think that Bfgx=f(gx) where x : α, g : α → β, f : β → γ, Bfg : α → γ is more familiar for programmers and those who know Bfg as f.g

If I failed to fix this, what to say my intent to build commuting diagrams.

maybe someone more skilled than me can make this article more readable — Preceding unsigned comment added by 2806:107E:4:15E:218:DEFF:FE2B:1215 (talk) 10:32, 27 May 2017 (UTC)