2026-07-24T00:57:14Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4066 2024-03-06T10:34:46Z ddc:004 open_access

Algorithms for Extended Alpha-Equivalence and Complexity Schmidt-Schauß, Manfred Rau, Conrad Sabel, David alpha-equivalence higher-order calculi deduction pi-calculus 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manfred Schmidt-Schauß and Conrad Rau and David Sabel 2013 Is Part Of LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2013.255 urn:nbn:de:0030-drops-40667 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.255 eng https://creativecommons.org/licenses/by/3.0/legalcode