University of Illinois Urbana-Champaign

Incremental Checking of Well-Founded Recursive Specifications Modulo Axioms

Schernhammer, Felix; Mseguer, Jose

Content Files
well-founded-recursion.pdf

Permalink

https://hdl.handle.net/2142/32095

Description

Title
Incremental Checking of Well-Founded Recursive Specifications Modulo Axioms
Author(s)
  • Schernhammer, Felix
  • Mseguer, Jose
Issue Date
2011-05-10
Keyword(s)
well-founded recursive theory, order-sorted rewriting modulo axioms, termination, confluence, sufficient completeness
Date of Ingest
2012-06-29T20:44:44Z
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 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.
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/32095

Owning Collections

Research and Tech Reports - Computer Science PRIMARY