A Characterization of Weakly Church–Rosser Abstract Reduction Systems That Are Not Church–Rosser

Basic properties of rewriting systems can be stated in the framework of abstract reduction systems (ARS). Properties like confluence (or Church–Rosser, CR) and weak confluence (or weak Church–Rosser, WCR) and their relationships can be studied in this setting: as a matter of fact, well-known counterexamples to the implication WCR CR have been formulated as ARS. In this paper, starting from the observation that such counterexamples are structurally similar, we set out a graph-theoretic characterization of WCR ARS that is not CR in terms of a suitable class of reduction graphs, such that in every WCR not CR ARS, we can embed at least one element of this class. Moreover, we give a tighter characterization for a restricted class of ARS enjoying a suitable regularity condition. Finally, as a consequence of our approach, we prove some interesting results about ARS using the mathematical tools developed. In particular, we prove an extension of the Newman's lemma and we find out conditions that, once assumed together with WCR property, ensure the unique normal form property. The Appendix treats two interesting examples, both generated by graph-rewriting rules, with specific combinatorial properties.     

Abstract abstract reduction

We propose novel algebraic proof techniques for rewrite systems. Church–Rosser theorems and further fundamental statements that do not mention termination are proved in Kleene algebra. Certain reduction and transformation theorems for termination that depend on abstract commutation, cooperation or simulation properties are proved in an extension with infinite iteration. Benefits of the algebraic approach are simple concise calculational proofs by equational reasoning, connection with automata-based decision procedures and a natural formal semantics for rewriting diagrams. It is therefore especially suited for mechanization and automation.     

Multiset rewriting over Fibonacci and Tribonacci numbers

We show how techniques from the formal logic, can be applied directly to the problems studied completely independently in the world of combinatorics, the theory of integer partitions. We characterize equinumerous partition ideals in terms of the minimal elements generating the complementary order filters. Here we apply a general rewriting methodology to the case of filters having overlapping minimal elements. In addition to a ‘bijective proof ’ for Zeckendorf-like theorems – that every positive integer is uniquely representable within the Fibonacci, Tribonacci and k-Bonacci numeration systems, we establish ‘bijective proofs’ for a new series of partition identities related to Fibonacci, Tribonacci and k-step Fibonacci numbers. The main result is proved with the help of a multiset rewriting system such that the system itself and the system consisting of its reverse rewriting rules, both have the Church–Rosser property, which provides an explicit bijection between partitions of two different types (represented by the two normal forms).     

Typed operational semantics for higher-order subtyping

Bounded operator abstraction is a language construct relevant to object oriented programming languages and to ML2000, the successor to Standard ML. In this paper, we introduce , a variant of F_<:^ω with this feature and with Cardelli and Wegner’s kernel Fun rule for quantifiers. We define a typed-operational semantics with subtyping and prove that it is equivalent with , using logical relations to prove soundness. The typed-operational semantics provides a powerful and uniform technique to study metatheoretic properties of , such as Church–Rosser, subject reduction, the admissibility of structural rules, and the equivalence with the algorithmic presentation of the system that performs weak-head reductions.Furthermore, we can show decidability of subtyping using the typed-operational semantics and its equivalence with the usual presentation. Hence, this paper demonstrates for the first time that logical relations can be used to show decidability of subtyping.     

Lifting Infinite Normal Form Definitions From Term Rewriting to Term Graph Rewriting

nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.     

Translating Combinatory Reduction Systems into the Rewriting Calculus

The last few years have seen the development of the rewriting calculus (or rho-calculus, ρCal) that extends first order term rewriting and λ-calculus. The integration of these two latter formalisms has been already handled either by enriching first-order rewriting with higher-order capabilities, like in the Combinatory Reduction Systems, or by adding to λ-calculus algebraic features. The different higher-order rewriting systems and the rewriting calculus share similar concepts and have similar applications, and thus, it seems natural to compare these formalisms. We analyze in this paper the relationship between the Rewriting Calculus and the Combinatory Reduction Systems and we present a translation of CRS-terms and rewrite rules into rho-terms and we show that for any CRS-reduction we have a corresponding rho-reduction.     

