What is meant by “Capture-avoiding substitutions”?
Normally, the specific variable names that we chose in the lambda calculus are meaningless – a function of x is the same thing as a function of a or b or c. In other words: (λx.(λy.yx)) is equivalent to (λa.(λb.ba)) – renaming x to a and y to b does not change anything. From this, …