Tell me more ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.
up vote 2 down vote favorite

How to prove that untyped $\lambda$ and simply typed $\lambda$ are of diferent expressive powers, using category theory?

I'm just getting to grips with the basic ideas of category theory, and I'm interested in this area of CS...

share|improve this question
Where did you get the idea that it could be done? Surely some references were given. I'm just speculating here, but I think the idea is to show that the two categories of $\lambda$ expressions are inequivalent. For instance, Awodey [2004; Chapter 6] shows that typed $\lambda$-calculus admits models by cartesian-closed categories, and that it is deductively sound and complete under this class of models. – Zhen Lin Aug 7 '11 at 11:08
I cannot be sure that this is possible. However it is proven in "standard" mathematics. – stralep Aug 7 '11 at 11:22
(Erratum: I mean Awodey [2010]. Not sure why I thought the book was published in 2004.) Well, what are your thoughts on the issue? Perhaps this question is more suited for cstheory.SE... – Zhen Lin Aug 7 '11 at 11:55
As seen on hi site here, original version of his book has been released 2006, and re-released 2010. I've found his lectures and problem sets there, so I will start with that. But I'm currently trying to learn CT, so I believe that this is more appropriate place for this question. – stralep Aug 7 '11 at 17:25
1  
You may want to take the question to brand-new cs.SE! – Raphael Mar 23 '12 at 23:35

Know someone who can answer? Share a link to this question via email, Google+, Twitter, or Facebook.

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.