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.

Download full text files

Export metadata

Author:David SabelORCiDGND
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
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
Institutes:Informatik und Mathematik / Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):License LogoDeutsches Urheberrecht