Algorithms for Extended Alpha-Equivalence and Complexity
Manfred Schmidt-Schauß, Conrad Rau, David Sabel · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2013
Equality of expressions in lambda-calculi, higher-order programming languages, higher-order programming calculi and process calculi is defined as alpha-equivalence. Permutability of bindings in let-constructs and structural congruence axioms extend alpha-equivalence. We analyse these extended alpha-equivalences and show that there are calculi with polynomial time algorithms, that a multiple-binding "let" may make alpha-equivalence as hard as finding graph-isomorphisms, and that the replication operator in the pi-calculus may lead to an EXPSPACE-hard alpha-equivalence problem.