Document Open Access Logo

Algorithms for Extended Alpha-Equivalence and Complexity

Authors Manfred Schmidt-Schauß, Conrad Rau, David Sabel



PDF
Thumbnail PDF

File

LIPIcs.RTA.2013.255.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Manfred Schmidt-Schauß
Conrad Rau
David Sabel

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

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)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail