2
$\begingroup$

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...

  • 0
    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.2011-08-07
  • 0
    I cannot be sure that this is possible. However it is proven in "standard" mathematics.2011-08-07
  • 0
    (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...2011-08-07
  • 0
    As seen on hi site [here](http://www.andrew.cmu.edu/user/awodey/), 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.2011-08-07
  • 1
    You may want to take the question to brand-new [cs.SE](http://cs.stackexchange.com)!2012-03-23

1 Answers 1