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