HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

Modular Aspects of Rewrite-Based Specifications

Bernhard Gramlich 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We investigate modular properties of term rewriting systems, the basic operational formalism for equational specifications. First we study sufficient conditions for the preservation of the termination property under disjoint (and more general) combinations of term rewriting systems. By means of a refined analysis of existing approaches we show how to prove several new asymmetric preservation results. For this purpose we introduce two interesting new properties of term rewriting systems related to collapsing reductions: uniquely collapsing and collapsing confluent. We discuss these properties w.r.t.~well-known confluence, consistency and normal form properties, and show that they are modular for left-linear systems, but not in general.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00073359
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 12:36:54 PM
Last modification on : Friday, February 4, 2022 - 3:31:46 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:43:46 PM

Identifiers

  • HAL Id : inria-00073359, version 1

Collections

Citation

Bernhard Gramlich. Modular Aspects of Rewrite-Based Specifications. [Research Report] RR-3330, INRIA. 1997, pp.20. ⟨inria-00073359⟩

Share

Metrics

Record views

65

Files downloads

268