O'Reilly logo

Good Math by Mark C. Chu-Carroll

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 . ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required