Evaluation: Run It!

There are only two real rules for evaluating expressions in λ calculus, called α conversion and β reduction.

α is a renaming operation. In λ calculus, the names of variables don’t have any meaning. If you rename a variable at its binding point in a λ and also rename it in all of the places where it’s used, you haven’t changed anything about its meaning. When you’re evaluating a complex expression, you’ll often end up with the same name being used in several different places. α conversion replaces one name with another to ensure that you don’t have name collisions.

For instance, if we had an expression like λ x . if (= x 0) then 1 else x^2, we could do an α conversion to replace x with y (written α[x/y]) and get λ y . ...

Get Good Math now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.