Alpha-renaming of higher-order meta-expressions
- Motivated by tools for automaed deduction on functional programming languages and programs, we propose a formalism to symbolically represent $\alpha$-renamings for meta-expressions. The formalism is an extension of usual higher-order meta-syntax which allows to $\alpha$-rename all valid ground instances of a meta-expression to fulfill the distinct variable convention. The renaming mechanism may be helpful for several reasoning tasks in deduction systems. We present our approach for a meta-language which uses higher-order abstract syntax and a meta-notation for recursive let-bindings, contexts, and environments. It is used in the LRSX Tool -- a tool to reason on the correctness of program transformations in higher-order program calculi with respect to their operational semantics. Besides introducing a formalism to represent symbolic $\alpha$-renamings, we present and analyze algorithms for simplification of $\alpha$-renamings, matching, rewriting, and checking $\alpha$-equivalence of symbolically $\alpha$-renamed meta-expressions.
Author: | David SabelORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30:3-443156 |
ISSN: | 1868-8330 |
Parent Title (German): | Frankfurter Informatik-Berichte [; Nr. 2007,2] |
Series (Serial Number): | Frankfurter Informatik-Berichte ([2017, 2]) |
Publisher: | Goethe-Univ., Fachbereich Informatik und Mathematik, Institut für Informatik |
Place of publication: | Frankfurt am Main |
Document Type: | Working Paper |
Language: | English |
Date of Publication (online): | 2017/06/19 |
Year of first Publication: | 2017 |
Publishing Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Release Date: | 2017/06/26 |
Tag: | Alpha equivalence; alpha renaming; meta languages |
GND Keyword: | Programmiersprachen; Semantik; Umbenennung |
Page Number: | 18 |
HeBIS-PPN: | 405730985 |
Institutes: | Informatik und Mathematik / Informatik |
Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Sammlungen: | Universitätspublikationen |
Licence (German): | Deutsches Urheberrecht |