Strict Coherence of Conditional Rewriting Modulo Axioms

Meseguer, José

Permalink

https://hdl.handle.net/2142/50288 Copy

Description

Title

Strict Coherence of Conditional Rewriting Modulo Axioms

Author(s)

Meseguer, José

Issue Date

2014-08

Keyword(s)

Conditional rewriting modulo equations, coherence, order-sorted specifications, operational termination, Church-Rosser property.

Abstract

Conditional rewriting modulo axioms with rich types makes specifications and declarative programs very expressive and succinct and is used in all well-known rule-based languages. However, the current foundations of rewriting modulo axioms have focused for the most part on the unconditional and untyped case. The main purpose of this work is to generalize the foundations of rewriting modulo axioms to the conditional order-sorted case. A related goal is to simplify such foundations. In particular, even in the unconditional case, the notion of strict coherence proposed here makes rewriting modulo axioms simpler and easier to understand. Good properties of strictly coherent conditional theories, like operational equi-termination of the R/B and R;B relations and general conditions for the conditional Church-Rosser property modulo B are also studied.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/50288

Sponsor(s)/Grant Number(s)

Partially Supported by NSF Grant CNS 13-19109.

Owning Collections