Code Mesh and infinite llamas

Kind of a companion post for a Code Mesh talk we did:

• Infinite Lambda Calculus
• The code we used for the talk
• The file we ended up with in the talk (it is what it is)
• Also there are some lambdas over here, generally speaking

Maybe the talk has a main point. Goes like this:

• We wanna get something like infinite, or at least pretty infinite, loops.
• Lambda calculus is Turing complete, but it kind of wasn’t supposed to be?
• Turing complete things can probably do infinite loops,
• Type systems tend to get rid of like accidental Turing completeness.

We can come up with a recipe for making a loopy thing:

• Look for a tiny expression that wouldn't typecheck if we had a type system-and-checker (if the type system doesn’t like an expression, then maybe that expression has something to do with Turing completeness and leads to infinite loops)
• Type checkers sure don’t like λx.x x
• (λx.x x) (λx.x x) goes on and on. Maybe for forever.
• Adding e.g. foo like so: (λx.x x) (λx.foo (x x)) will give us as many foos as we want. Doing a few steps of evaluation will get us foo (foo ((λx.foo (x x)) (λx.foo (x x)))). If we do more steps we get more foos.
• We can do this with any f, instead of just with foo, because lambda abstraction: λf.(λx.x x) (λx.f (x x))
• One step of evaluation takes us from λf.(λx.x x) (λx.f (x x)) to λf.(λx.f (x x)) (λx.f (x x))

λf.(λx.f (x x)) (λx.f (x x)) is the Y combinator :)