Rewrite, rewrite, rewrite, rewrite, rewrite, \dots

DOI10.1016/0304-3975(91)90040-9zbMath0759.68044OpenAlexW2012961833MaRDI QIDQ1176247

Nachum Dershowitz, Stéphane Kaplan, David Alan Plaisted

Publication date: 25 June 1992

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(91)90040-9

zbMATH Keywords

normal formsalgebraic semanticsconfluenceterminationtransfinite derivations

Mathematics Subject Classification ID

Applications of universal algebra in computer science (08A70) Semantics in the theory of computing (68Q55) Grammars and rewriting systems (68Q42) Recursive ordinals and ordinal notations (03F15)

Related Items

Redex capturing in term graph rewriting (concise version) ⋮ Open problems in rewriting ⋮ More problems in rewriting ⋮ Head boundedness of nonterminating rewritings ⋮ On confluence and residuals in Cauchy convergent transfinite rewriting ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ Infinitary rewriting: meta-theory and convergence ⋮ Convergence in infinitary term graph rewriting systems is simple ⋮ CPO models for infinite term rewriting ⋮ Highlights in infinitary rewriting and lambda calculus ⋮ Computing in unpredictable environments: semantics, reduction strategies, and program transformations ⋮ Rational rewriting ⋮ Projections for infinitary rewriting (extended version) ⋮ Rewrite, rewrite, rewrite, rewrite, rewrite, \dots ⋮ Infinite normal forms for non-linear term rewriting systems ⋮ Deciding observational congruence of finite-state CCS expressions by rewriting ⋮ Projections for infinitary rewriting ⋮ Algebra and automated deduction ⋮ Computable total functions on metric algebras, universal algebraic specifications and dynamical systems ⋮ Some results on extensionality in lambda calculus ⋮ Infinitary combinatory reduction systems ⋮ On modularity in infinitary term rewriting ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Proving semantic properties as first-order satisfiability ⋮ Modularity of Convergence in Infinitary Rewriting ⋮ Unnamed Item ⋮ Orders, reduction graphs and spectra ⋮ Context-sensitive rewriting strategies ⋮ Infinitary affine proofs ⋮ On the complexity of stream equality ⋮ Computing in unpredictable environments: Semantics, reduction strategies, and program transformations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the algebraic specification of infinite objects - ordered and continuous models of algebraic types
• Conditional rewrite rules
• Corrigendum to ``Termination of rewriting
• Computing in systems described by equations
• Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
• REDEX CAPTURING IN TERM GRAPH REWRITING
• Infinite trees in normal form and recursive equations having a unique solution
• Operational and Semantic Equivalence Between Recursive Programs
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Data Types as Lattices
• Initial Algebra Semantics and Continuous Algebras
• Algebraic semantics and complexity of term rewriting systems
• Transfinite reductions in orthogonal term rewriting systems
• Infinite terms and infinite rewritings