Normal forms and normal theories in conditional rewriting

Salvador Lucas, José Meseguer

Research output: Contribution to journalArticle

Abstract

We present several new concepts and results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs), which support types, subtypes and rewriting modulo axioms, and contains the more restricted framework of conditional term rewriting systems (CTRSs) as a special case. The concepts shed light on several subtle issues about conditional rewriting and conditional termination. We point out that the notions of irreducible term and of normal form, which coincide for unconditional rewriting, have been conflated for conditional rewriting but are in fact totally different notions. Normal form is a stronger concept. We call any rewrite theory where all irreducible terms are normal forms a normal theory. We argue that normality is essential to have good executability and computability properties. Therefore we call all other theories abnormal, freaks of nature to be avoided. The distinction between irreducible terms and normal forms helps in clarifying various notions of strong and weak termination. We show that abnormal theories can be terminating in various, equally abnormal ways; and argue that any computationally meaningful notion of strong or weak conditional termination should be a property of normal theories. In particular we define the notion of a weakly operationally terminating (or weakly normalizing) OSRT, discuss several evaluation mechanisms to compute normal forms in such theories, and investigate general conditions under which the rewriting-based operational semantics and the initial algebra semantics of a confluent, weakly normalizing OSRT coincide thanks to a notion of canonical term algebra. Finally, we investigate appropriate conditions and proof methods to ensure that a rewrite theory is normal; and characterize the stronger property of a rewrite theory being operationally terminating in terms of a natural generalization of the notion of quasi-decreasing order.

Original languageEnglish (US)
Pages (from-to)67-97
Number of pages31
JournalJournal of Logical and Algebraic Methods in Programming
Volume85
Issue number1
DOIs
StatePublished - Jan 2016

    Fingerprint

Keywords

  • Conditional term rewriting
  • Maude
  • Normal forms
  • Normal theory
  • Operational termination
  • Rewriting logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Software
  • Logic
  • Computational Theory and Mathematics

Cite this