License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.255
URN: urn:nbn:de:0030-drops-40667
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4066/
Schmidt-Schauß, Manfred ;
Rau, Conrad ;
Sabel, David
Algorithms for Extended Alpha-Equivalence and Complexity
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.
BibTeX - Entry
@InProceedings{schmidtschau_et_al:LIPIcs:2013:4066,
author = {Manfred Schmidt-Schau{\ss} and Conrad Rau and David Sabel},
title = {{Algorithms for Extended Alpha-Equivalence and Complexity}},
booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
pages = {255--270},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-53-8},
ISSN = {1868-8969},
year = {2013},
volume = {21},
editor = {Femke van Raamsdonk},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4066},
URN = {urn:nbn:de:0030-drops-40667},
doi = {10.4230/LIPIcs.RTA.2013.255},
annote = {Keywords: alpha-equivalence, higher-order calculi, deduction, pi-calculus}
}
Keywords: |
|
alpha-equivalence, higher-order calculi, deduction, pi-calculus |
Collection: |
|
24th International Conference on Rewriting Techniques and Applications (RTA 2013) |
Issue Date: |
|
2013 |
Date of publication: |
|
24.06.2013 |