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

  • 1
    You may want to take the question to brand-new [cs.SE](http://cs.stackexchange.com)!2012-03-23

1 Answers 1

0

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.