Code Mesh and infinite llamas
Possibly a bit of a companion post for the Code Mesh talk Infinite Lambda Calculus.
Maybe the talk has a main point or something. It goes possibly 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 leads to Turing completeness and infinite loops?)
- Type checkers sure don’t much like λx.x x.
- (λx.x x) (λx.x x) goes on and on. For maybe forever?
- Adding e.g. foo like so: (λx.x x) (λx.foo (x x)) will give us (more than) 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 like any f, instead of just with foo, because lambda abstraction: λf.(λx.x x) (λx.f (x x)).
- One step of evaluation takes λ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 :)