A recursive definition of what an expression is

(written by lawrence krubner, however indented passages are often quotes). You can contact lawrence at: lawrence@krubner.com, or follow me on Twitter.

I like this:

We’ll give a recursive definition of what an expression is; in other words, we’ll state what the most basic kind of expression is, we’ll say how to create new, more complex expressions out of existing expressions, and we’ll say that only things made in this way are valid expressions.

Variables are valid expressions.

If ee is any expression, and xx is any variable, then λx.eλx.e is an expression. Here it helps to think of e as typically (thought not necessarily) a more complex expression involving xx, e.g. x2+2×2+2, and then λx.eλx.e as the anonymous function that takes an input xx and returns the result of evaluating the expression ee with the given value of xx. In other words, think of it like this:

function(x) { return x^2 + 2; }

If ff and ee are valid expressions, then f(e)f(e) is a valid expression. This is called Application, for obvious reasons.

If xx is a variable, and e1e1 and e0e0 are valid expressions, then substituting every occurrence of xx in e0e0 for e1e1 yields a valid expression. So, for example, if e1e1 is the expression x2+2×2+2, and e0e0 is the expression y/3y/3, then if we let x=e0x=e0 in e1e1, we get the expression (y/3)2+2(y/3)2+2.
[NB: This last clause is redundant and not officially a part of the Lambda Calculus definition of an expression, as substituting e0e0 for xx in e1e1 is equivalent to applying the abstraction λx.e1λx.e1 to e0e0. It’s added to support something called let-polymorphism.]

And nothing else is a valid expression.

Post external references

  1. 1
    http://akgupta.ca/blog/2013/06/07/so-you-still-dont-understand-hindley-milner-part-2/
Source