Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems

DOI10.1145/322217.322230zbMath0458.68007OpenAlexW1979101142MaRDI QIDQ3908463

Gérard Huet

Publication date: 1980

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/322217.322230

zbMATH Keywords

operational semanticsconfluenceequational theoriesChurch-Rosser propertycombinatorial theoriesequality theorem proving

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items (only showing first 100 items - show all)

Context rewriting ⋮ Collapsed tree rewriting: Completeness, confluence, and modularity ⋮ Confluence of terminating membership conditional TRS ⋮ Completeness and confluence of order-sorted term rewriting ⋮ Extended term rewriting systems ⋮ Conditional rewriting logic: Deduction, models and concurrency ⋮ Infinite terms and infinite rewritings ⋮ Testing confluence of nonterminating rewriting systems ⋮ Completion procedures as semidecision procedures ⋮ Linear completion ⋮ Design strategies for rewrite rules ⋮ Conditional semi-Thue systems for presenting monoids ⋮ One-rule trace-rewriting systems and confluence ⋮ Critical pairs in term graph rewriting ⋮ Confluence up to Garbage ⋮ Game characterizations of logic program properties ⋮ Formalization of a λ-calculus with explicit substitutions in Coq ⋮ Unification in varieties of completely regular semigroups ⋮ A note on confluent Thue systems ⋮ Confluence of one-rule Thue systems ⋮ Shuffle polygraphic resolutions for operads ⋮ Axioms for a theory of signature bases ⋮ How to prove decidability of equational theories with second-order computation analyser SOL ⋮ Local confluence of conditional and generalized term rewriting systems ⋮ Towards automated deduction in cP systems ⋮ The conservation theorem for differential nets ⋮ Unnamed Item ⋮ Automated generation of illustrated proofs in geometry and beyond ⋮ Unnamed Item ⋮ Confluence: The Unifying, Expressive Power of Locality ⋮ Normal form in Hecke-Kiselman monoids associated with simple oriented graphs ⋮ Unification theory ⋮ New Undecidability Results for Properties of Term Rewrite Systems ⋮ A Transformational Approach to Prove Outermost Termination Automatically ⋮ General Idempotency Languages Over Small Alphabets ⋮ Strictly orthogonal left linear rewrite systems and primitive recursion ⋮ A PVS Theory for Term Rewriting Systems ⋮ Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem ⋮ On interreduction of semi-complete term rewriting systems ⋮ Decreasing Diagrams and Relative Termination ⋮ CSI – A Confluence Tool ⋮ Sorting via chip-firing ⋮ Identification of proofs via syzygies ⋮ Unnamed Item ⋮ Strongly analytic tableaux for normal modal logics ⋮ Inferring a tree from walks ⋮ A Non-Deterministic Multiset Query Language ⋮ Computing with relational machines ⋮ The ℛ-height of semigroups and their bi-ideals ⋮ Computing in unpredictable environments: Semantics, reduction strategies, and program transformations ⋮ Confluence without termination via parallel critical pairs ⋮ Confluence of algebraic rewriting systems ⋮ Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs ⋮ A rewriting coherence theorem with applications in homotopy type theory ⋮ On sufficient-completeness and related properties of term rewriting systems ⋮ On recursive path ordering ⋮ Reductions in tree replacement systems ⋮ n-level rewriting systems ⋮ The problems of cyclic equality and conjugacy for finite complete rewriting systems ⋮ Pushdown machines for the macro tree transducer ⋮ Unification in varieties of idempotent semigroups ⋮ A refinement of strong sequentiality for term rewriting with constructors ⋮ Proof by consistency ⋮ A catalogue of complete group presentations ⋮ Equivalences and transformations of regular systems - applications to recursive program schemes and grammars ⋮ Termination of rewriting ⋮ Thue systems as rewriting systems ⋮ Unification in combinations of collapse-free regular theories ⋮ Analysis of Dehn's algorithm by critical pairs ⋮ Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study ⋮ The Church-Rosser property for ground term-rewriting systems is decidable ⋮ Rewriting systems and word problems in a free partially commutative monoid ⋮ An axiomatic definition of context-free rewriting and its application to NLC graph grammars ⋮ On deciding the confluence of a finite string-rewriting system on a given congruence class ⋮ History and basic features of the critical-pair/completion procedure ⋮ Word problems and a homological finiteness condition for monoids ⋮ Linear numeration systems of order two ⋮ Only prime superpositions need be considered in the Knuth-Bendix completion procedure ⋮ Critical pair criteria for completion ⋮ Preperfectness is undecidable for Thue systems containing only length- reducing rules and a single commutation rule ⋮ On lexicographic semi-commutations ⋮ Explaining Gabriel-Zisman localization to the computer ⋮ Implementing first-order rewriting with constructor systems ⋮ Decidable sentences of Church-Rosser congruences ⋮ Orderings for term-rewriting systems ⋮ Finite generation of ambiguity in context-free languages ⋮ Deterministic tree pushdown automata and monadic tree rewriting systems ⋮ Church-Rosser controlled rewriting systems and equivalence problems for deterministic context-free languages ⋮ Full abstraction and limiting completeness in equational languages ⋮ Using unavoidable set of trees to generalize Kruskal's theorem ⋮ Resource operators for \(\lambda\)-calculus ⋮ Series parallel digraphs with loops ⋮ Higher-order rewrite systems and their confluence ⋮ A polynomial algorithm testing partial confluence of basic semi-Thue systems ⋮ A \(\rho\)-calculus of explicit constraint application ⋮ Compositions with superlinear deterministic top-down tree transformations ⋮ A formalization of the Knuth-Bendix(-Huet) critical pair theorem ⋮ Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent ⋮ Tableaux and hypersequents for justification logics ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

This page was built for publication: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems