Rewriting of higher-order-meta-expressions with recursive bindings

  • We introduce rewriting of meta-expressions which stem from a meta-language that uses higher-order abstract syntax augmented by meta-notation for recursive let, contexts, sets of bindings, and chain variables. Additionally, three kinds of constraints can be added to meta-expressions to express usual constraints on evaluation rules and program transformations. Rewriting of meta-expressions is required for automated reasoning on programs and their properties. A concrete application is a procedure to automatically prove correctness of program transformations in higher-order program calculi which may permit recursive let-bindings as they occur in functional programming languages. Rewriting on meta-expressions can be performed by solving the so-called letrec matching problem which we introduce. We provide a matching algorithm to solve it. We show that the letrec matching problem is NP-complete, that our matching algorithm is sound and complete, and that it runs in non-deterministic polynomial time.

Download full text files

Export metadata

Author:David SabelORCiDGND
Parent Title (German):Frankfurter Informatik-Berichte [; Nr. 2007,1]
Series (Serial Number):Frankfurter Informatik-Berichte ([2017, 1])
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:matching; program transformation; rewriting; verification
GND Keyword:Terrmersetzungssystem; Reduktionssystem
Page Number:16
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