[Zurück]

F. Schernhammer, J. Meseguer:
"Incremental Checking of Well-Founded Recursive Specifications Modulo Axioms";
in: "Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2011), July 20-22, 2011, Odense, Denmark", P. Schneider-Kamp, M. Hanus (Hrg.); herausgegeben von: Peter Schneider-Kamp and Michael Hanus; ACM Press, 2011, ISBN: 978-1-4503-0776-5, S. 5 - 16.

We introduce the notion of well-founded recursive order-sorted
equational logic (OS) theories modulo axioms. Such theories define
functions by well-founded recursion and are inherently terminating.
Moreover, for well-founded recursive theories important properties
such as confluence and sufficient completeness are modular
for so-called fair extensions. This enables us to incrementally check
these properties for hierarchies of such theories that occur naturally
in modular rule-based functional programs. Well-founded recursive
OS theories modulo axioms contain only commutativity and
associativity-commutativity axioms. In order to support arbitrary
combinations of associativity, commutativity and identity axioms,
we show how to eliminate identity and (under certain conditions)
associativity (without commutativity) axioms by theory transformations
in the last part of the paper.

http://dx.doi.org/10.1145/2003476.2003481

http://publik.tuwien.ac.at/files/PubDat_206726.pdf