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 . ...
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Read now
Unlock full access