Thursday, September 17, 2009

Simply Typed Lambda Calculus vs. Untyped

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-typed things that you have around. The Untyped Lambda Calculus, however, allows programs that never terminiate. I guess the Y-combinator is a pretty good example here. I once learned that the Untyped Lambda Calculus can be embedded inside the Typed Lambda Calculus by having essentially one type, the everything type. So I guess this makes sense, since there are no arrow types that can decrease monotonically...

Now I have more questions: 
Does this mean the untyped lambda calculus is Turing complete?
How does the encoding of the untyped lambda calculus into the lambda calculus work? I mean, don't functions always have to have function type? Or is the everything type some kind of function type?

8 comments:

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

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

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

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

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

    ReplyDelete
  6. Yes, that makes sense! Thanks.

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

    ReplyDelete