From Wikipedia, the free encyclopedia

[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)