Substitution in Untyped Lambda Calculus

Stream: Type theory

[Shashank Pathak]

Hi. This is not a Lean specific question. I am reading 'Untyped Lambda Calculus' from 'Type Theory and Formal Proofs - An Introduction' by Nederpelt and Geuvers. In it, the authors mention what they mean by the symbol $\equiv$. The call it syntactical identity. What I understand by this is if $M \equiv N$ for two $\lambda$-terms $M$ and $N$, then they are same as sequence of symbols.

When they define substitution, they define it recursively, and for the abstraction case they do it like this - $(λy . P )[x := N ] ≡ λz . (P^{y→z} [x := N ]),$ if $λz . P^{y→z}$ is an α-variant of $λy . P$ such that $z$ is not a free-variable in $N$. $P^{y → z}$ means replacing all free occurrences of $y$ in $P$ with $z$, and being an $\alpha$-variant means that one can be obtained from the other through $\alpha$-conversion.

My question is that if I consider $\equiv$ to be equality as a sequence of symbols, then this definition feels vague, because as there are probably countably many variables, I can choose many $z$ s satisfying the condition. Should I treat $\equiv$ as something less strict than syntactic identity? Thanks.

[Jannis Limperg]

Indeed (λ y, P)[x := N] is not uniquely defined by the clause you quote. This hopefully won't matter for the rest of the text because one virtually always considers lambda terms up to α-conversion, i.e. λ x, x and λ y, y are treated as the same.

The authors chose this iffy definition to address a technical issue called capture-avoiding substitution.

[Shashank Pathak]

Thanks. So, should I change my notion of equality of lambda terms to them being $\alpha$-convertible, i.e. two lambda terms are equal iff they are $\alpha$-convertible?

[Jannis Limperg]

Depends; there is no one right notion. I would say most of the time you want α-equality, but sometimes you want syntactic equality and I'm sure the book will also talk about αβη-equality.

[Shashank Pathak]

Oh, I see. Many thanks :)