Beta reduction is essentially function application. If you have a function described by what it does to x and apply it to an argument t, you rewrite the xs as ts. The formal definition of β-reduction is more complicated than this in order to account for free versus bound variables, but this informal description is sufficient for this blog post. We will first show that β-reduction holds some surprises, then explain how these surprises go away when you add typing.
Suppose you have an expression (λx.x + 2)y, which means apply to y the function that takes its argument and adds 2. Then β-reduction rewrites this expression as y + 2. In a more complicated expression, you might be able to apply β-reduction several times. When you do apply β-reduction several times, does the process always stop? And if you apply β-reduction to parts of an expression in a different order, can you get different results?
Failure to normalize
You might reasonably expect that if you apply β-reduction enough times you eventually get an expression you can’t reduce any further. Au contraire!
Consider the expression (λx.xx) (λx.xx). Beta reduction says to replace each of the red xs with the expression in blue. But when we do that, we get the original expression (λx.xx) (λx.xx) back. Beta reduction gets stuck in an infinite loop.
Next consider the expression L = (λx.xxy) (λx.xxy). Applying β-reduction the first time gives (λx.xxy) (λx.xxy) y or Ly. Applying β-reduction again yields Lyy. Beta “reduction” doesn’t reduce the expression at all but makes it bigger.
The technical term for what we’ve seen is that β-reduction is not normalizing. A rewrite system is strongly normalizing if applying the rules in any order eventually terminates. It’s weakly normalizing if there’s at least some sequence of applying the rules that terminates. Beta reduction is neither strongly nor weakly normalizing in the context of (untyped) lambda calculus.
Types to the rescue
In simply typed lambda calculus, we assign types to every variable, and functions have to take the right type of argument. This additional structure prevents examples such as those above that fail to normalize. If x is a function that takes an argument of type A and returns an argument of type B then you can’t apply x to itself. This is because x takes something of type A, not something of type function from A to B. You can prove that not only does this rule out specific examples like those above, it rules out all possible examples that would prevent β-reduction from terminating.
To summarize, β-reduction is not normalizing, not even weakly, in the context of untyped lambda calculus, but it is strongly normalizing in the context of simply typed lambda calculus.
Confluence
Although β-reduction is not normalizing for untyped lambda calculus, the Church-Rosser theorem says it is confluent. That is, if an expression P can be transformed by β-reduction two different ways into expressions M and N, then there is an expression T such that both M and N can be reduced to T. This implies that if β-reduction does terminate, then it terminates in a unique expression (up to α-conversion, i.e. renaming bound variables). Simply typed lambda calculus is confluent as well, and so in that context we can say β-reduction always terminates in a unique expression (again up to α-conversion).
I rather like these neat, simple posts making some straightforward point. In this case, though, I note the phrasing is lopsided in favor of the constrained side: “failure”; “rescue”. An opposing bias would describe types as “crippling” general computation.
Good point. I’ve been working with theorem proving where you’re trying to be as expressive as you can while avoiding general computation because it introduces the potential for undecidable problems.
Very nice explanation.
I think “α-equivalence” or “α-conversion” is more correct, instead of “α-reduction”. https://twitter.com/jb9i
You can use a type system that has infinite types and then you can get the y combinator to type check.
Not necessarily desirable, but infinite reduction series can be represented by infinite types.
True, once you step beyond standard typed language calculus, there are type systems that allow such things.
In general, a type system provides a formal proof system for allowability of term construction; you aren’t allowed to construct a term unless you can prove it’s allowed. The alternative is to let terms be constructed, and then have the reduction process fail later on if it tries to do something bad. But, thanks to Godel, either your type system still permits some terms that will later fail, or it excludes some terms that would succeed. (Here, the failure is non-halting, so the undecidability is the halting problem.)
To apply these concepts to practical code, these are the sorts of rules that allow a compiler to optimize away code and function calls, iff the functions in question are 1) pure and 2) typed. Am I following the application correctly?