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.
Verfasserangaben: | David SabelORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30:3-443156 |
ISSN: | 1868-8330 |
Titel des übergeordneten Werkes (Deutsch): | Frankfurter Informatik-Berichte [; Nr. 2007,2] |
Schriftenreihe (Bandnummer): | Frankfurter Informatik-Berichte ([2017, 2]) |
Verlag: | Goethe-Univ., Fachbereich Informatik und Mathematik, Institut für Informatik |
Verlagsort: | Frankfurt am Main |
Dokumentart: | Arbeitspapier |
Sprache: | Englisch |
Datum der Veröffentlichung (online): | 19.06.2017 |
Jahr der Erstveröffentlichung: | 2017 |
Veröffentlichende Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Datum der Freischaltung: | 26.06.2017 |
Freies Schlagwort / Tag: | Alpha equivalence; alpha renaming; meta languages |
GND-Schlagwort: | Programmiersprachen; Semantik; Umbenennung |
Seitenzahl: | 18 |
HeBIS-PPN: | 405730985 |
Institute: | Informatik und Mathematik / Informatik |
DDC-Klassifikation: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Sammlungen: | Universitätspublikationen |
Lizenz (Deutsch): | Deutsches Urheberrecht |