Home » forums » LtU Forum

Curry Howard and more powerful type systems

The ongoing thread On the (Alleged) Value of Proof for Assurance has sparked a discussion about applying the Curry Howard Isomorphism to more than intuitionistic logic and the simply typed LC. All these attempts are rather hand-wavey to me, but the discussion revolves around Isabelle and Coq, neither of which do I know.

Neelk has made it pretty clear that CH does not apply to Isabelle, but it has gotten me wondering.

* Is there a rigorous way to apply CH to a more powerful type system than the simply typed LC?

* Is it nonsensical to try and apply it?

* Does the ability to type-check non-terminating expressions have an impact? Similarly, do existential types? (I'm thinking F-Omega)

* Are there any articles/books that do apply it to more powerful type systems which are accessible to someone without a PhD?

By Brandon Niemczyk at 2010-03-23 01:43 | LtU Forum | previous forum topic | next forum topic | other blogs | 5041 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Answering the first question

Is there a rigorous way to apply CH to a more powerful type system than the simply typed LC?

Yes. A straightforward way to do it: ignore the terms.

Given a type judgement
(1) x1:A1, ..., xn:An |- M : A
remove the terms to obtain a sequent
(2) A1, ..., An |- A

Or, more formally, define a relation |- by: (2) iff there exist terms x1, ..., xn, M such that (1).

Now expose enough axioms, and you get a sound and complete sequent calculus for |-. If you view that calculus as a logic, then it is the logic isomorphic to the original type system via CH.

Usually the axioms exposed are simply the rules of the type system, with the isomorphism applied to them.

By Ohad Kammar at Tue, 2010-03-23 02:46 | login or register to post comments

OK, I'm pretty sure I am

OK, I'm pretty sure I am groking this correctly, but it begs the question:

The isomorphic logic is not necessarily intuitionistic logic, correct? Is there any practical use of finding an arbitrary isomorphic logic? I thought the great thing about CH is that existing knowledge of both the lambda calculus and logic could be used within the context of the other.

By Brandon Niemczyk at Tue, 2010-03-23 16:59 | login or register to post comments

The utility of correspondences

The isomorphic logic is not necessarily intuitionistic logic, correct?

That's right. For example, the referenced book details a correspondence between classical logic and a lambda calculus with control operators.

Is there any practical use of finding an arbitrary isomorphic logic? I thought the great thing about CH is that existing knowledge of both the lambda calculus and logic could be used within the context of the other.

Certainly finding a correspondence between two existing domains of study allows you to more easily translate knowledge from one to the other.

But it can also be a useful way to get a better look at the elephant that the different blind men on either side of the correspondence are describing.

It also may be the case that, for certain purposes, it's just more convenient to use one approach or the other, and the correspondence gives you the freedom to chose the side you want to work with.

Lastly, you might just like studying the things on both sides of the correspondence, and it gives you an excuse to combine them. ;-)

By Marc Hamann at Tue, 2010-03-23 17:18 | login or register to post comments

clueless question

is there a mathematical/logic term for the elephant in this particular situation?

By raould at Wed, 2010-03-24 18:36 | login or register to post comments

A Tricky Question

is there a mathematical/logic term for the elephant in this particular situation?

How someone will answer this will depend on the circumstances and their philosophical convictions (whether they are aware of them or not.)

Calling it "mathematical/logical truth or reality" is a possibility, but whatever it is, it is what we really want when we talk about "semantics".

I personally have my own name for it, though some people won't like it: computation. ;-)

By Marc Hamann at Wed, 2010-03-24 19:06 | login or register to post comments

There is a book

Are there any articles/books that do apply it to more powerful type systems which are accessible to someone without a PhD?

There is a book that covers this in great depth, taking the reader through the Lambda Cube and then some.

Do you need a PhD to read it? In the literal sense, I can vouch that the answer is no. In some ways it is a straightforward read, and fairly self-contained, though it certainly would be easier to read if you have pretty good grounding in lambda calculi, type systems, logic and proof theory.

All these attempts are rather hand-wavey to me

To make some of what we are talking about in that other thread rigorous enough to satisfy a broad range of perspectives would require a very thick book with a thick bibliography, plus many years of pain.

It is virtually impossible to make rigorous explanations in a forum like LtU, because they require too much space, study and detail. The best one can often do is to start with general statements of perspective and understanding, and drill down into little bits of technical detail as you uncover a shared basis of technical understanding with your interlocutors.

My apologies if that doesn't seem iron-clad enough for you. ;-)

By Marc Hamann at Tue, 2010-03-23 14:19 | login or register to post comments

Thanks for the book

Thanks for the book recommendation. It seems like what I'm looking for. I am ok with lambda calculi and type systems. One of the reasons I'm interested in learning more about CH is I'm hoping it can help me "bridge" some of my knowledge into formal logic and proof theory.

To make some of what we are talking about in that other thread rigorous enough to satisfy a broad range of perspectives would require a very thick book with a thick bibliography, plus many years of pain.

It is virtually impossible to make rigorous explanations in a forum like LtU, because they require too much space, study and detail. The best one can often do is to start with general statements of perspective and understanding, and drill down into little bits of technical detail as you uncover a shared basis of technical understanding with your interlocutors.

My apologies if that doesn't seem iron-clad enough for you. ;-)

No disrespect was intended, I probably should have chosen a better description. I just didn't really understand the explanation as it was and I was hoping for something that at least pointed the reader to relevant references. The book referenced above seems to fit the bill.

By Brandon Niemczyk at Tue, 2010-03-23 14:42 | login or register to post comments

Try before you buy

One of the reasons I'm interested in learning more about CH is I'm hoping it can help me "bridge" some of my knowledge into formal logic and proof theory.

Before you shell out big bucks for the published form, be sure to check out the freely-available pre-version mentioned in the linked thread.

It is fairly different from the final one, and I do think the final one is a more polished and elegant presentation (I certainly don't regret buying it), but it would give you an idea what the complexity level and basic content is. If you find that tough going, I would recommend opting for more introductory texts in the relevant sub-disciplines before going whole hog.

No disrespect was intended

None taken. Even though you wrote it, I'm sure there were countless other LtU readers who were thinking it. ;-)

By Marc Hamann at Tue, 2010-03-23 15:18 | login or register to post comments