Incremental checking of well-founded recursive specifications modulo axioms

Felix Schernhammer, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationPPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
Pages5-16
Number of pages12
DOIs
StatePublished - Sep 2 2011
Event13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 - Odense, Denmark
Duration: Jul 20 2011Jul 22 2011

Publication series

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

Other

Other13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011
CountryDenmark
CityOdense
Period7/20/117/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

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