Code Mesh and infinite llamas


Possibly a bit of a companion post for the Code Mesh talk Infinite Lambda Calculus.

Importantliest: The code used, along with some instructions, is on GitHub. The, uh, file we ended up with in the talk also is. It is what it is.

(Also, there are some related lambdas like, nearby. It is possible to take a look over here, or just like play with stuff over there.)

Maybe the talk has a main point or something. It goes possibly like this:

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

  1. 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?)
  2. Type checkers sure don’t much like λx.x x.
  3. (λx.x x) (λx.x x) goes on and on. For maybe forever?
  4. Adding e.g. foo like so: (λx.x x) (λ (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 x)) (λ (x x)))). If we do more steps we get more foos.
  5. We can do this with like any f, instead of just with foo, because lambda abstraction: λf.(λx.x x) (λx.f (x x)).
  6. 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 :)