Not covered in this PDF but extremely important is the notion of substitution. This is the only computational operation of the lambda calculus, and is the reaso

Not covered in this PDF but extremely important is the notion of substitution. This is the only computational operation of the lambda calculus, and is the reason why lambda calculus is Turing-complete. Substitution is also hard to get right, but here's how it would work with "fresh" variables[0]. Alternatively one may avoid names altogether and use de Bruijn indices[1], however there's a significant performance cost in doing so. See λ-calculus cooked four ways[2] for more information. [0] https://en.wikipedia.org/wiki/Lambda_calculus#Capture-avoiding_substitutions https://en.wikipedia.org/wiki/Lambda_calculus#Capture-avoidi... [1] https://en.wikipedia.org/wiki/De_Bruijn_index https://en.wikipedia.org/wiki/De_Bruijn_index [2] https://raw.githubusercontent.com/steshaw/lennart-lambda/master/top.pdf https://raw.githubusercontent.com/steshaw/lennart-lambda/mas...