Simply Typed Lambda Calculus vs. Untyped

[nolacoaster]

Today I learned something new! At first it was startling, but in hindsight it makes perfect sense: The Simply Typed Lambda Calculus is not Turing complete. Any well-typed program will eventually terminate, and the intuition here is that your program can only have a finite number of arrow types, and evaluation will always reduce the number of arrow-

Comments

[jcreed]

Yes, the un(i)typed lambda calculus is turing-complete.

If you want a typed model of the untyped lambda calculus, the everything type, call it D, has to be isomorphic ("has to be effectively the same type as") to D → D. The everything type is a function type, and its functions expect an everything and return an everything.

To actually describe what this set of things is carefully, you sometimes resort to tricky domain-theory tricks invented by Dana Scott.

[jcreed]

Note that that typed lambda calculus that has D = D → D is decidedly not the simply-typed lambda calculus anymore, and of course it can't be, since it's turing complete and the STLC is not.

[nolacoaster]

Yes, that makes sense! Thanks.

[simrob]

The encoding of the untyped lambda calculus into the lambda calculus.

I actually don't know what this means, and the way I interpret it it shouldn't be possible...

[nolacoaster]

This is just me paraphrasing a comment made by Bob four years ago in 814 that a typed language is strictly more expressive than an untyped language because you can encode an untyped language in a typed one where every single value has the same type.

As jcreed points out above, if you want to encode the untyped lambda calculus with a typed language, that language cannot be the simply typed lambda calculus, because it's not Turing complete.

[nolacoaster]

I can give more details after we get to that lecture in 814 (which I am sitting in on, four years later). :-)

[simrob]

Aah, yes. You can encode the untyped lambda calculus into a lambda calculus with one recursive type "μx.x→x", but not the simply typed lambda calculus, per jcreed. I was just confused by the setup.