LIPIcs.RTA.2013.255.pdf
- Filesize: 0.52 MB
- 16 pages
Document
Algorithms for Extended Alpha-Equivalence and Complexity
Authors
-
Part of:
Volume:
24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2013-06-24
Cite AsGet BibTex
Manfred Schmidt-Schauß, Conrad Rau, and David Sabel. Algorithms for Extended Alpha-Equivalence and Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 255-270, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.RTA.2013.255
https://doi.org/10.4230/LIPIcs.RTA.2013.255
Abstract
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.
Keywords
- alpha-equivalence
- higher-order calculi
- deduction
- pi-calculus
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads