Towards correctness of program transformations through unification and critical pair computation
- Correctness of program transformations in extended lambda-calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules, which results in so-called complete sets of diagrams. The method is similar to the computation of critical pairs for the completion of term rewriting systems. We explore cases where the computation of these overlaps can be done in a first order way by variants of critical pair computation that use unification algorithms. As a case study of an application we describe a finitary and decidable unification algorithm for the combination of the equational theory of left-commutativity modelling multi-sets, context variables and many-sorted unification. Sets of equations are restricted to be almost linear, i.e. every variable and context variable occurs at most once, where we allow one exception: variables of a sort without ground terms may occur several times. Every context variable must have an argument-sort in the free part of the signature. We also extend the unification algorithm by the treatment of binding-chains in let- and letrec-environments and by context-classes. This results in a unification algorithm that can be applied to all overlaps of normal-order reductions and transformations in an extended lambda calculus with letrec that we use as a case study.
Author: | Conrad Rau, Manfred Schmidt-SchaußORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30-71275 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-41-v1.pdf |
Parent Title (English): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 41 |
Series (Serial Number): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (41) |
Publisher: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology |
Place of publication: | Frankfurt [am Main] |
Document Type: | Working Paper |
Language: | English |
Year of Completion: | 2010 |
Year of first Publication: | 2010 |
Publishing Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Release Date: | 2010/09/04 |
Issue: | Version: 12 Juni 2010 |
Page Number: | 16 |
First Page: | 1 |
Last Page: | 16 |
HeBIS-PPN: | 226607933 |
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 |