The lambda calculus excerpt on the site has some issues as well. It says: > Lambda Calculus is reduced from left to right, which is very important No, you can

The lambda calculus excerpt on the site has some issues as well. It says: > Lambda Calculus is reduced from left to right, which is very important No, you can do feasible reductions in any order. The problem is that you need to define β-conversion and normal forms (β normal from is obtained by repeatedly applying β-conversion to the leftmost redex). Also, the example reduction is just wrong. You cannot transform (λx. x x) (λx. x x) into x x (λx. x x) - that's just not how β-reduction works. Applying a β-reduction to that term yields the same term, because you substitute the second expression for x in the first, thus obtaining the input all over.