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

$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – Zhen Lin
    Aug 7, 2011 at 11:08
  • $\begingroup$ I cannot be sure that this is possible. However it is proven in "standard" mathematics. $\endgroup$
    – stralep
    Aug 7, 2011 at 11:22
  • $\begingroup$ (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... $\endgroup$
    – Zhen Lin
    Aug 7, 2011 at 11:55
  • $\begingroup$ 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. $\endgroup$
    – stralep
    Aug 7, 2011 at 17:25
  • 1
    $\begingroup$ You may want to take the question to brand-new cs.SE! $\endgroup$
    – Raphael
    Mar 23, 2012 at 23:35

1 Answer 1

0
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .