Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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|cite|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
You may want to take the question to brand-new cs.SE! – Raphael Mar 23 '12 at 23:35

Providing an answer just so that this question can be closed.

One way of showing that the expressive strength is different is to note that the simply-typed lambda calculus is strongly normalizing (see, e.g., Pierce: "Types and Programming Languages"), and hence, every function expressible in it terminates. On the other hand, the untyped lambda calculus is Turing-complete and can therefore express nonterminating functions.

share|cite|improve this answer

Your Answer


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

Not the answer you're looking for? Browse other questions tagged or ask your own question.