Filtern
Erscheinungsjahr
- 2017 (1) (entfernen)
Dokumenttyp
- Arbeitspapier (1) (entfernen)
Sprache
- Englisch (1) (entfernen)
Volltext vorhanden
- ja (1)
Gehört zur Bibliographie
- nein (1) (entfernen)
Schlagworte
- Semantik (1) (entfernen)
Institut
- Informatik (1) (entfernen)
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.