TY - GEN
T1 - Incremental checking of well-founded recursive specifications modulo axioms
AU - Schernhammer, Felix
AU - Meseguer, José
PY - 2011
Y1 - 2011
N2 - 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 conuence 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.
AB - 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 conuence 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.
KW - Conuence
KW - Modularity
KW - Order-sorted rewriting modulo axioms
KW - Sufficient completeness
KW - Termination
KW - Well-founded recursive theory
UR - http://www.scopus.com/inward/record.url?scp=80052164663&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=80052164663&partnerID=8YFLogxK
U2 - 10.1145/2003476.2003481
DO - 10.1145/2003476.2003481
M3 - Conference contribution
AN - SCOPUS:80052164663
SN - 9781450307765
T3 - PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
SP - 5
EP - 16
BT - PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
T2 - 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011
Y2 - 20 July 2011 through 22 July 2011
ER -