Complete involutive rewriting systems

Given a monoid string rewriting system M, one way of obtaining a complete rewriting system for M is to use the classical Knuth–Bendix critical pairs completion algorithm. It is well-known that this algorithm is equivalent to computing a noncommutative Gröbner basis for M. This article develops an alternative approach, using noncommutative involutive basis methods to obtain a complete involutive rewriting system for M.     

Autowrite: A Tool for Term Rewrite Systems and Tree Automata

Autowrite is an experimental software tool written in Common Lisp Oriented System (CLOS) which handles term rewrite systems and bottom-up tree automata. A graphical interface written using McCLIM, (the free implementation of the CLIM specification) frees the user of any Lisp knowledge. Software and documentation can be found at http://dept-info.labri.u-bordeaux.fr/~idurand/autowrite. Autowrite was initially designed to check call-by-need properties of term rewrite systems. For this purpose, it implements the tree automata constructions used in [F. Jacquemard. Decidable approximations of term rewriting systems. In Proc. 7th RTA, volume 1103 of LNCS, pages 362–376, 1996; I. Durand and A. Middeldorp. Decidable call by need computations in term rewriting (extended abstract). In Proc. 14th CADE, volume 1249 of LNAI, pages 4–18, 1997; Irène Durand and Aart Middeldorp. On the complexity of deciding call-by-need. Technical Report 1196–98, LaBRI, 1998; T. Nagaya and Y. Toyama. Decidability for left-linear growing term rewriting systems. Information and Computation, 178(2):499–514, 2002] and many useful operations on terms, term rewrite systems and tree automata.     

Deduction, Strategies, and Rewriting

Automated deduction methods should be specified not procedurally, but declaratively, as inference systems which are proved correct regardless of implementation details. Then, different algorithms to implement a given inference system should be specified as strategies to apply the inference rules. The inference rules themselves can be naturally specified as (possibly conditional) rewrite rules. Using a high-performance rewriting language implementation and a strategy language to guide rewriting computations, we can obtain in a modular way implementations of both the inference rules of automated deduction procedures and of algorithms controling their application. This paper presents the design of a strategy language for the Maude rewriting language that supports this modular decomposition: inference systems are specified in system modules, and strategies in strategy modules. We give a set-theoretic semantics for this strategy language, present its different combinators, illustrate its main ideas with several examples, and describe both a reflective prototype in Maude and an ongoing C++ implementation.     

Recursion Engineering for Reduction Incorporated Parsers

Reduction Incorporated (RI) recognisers and parsers deliver high performance by suppressing the stack activity except for those rules that generate fully embedded recursion. Automaton constructions for RI parsing have been presented by Aycock and Horspool [John Aycock and Nigel Horspool. Faster generalised LR parsing. In Compiler Construction, 8th Intnl. Conf, CC'99, volume 1575 of Lecture Notes in Computer Science, pages 32 – 46. Springer-Verlag, 1999] and by Scott and Johnstone [Adrian Johnstone and Elizabeth Scott. Generalised regular parsers. In Gorel Hedin, editor, Compiler Construction, 12th Intnl. Conf, CC'03, volume 2622 of Lecture Notes in Computer Science, pages 232–246. Springer-Verlag, Berlin, 2003] but both can yield very large tables. An unusual aspect of the RI automaton is that the degree of stack activity suppression can be varied in a fine-grained way, and this provides a large family of potential RI automata for real programming languages, some of which have manageable table size but still show high performance. We give examples drawn from ANSI-C, Cobol and Pascal; discuss some heuristics for guiding manual specification of stack activity suppression; and describe work in progress on the automatic construction of RI automata using profiling information gathered from running parsers: in this way we propose to optimise our parsers' table size against performance on actual parsing tasks.