Incremental checking of well-founded recursive specifications modulo axioms

Felix Schernhammer; José Meseguer

doi:10.1145/2003476.2003481

Incremental checking of well-founded recursive specifications modulo axioms

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English (US)
Title of host publication	PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
Pages	5-16
Number of pages	12
DOIs	https://doi.org/10.1145/2003476.2003481
State	Published - Sep 2 2011
Event	13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 - Odense, Denmark Duration: Jul 20 2011 → Jul 22 2011

Publication series

Name	PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

Other

Other	13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011
Country	Denmark
City	Odense
Period	7/20/11 → 7/22/11

Keywords

Conuence
Modularity
Order-sorted rewriting modulo axioms
Sufficient completeness
Termination
Well-founded recursive theory

ASJC Scopus subject areas

Computational Theory and Mathematics
Applied Mathematics

Access to Document

10.1145/2003476.2003481

Fingerprint Dive into the research topics of 'Incremental checking of well-founded recursive specifications modulo axioms'. Together they form a unique fingerprint.

Cite this

Schernhammer, F., & Meseguer, J. (2011). Incremental checking of well-founded recursive specifications modulo axioms. In PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming (pp. 5-16). (PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming). https://doi.org/10.1145/2003476.2003481

Incremental checking of well-founded recursive specifications modulo axioms. / Schernhammer, Felix; Meseguer, José.

PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming. 2011. p. 5-16 (PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Schernhammer, F & Meseguer, J 2011, Incremental checking of well-founded recursive specifications modulo axioms. in PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming. PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming, pp. 5-16, 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011, Odense, Denmark, 7/20/11. https://doi.org/10.1145/2003476.2003481

@inproceedings{14fd2ba4784e40d998b5fb317f31a311,

title = "Incremental checking of well-founded recursive specifications modulo axioms",

abstract = "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.",

keywords = "Conuence, Modularity, Order-sorted rewriting modulo axioms, Sufficient completeness, Termination, Well-founded recursive theory",

author = "Felix Schernhammer and Jos{\'e} Meseguer",

year = "2011",

month = sep,

day = "2",

doi = "10.1145/2003476.2003481",

language = "English (US)",

isbn = "9781450307765",

series = "PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming",

pages = "5--16",

booktitle = "PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming",

note = "13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 ; Conference date: 20-07-2011 Through 22-07-2011",

}

TY - GEN

T1 - Incremental checking of well-founded recursive specifications modulo axioms

AU - Schernhammer, Felix

AU - Meseguer, José

PY - 2011/9/2

Y1 - 2011/9/2

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 -