Skip to content

Instantly share code, notes, and snippets.

@jorendorff
Last active August 29, 2015 13:56
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jorendorff/9193867 to your computer and use it in GitHub Desktop.
Save jorendorff/9193867 to your computer and use it in GitHub Desktop.

λ-calculus Bonus Material!

Credit where it’s due

The author of the talk I gave yesterday at PyTennessee is Jim Blandy. Jim is a Mozilla engineer, a go player, a drinker of tea, and one of the most generous people I’ve ever met.

Bits and pieces

  • Are the Church numerals 32-bit integers? Or 64-bit integers? Or do they go on forever?

  • Subtraction is tricky. Here’s the code to subtract 1 from a Church numeral:

    sub1 = lambda n: (lambda f: lambda x: (n (lambda g: lambda h: h(g(f))))(lambda u: x)(lambda u: u))
    

    I’m still unraveling that one.

    But the great thing about functions is that you don’t have to understand how they work in order to use them. Here’s the full subtraction function, based on sub1 above:

    # simply repeat sub1 b times
    sub = lambda a: lambda b: b(sub1)(a)
    
  • How could boolean values be represented? What are the key operations? We found a definition of the numbers that let us tell them apart; how will you tell the booleans true and false apart?

  • The definition of exponentiation is astonishingly simple:

    pow = lambda a: lambda b: b(a)
    

    Why is that? Can you explain this function in English words?

  • What does this expression evaluate to?

    (lambda x: x(x))(lambda x: x(x))
    

There are more lambdas than lambdas

I had to drop this from Jim’s talk, to fit in the time we had, and really wish I could have gotten to it. But it does require a little background.

There are different sizes of infinite sets.

  • “Same size”, for both finite and infinite sets, means there exists a full one-to-one pairing of the two sets.

  • The integers are the same size as the even integers.

  • The integers are the same size as the naturals.

  • The integers are the same size as the fractions. (For each i, list all the fractions in least terms that, say, have numerator and denominator that add up to i; now number them. The numbering pairs integers with fractions.)

  • But there are more real numbers than integers! (Cantor’s diagonal proof. Incidentally if you are already familiar with this stuff you might like Cantor’s other proofs of this statement.)

How many functions are there?

Let’s start with a finite example. Consider all functions that take a whole number from 1 to 10 and return a boolean value. How many such functions are there? (Two functions only count as different if they give different answers for at least one of the ten possible inputs; it is possible for the same function to be implemented two different ways.)

The answer: 210 different functions.

The general formula is: the size of the set of functions A → B — that is, the set of all possible functions with domain (argument type) A and range (return type) B — is len(B) ** len(A).

So how many lambdas are there?

  • Call F the set of all lambdas.

  • What is the domain of a lambda? It must be F. So is the range.

  • So F is the set of functions with domain F and range F: F = F → F

  • So the size of F is len(F) ** len(F).

There's a problem, here. There's no such size. If A > 1, then A**A is always larger than A. Even when A is infinite, len(A→A) is always a larger infinity than len(A); you can prove it with a diagonalization argument. Thus, the set F = F → F doesn’t exist.

This made mathematicians suspicious of the λ-calculus for a while!

There’s more crazy going on here than I can quickly dispense with, but one way to get out of at least some of the trouble we’ve got ourselves into here is to consider that maybe lambdas and functions are not exactly the same thing. Every lambda denotes a function, but not every function can be written as a lambda.

A function is any mapping of inputs to outputs. A lambda is a rule mapping inputs to outputs. For some mappings, it’s easy to write a rule: there’s an obvious pattern to the inputs and outputs. The stronger the pattern, the shorter and simpler the rule. But some mappings, that is, some functions, have no discernable pattern. Those cannot be written down as a finite expression in the λ-calculus.

Or, assuming that the λ-calculus is a good definition of what computers can do: some functions are not computable.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment