Tree-Manipulating Systems and Church-Rosser Theorems

DOI10.1145/321738.321750zbMath0267.68013OpenAlexW2056239109MaRDI QIDQ5684229

Publication date: 1973

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

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

Mathematics Subject Classification ID

Trees (05C05) Formal languages and automata (68Q45) Recursive functions and relations, subrecursive hierarchies (03D20) General topics in the theory of software (68N01) General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science (68-00)

Related Items

Efficient ground completion, Confluence and superdevelopments, The combinator M and the Mockingbird lattice, Extending graph rewriting with copying, Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting, Local confluence of conditional and generalized term rewriting systems, Unnamed Item, Ein algebraischer Beweis für das Church-Rosser-Theorem, Unnamed Item, The Church-Rosser property in symmetric combinatory logic, 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, From Rules to Constraint Programs with the Rules2CP Modelling Language, Unnamed Item, Transfinite reductions in orthogonal term rewriting systems, Chain properties of rule closures, Confluence without termination via parallel critical pairs, Algorithmic decidability of the Church-Rosser property in algebras of nondeterminate algorithms with closed logical conditions, Confluence of orthogonal term rewriting systems in the prototype verification system, An axiomatic approach to the Korenjak-Hopcroft algorithms, Reductions in tree replacement systems, Some results on the confluence property of combined term rewriting systems, Term rewriting in CTΣ, Syntactic properties of the refal language, Unnamed Item, A combinatory account of internal structure, Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent, Algebraic solutions to recursion schemes, Termination of rewriting, The Church-Rosser property for ground term-rewriting systems is decidable, History and basic features of the critical-pair/completion procedure, On the tree-transformation power of XSLT, Attacking a public key cryptosystem based on tree replacement, A note on thue systems with a single defining relation, On explicit substitution with names, Confluence of indirection reductions in graph rewrite systems, Unnamed Item, Decidable sentences of Church-Rosser congruences, Implementation of Deadlock Analysis in Data Flow Graphs, Deterministic tree pushdown automata and monadic tree rewriting systems, Integration of parametric and ``ad hoc second order polymorphism in a calculus with subtyping, Polymorphic extensions of simple type structures. With an application to a bar recursive minimization, Unnamed Item, Final algebra semantics and data type extensions, Layer Systems for Proving Confluence, From diagrammatic confluence to modularity, Optimal evaluations of graph-like expressions, Developing developments, A representation of trees by languages. II, Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent, Speeding up subtree replacement systems, An abstract Church-Rosser theorem. II: Applications, Persistence of vector replacement systems is decidable, An algebraic definition for control structures, Finite canonical rewriting systems for congruences generated by concurrency relations, A modified tree-to-tree correction problem, Decreasing diagrams and relative termination, Unnamed Item, DPDA's in 'Atomic normal form' and applications to equivalence problems, Testing for the Church-Rosser property, Chain properties of rule closures, Recognizable formal power series on trees, Graph grammars and operational semantics, Monadic Thue systems, When is a monoid a group? The Church-Rosser case is tractable, Church-Rosser systems with respect to formal languages, Mixed computation: potential applications and problems for study, Decreasing diagrams with two labels are complete for confluence of countable systems, On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems, Checking overlaps of nominal rewriting rules, Unnamed Item, Unnamed Item, Confluence of the lambda calculus with left-linear algebraic rewriting, Deriving graphs from graphs by applying a production, Optimal reduction in replacement systems, Infinite trees in normal form and recursive equations having a unique solution, Unnamed Item, Program equivalence and context-free grammars, Lambda-calculus with director strings, Least fixed points revisited, Aλδ-calculus with an algorithmicδ, A theory of reversibility for Erlang, Correctness of parallel programs: The Church-Rosser approach, On reduction of asynchronous systems, IO and OI. I, Synchronization and computing capabilities of linear asynchronous structures, A class of replacement systems with simple optimality theory, IO and OI. II, A representation of trees by languages. I, Addressable approximations to nonaddressable data graphs, (A-)synchronous (non)-deterministic cell spaces simulating each other, Recursive converters on a memory, Shallow confluence of conditional term rewriting systems, Functional systems: Theoretical and practical aspects, Church-Rosser strategies in the lambda calculus, Church-Rosser converters, Confluence by critical pair analysis revisited, Proving Confluence of Term Rewriting Systems Automatically, The Church-Rosser property in dual combinatory logic, Diagram techniques for confluence, Non-Looping String Rewriting, Measurements and Confluence in Quantum Lambda Calculi With Explicit Qubits, Algebraic and operational semantics of specifications allowing exceptions and errors, Semantics and strong sequentiality of priority term rewriting systems, Approximation properties of abstract data types, A note on special thue systems with a single defining relation, Interaction nets for linear logic, Fundamental properties of infinite trees, On the correspondence between two classes of reduction systems, Dependent types with subtyping and late-bound overloading, Axiomatisation des tests, Real or natural number interpretation and their effect on complexity, Functionality problem in a class of relation schemas, Labelings for decreasing diagrams, Confluence by decreasing diagrams, The Equivalence of Complete Reductions, Confluence and commutation for nominal rewriting systems with atom-variables