All Questions
1 question
11
votes
4
answers
1k
views
Why is alpha-equivalence in untyped $\lambda$-calculus substitutive?
This is something all introductory texts seem to avoid proving, and many even avoid stating.
We consider untyped $\lambda$-terms on some countably infinite alphabet. If $x$ is a variable and $p$ is ...