Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
From MaRDI portal
Publication:3908463
DOI10.1145/322217.322230zbMath0458.68007OpenAlexW1979101142MaRDI QIDQ3908463
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
operational semanticsconfluenceequational theoriesChurch-Rosser propertycombinatorial theoriesequality theorem proving
Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)
Related Items
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, Attributed graph transformation with inheritance: efficient conflict detection and local confluence analysis using abstract critical pairs, Some decision problems about controlled rewriting systems, Decreasing diagrams and relative termination, Equational completion in order-sorted algebras, A characterisation of deterministic context-free languages by means of right-congruences, An algorithm for the construction of matrix representations for finitely presented non-commutative algebras, A rationale for conditional equational programming, Weighted graphs: A tool for studying the halting problem and time complexity in term rewriting systems and logic programming, Rigid E-unification: NP-completeness and applications to equational matings, Modular termination of \(r\)-consistent and left-linear term rewriting systems, Confluence for graph transformations, Towards a foundation of completion procedures as semidecision procedures, Modularity in noncopying term rewriting, Redundancy criteria for constrained completion, Some undecidable termination problems for semi-Thue systems, On proving confluence modulo equivalence for Constraint Handling Rules, Strict coherence of conditional rewriting modulo axioms, Testing for the ground (co-)reducibility property in term-rewriting systems, On weakly confluent monadic string-rewriting systems, Approximate XML structure validation based on document-grammar tree similarity, Importing logics, Quasi-interpretations. A way to control resources, Anti-patterns for rule-based languages, Conditional linearization, On the confluence of lambda-calculus with conditional rewriting, Building exact computation sequences, Unification in commutative theories, Unification in a combination of arbitrary disjoint equational theories, Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness, De Bruijn's weak diamond property revisited, Automating the Knuth Bendix ordering, Non-commutative Gröbner bases in algebras of solvable type, Termination by completion, Term rewriting: Some experimental results, On word problems in Horn theories, Automating inductionless induction using test sets, The solutions of two star-height problems for regular trees, Finite complete rewriting systems for the Jantzen monoid and the Greendlinger group, Determinism in parallel systems, Proofs by induction in equational theories with constructors, Finite complete rewriting systems and the complexity of word problem, Remarks on an example of Jantzen, Fundamental properties of infinite trees, Some undecidability results for non-monadic Church-Rosser Thue systems, A superposition oriented theorem prover, On graph rewritings, Axiomatisation des tests, Modular tree transducers, Simple second-order languages for which unification is undecidable, Comparison of priority rules in pattern matching and term rewriting, A note on a special one-rule semi-Thue system, Termination orderings for associative-commutative rewriting systems, A finite Thue system with decidable word problem and without equivalent finite canonical system, Properties of substitutions and unifications, Bottom-up tree pushdown automata: Classification and connection with rewrite systems, Abduction in logic programming: A new definition and an abductive procedure based on rewriting, Rewriting modulo isotopies in pivotal linear \((2,2)\)-categories, Eta-conversion for the languages of explicit substitutions, The translation power of top-down tree-to-graph transducers, Some results on the confluence property of combined term rewriting systems, Synthesized and inherited functions. A new computational model for syntax-directed semantics, Coherent confluence modulo relations and double groupoids, Undecidable properties of deterministic top-down tree transducers, A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier), Higher categories, strings, cubes and simplex equations, Label-selective \(\lambda\)-calculus syntax and confluence, Buchberger's algorithm: The term rewriter's point of view, Isoperimetric functions for graph products, Infinite complete group presentations, Combination problems for commutative/monoidal theories or how algebra can help in equational unification, Linear generalized semi-monadic rewrite systems effectively preserve recognizability, Rewriting systems over similarity and generalized pseudometric spaces and their properties, On inductive inference of cyclic structures, An improved general path order, A notation for lambda terms. A generalization of environments, Computing in unpredictable environments: semantics, reduction strategies, and program transformations, A calculational approach to mathematical induction, A confluent calculus for concurrent constraint programming, Developing developments, Twenty years of rewriting logic, A complete proof of correctness of the Knuth-Bendix completion algorithm, NTS grammars and Church-Rosser systems, Testing for the Church-Rosser property, Pebble games for studying storage sharing, Attribute grammars and recursive program schemes. I. II, Graph grammars and operational semantics, Monadic Thue systems, When is a monoid a group? The Church-Rosser case is tractable, A Noetherian and confluent rewrite system for idempotent semigroups, Confluence and convergence modulo equivalence in probabilistically terminating reduction systems, The geometry of tensor calculus. I, Rewrite, rewrite, rewrite, rewrite, rewrite, \dots, Trace monoids with some invertible generators: Two decision problems, A criterion for proving noetherianity of a relation, Combining matching algorithms: The regular case, Sequentiality in orthogonal term rewriting systems, Reduction rules for resolution-based systems, Closure properties of knapsack semilinear groups, Conditional rewriting logic as a unified model of concurrency, Checking overlaps of nominal rewriting rules, An implementation of syntax directed functional programming on nested- stack machines, Causal automata, A new invariant of plane bipartite cubic graphs, Modularity of simple termination of term rewriting systems with shared constructors, Confluent linear numeration systems, Adding algebraic rewriting to the untyped lambda calculus, The Whitney duals of a graded poset, Tree transducers with external functions, Decision problems for semi-Thue systems with a few rules, Cancellation rules and extended word problems, Calcul de longueurs de chaînes de réécriture dans le monoïde libre, Symmetric bimonoidal intermuting categories and \(\omega\times\omega\) reduced bar constructions, Convergent presentations and polygraphic resolutions of associative algebras, A knowledge-based approach to program synthesis from examples, Decidability of elementary theories of certain finitely defined algebras, Confluence up to garbage in graph transformation, Completion for rewriting modulo a congruence, On the Knuth-Bendix completion for concurrent processes, Complete sets of transformations for general E-unification, On deciding confluence of finite string-rewriting systems modulo partial commutativity, Confluence by critical pair analysis revisited, Diagram techniques for confluence, On the descriptive power of term rewriting systems, Relating rewriting techniques on monoids and rings: congruences on monoids and ideals in monoid rings, Semantics and strong sequentiality of priority term rewriting systems, The first-order theory of linear one-step rewriting is undecidable, On the equivalence problem for letter-to-letter top-down tree transducers, Units of special Church-Rosser monoids, On the logic of unification, A strong restriction of the inductive completion procedure, Basic narrowing revisited, Combinatorial \(N_\infty\) operads, On equational theories, unification, and (un)decidability, Unification in permutative equational theories is undecidable, Congruential complements of ground term rewrite systems, About the rewriting systems produced by the Knuth-Bendix completion algorithm, Infinite regular Thue systems, Homotopy reduction systems for monoid presentations, A categorical critical-pair completion algorithm, On finitely presented and free algebras of Cantor varieties, Skew confluence and the lambda calculus with letrec, Partial completion of equational theories, Bisimilarity in term graph rewriting., Equality between functionals in the presence of coproducts, Automatic acquisition of search control knowledge from multiple proof attempts., A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser, Context-sensitive rewriting strategies, An abstract machine for concurrent modular systems: CHARM, On the duality of abduction and model generation in a framework for model generation with equality, Efficient solution of the word problem in slim varieties, Properties of grammatical codes of trees, Rewriting systems of Coxeter groups, Confluence by decreasing diagrams, Confluence and commutation for nominal rewriting systems with atom-variables, Confluence of orthogonal term rewriting systems in the prototype verification system, Termination and confluence in infinitary term rewriting, An axiomatic approach to the Korenjak-Hopcroft algorithms, Term rewriting in CTΣ, Syntactic properties of the refal language, Unnamed Item, A combinatory account of internal structure, CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems, Reducing Relative Termination to Dependency Pair Problems, On how to move mountains ‘associatively and commutatively’, A local termination property for term rewriting systems, Algebraic semantics and complexity of term rewriting systems, Regular Patterns in Second-Order Unification, Efficient ground completion, Consider only general superpositions in completion procedures, Rewriting, and equational unification: the higher-order cases, Unification, weak unification, upper bound, lower bound, and generalization problems, Decidability of confluence and termination of monadic term rewriting systems, Bottom-up tree pushdown automata and rewrite systems, On relationship between term rewriting systems and regular tree languages, Proving equational and inductive theorems by completion and embedding techniques, Open problems in rewriting, Bi-rewriting, a term rewriting technique for monotonic order relations, Distributing equational theorem proving, More problems in rewriting, Problems in rewriting applied to categorical concepts by the example of a computational comonad, Problems in rewriting III, The first-order theory of one-step rewriting is undecidable, Decidable approximations of term rewriting systems, Semantics and strong sequentially of priority term rewriting systems, Unique normal forms for nonlinear term rewriting systems: Root overlaps, Ranking trees generated by rotations, On quasi-interpretations, blind abstractions and implicit complexity, Algebraic coherent confluence and higher globular Kleene algebras, Abelian networks IV. Dynamics of nonhalting networks, String Diagram Rewrite Theory I: Rewriting with Frobenius Structure, A note on thue systems with a single defining relation, Church-Rooser property and homology of monoids, Continuous monoids and yields of infinite trees, Unnamed Item, Gröbner bases of associative algebras and the Hochschild cohomology, The undecidability of the DA-unification problem, On confluence of one-rule trace-rewriting systems, On confluence versus strong confluence for one-rule trace-rewriting systems, Unnecessary inferences in associative-commutative completion procedures, Rewriting in higher dimensional linear categories and application to the affine oriented Brauer category, Normal Higher-Order Termination, Layer Systems for Proving Confluence, Linear numeration systems, θ-developments and finite automata, Applying term rewriting methods to finite groups, Unification properties of commutative theories: A categorical treatment, A confluent relational calculus for higher-order programming with constraints, An introduction to category-based equational logic, Unnamed Item, Confluence Modulo Equivalence in Constraint Handling Rules, Unnamed Item, Unnamed Item, A Characterization of NC k by First Order Functional Programs, EVANS' NORMAL FORM THEOREM REVISITED, Braids via term rewriting, Unification of drags and confluence of drag rewriting, A Completion Method to Decide Reachability in Rewrite Systems, Finite canonical rewriting systems for congruences generated by concurrency relations, Graph expressions and graph rewritings, Word-mappings of level 2, Church-Rosser systems with respect to formal languages, Embedding and Confluence of Graph Transformations with Negative Application Conditions, Decreasing diagrams with two labels are complete for confluence of countable systems, Using groups for investigating rewrite systems, From Analytical Mechanics Problems to Rewriting Theory Through M. Janet’s Work, Noncommutative Gröbner Bases: Applications and Generalizations, Semantics of Concurrent Revisions, Development closed critical pairs, Unnamed Item, Learning domain knowledge to improve theorem proving, Diagrammatic confluence for Constraint Handling Rules, Unnamed Item, Standard Gröbner-Shirshov Bases of Free Algebras Over Rings, I, Decreasing subsequences in permutations and Wilf equivalence for involutions, A polynomial algorithm testing partial confluence of basic semi-Thue systems, Combining matching algorithms: The regular case, Abstract canonical presentations, A semantic approach to order-sorted rewriting, Normal forms for binary relations, Any ground associative-commutative theory has a finite canonical system, Unnamed Item, The Attributed Pi-Calculus with Priorities, Shallow confluence of conditional term rewriting systems, Proving Confluence of Term Rewriting Systems Automatically, Completeness of combinations of constructor systems, Root system chip-firing. I: Interval-firing, Upper Bounds on Stream I/O Using Semantic Interpretations, Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems, Termination Modulo Combinations of Equational Theories, Transformation of Shaped Nested Graphs and Diagrams1 1This work has been partially supported by the ESPRIT Working Group Applications of Graph Transformation (Appligraph)., A note on special thue systems with a single defining relation, Confluence in probabilistic rewriting, Real or natural number interpretation and their effect on complexity, Total unfolding: theory and applications, Labelings for decreasing diagrams
