Confluence by decreasing diagrams

DOI10.1016/0304-3975(92)00023-KzbMath0803.68058MaRDI QIDQ1322164

Vincent van Oostrom

Publication date: 5 May 1994

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

zbMATH Keywords

abstract reduction systemsconfluence criterionlocal decreasingness

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Rewriting modulo isotopies in pivotal linear \((2,2)\)-categories ⋮ Unnamed Item ⋮ More problems in rewriting ⋮ Problems in rewriting III ⋮ Rewriting in higher dimensional linear categories and application to the affine oriented Brauer category ⋮ Unnamed Item ⋮ Layer Systems for Proving Confluence ⋮ Finding small counterexamples for abstract rewriting properties ⋮ Modularity in term rewriting revisited ⋮ From diagrammatic confluence to modularity ⋮ Control reduction theories: the benefit of structural substitution ⋮ Braids via term rewriting ⋮ Unnamed Item ⋮ Decreasing diagrams and relative termination ⋮ Confluence by Decreasing Diagrams ⋮ Rewriting modulo isotopies in Khovanov-Lauda-Rouquier's categorification of quantum groups ⋮ Modularity of Confluence ⋮ Decreasing diagrams with two labels are complete for confluence of countable systems ⋮ Using bisimulation proof techniques for the analysis of distributed abstract machines ⋮ Confluence: The Unifying, Expressive Power of Locality ⋮ a-Logic With Arrows ⋮ Development closed critical pairs ⋮ Diagrammatic confluence for Constraint Handling Rules ⋮ Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem ⋮ Decreasing Diagrams and Relative Termination ⋮ CSI – A Confluence Tool ⋮ Unnamed Item ⋮ De Bruijn's weak diamond property revisited ⋮ Proving Confluence of Term Rewriting Systems Automatically ⋮ Diagram techniques for confluence ⋮ Improving rewriting induction approach for proving ground confluence ⋮ Labelings for decreasing diagrams ⋮ Confluence without termination via parallel critical pairs ⋮ Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs ⋮ On reduction and normalization in the computational core

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• On multiset orderings
• On theories with a combinatorial definition of 'equivalence'
• Proving termination with multiset orderings
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Tree-Manipulating Systems and Church-Rosser Theorems