The notion of 𝛼-equivalence between 𝜆-terms is used to identify terms that are considered equal modulo renaming bound variables. Using De Bruijn indices we can give a unique representation for closed 𝜆-terms
modulo 𝛼-equivalence. Equating terms that have the same De Bruijn representation falls short when comparing subterms occurring within a larger context: it may equate either too few or too many subterms.

We have introduced (in a paper accepted for PLDI 2024) a formal notion of context-sensitive 𝛼-equivalence, where two open terms can be compared within a context that resolves their free variables. This equivalence coincides exactly with the notion of bisimulation equivalence and we have an efficient 𝑂 (𝑛 log 𝑛) runtime algorithm that identifies 𝜆-terms modulo context-sensitive 𝛼-equivalence.

In the talk I will start with some background of 𝜆-calculus as a computational model and the roles of 𝛼-equivalence, substitution and sub-term sharing in computing with 𝜆-terms.

Joint work with Lasse Blaauwbroek and Miroslav Olsak.