A Generalized Higher-Order Chemical Computation Model

Gamma is a programming model where computation is seen as chemical reactions between data represented as molecules floating in a chemical solution. Formally, this model is represented by the rewriting of a multiset where rewrite rules model the chemical reactions. Recently, we have proposed the γ-calculus, a higher-order extension, where the rewrite rules are first-class citizen. The work presented in this paper increases further the expressivity of the chemical model with generalized multisets: multiplicities of elements may be infinite and/or negative. Applications of these new notions are illustrated by some programming examples.     

Code generation based on formal BURS theory and heuristic search

BURS theory provides a powerful mechanism to efficiently generate pattern matches in a given expression tree. BURS, which stands for bottom-up rewrite system, is based on term rewrite systems, to which costs are added. We formalise the underlying theory, and derive an algorithm that computes all pattern matches. This algorithm terminates if the term rewrite system is finite. We couple this algorithm with the well-known search algorithm A that carries out pattern selection. The search algorithm is directed by a cost heuristic that estimates the minimum cost of code that has yet to be generated. The advantage of using a search algorithm is that we need to compute only those costs that may be part of an optimal rewrite sequence (and not the costs of all possible rewrite sequences as in dynamic programming). A system that implements the algorithms presented in this work has been built. Received: 20 November 1995 / 26 June 1996     

Scoped Dynamic Rewrite Rules

The applicability of term rewriting to program transformation is limited by the lack of control over rule application and by the context-free nature of rewrite rules. The first problem is addressed by languages supporting user-definable rewriting strategies. This paper addresses the second problem by extending rewriting strategies with scoped dynamic rewrite rules. Dynamic rules are generated at run-time and can access variables available from their definition context. Rules generated within a rule scope are automatically retracted at the end of that scope. The technique is illustrated by means of several program tranformations: bound variable renaming, function inlining, and dead function elimination.     

Orienting rewrite rules with the Knuth–Bendix order

We consider two decision problems related to the Knuth–Bendix order (KBO). The first problem is orientability: given a system of rewrite rules R, does there exist an instance of KBO which orients every ground instance of every rewrite rule in R. The second problem is whether a given instance of KBO orients every ground instance of a given rewrite rule. This problem can also be reformulated as the problem of solving a single ordering constraint for the KBO. We prove that both problems can be solved in the time polynomial in the size of the input. The polynomial-time algorithm for orientability builds upon an algorithm for solving systems of homogeneous linear inequalities over integers. We show that the orientability problem is P-complete. The polynomial-time algorithm for solving a single ordering constraint does not need to solve systems of linear inequalities and can be run in time O(n²). Also we show that if a system is orientable using a real-valued instance of KBO, then it is also orientable using an integer-valued instance of KBO. Therefore, all our results hold both for the integer-valued and the real-valued KBO.     

One-sided forbidding grammars and selective substitution grammars

In one-sided forbidding grammars, the set of rules is divided into the set of left forbidding rules and the set of right forbidding rules. A left forbidding rule can rewrite a non-terminal if each of its forbidding symbols is absent to the left of the rewritten symbol in the current sentential form, while a right forbidding rule is applied analogically except that this absence is verified to the right. Apart from this, they work like ordinary forbidding grammars. As its main result, this paper proves that one-sided forbidding grammars are equivalent to selective substitution grammars. This equivalence is established in terms of grammars with and without erasing rules. Furthermore, this paper proves that one-sided forbidding grammars in which the set of left forbidding rules coincides with the set of right forbidding rules characterize the family of context-free languages. In the conclusion, the significance of the achieved results is discussed.     

Generalized one-sided forbidding grammars

In generalized one-sided forbidding grammars (GOFGs), each context-free rule has associated a finite set of forbidding strings, and the set of rules is divided into the sets of left and right forbidding rules. A left forbidding rule can rewrite a nonterminal if each of its forbidding strings is absent to the left of the rewritten symbol. A right forbidding rule is applied analogically. Apart from this, they work like any generalized forbidding grammar. This paper proves the following three results. (1) GOFGs where each forbidding string consists of at most two symbols characterize the family of recursively enumerable languages. (2) GOFGs where the rules in one of the two sets of rules contain only ordinary context-free rules without any forbidding strings characterize the family of context-free languages. (3) GOFGs with the set of left forbidding rules coinciding with the set of right forbidding rules characterize the family of context-free languages.     

Modeling Pointer Redirection as Cyclic Term-graph Rewriting

We tackle the problem of data-structure rewriting including global and local pointer redirections. Each basic rewrite step may perform three kinds of actions: (i) Local redirection, the aim of which is to redirect specific pointers determined by means of a pattern; (ii) Replacement, that may add new information to data-structures; (iii) Global redirection, which is aimed at redirecting all pointers targeting a node towards another one. We define a new framework, following the double-pushout approach, where graph rewrite rules may mix these three kinds of actions in a row. We define first the category of graphs we consider and then we define rewrite rules as pairs of graph homomorphisms of the form L←K→R. In our setting, graph K is not arbitrary, it is used to encode pointer redirection. Furthermore, pushouts do not always exist and complement pushouts, when they exist, are not unique. Despite these concerns, our definition of rewriting steps is such that a rewrite rule can always be fired, once a matching is found.     

Regaining cut admissibility in deduction modulo using abstract completion

Deduction modulo is a way to combine computation and deduction in proofs, by applying the inference rules of a deductive system (e.g. natural deduction or sequent calculus) modulo some congruence that we assume here to be presented by a set of rewrite rules. Using deduction modulo is equivalent to proving in a theory corresponding to the rewrite rules, and leads to proofs that are often shorter and more readable. However, cuts may be not admissible anymore.We define a new system, the unfolding sequent calculus, and prove its equivalence with the sequent calculus modulo, especially w.r.t. cut-free proofs. It permits to show that it is even undecidable to know if cuts can be eliminated in the sequent calculus modulo a given rewrite system.Then, to recover the cut admissibility, we propose a procedure to complete the rewrite system such that the sequent calculus modulo the resulting system admits cuts. This is done by generalizing the Knuth–Bendix completion in a non-trivial way, using the framework of abstract canonical systems.These results enlighten the entanglement between computation and deduction, and the power of abstract completion procedures. They also provide an effective way to obtain systems admitting cuts, therefore extending the applicability of deduction modulo in automated theorem proving.     

Transformations of the one-dimensional cellular automata rule space

We introduce the notion of double permutation in order to study particular classes of transformations of the one-dimensional cellular automata rule space. These classes of transformations are characterized according to different sets of metrical, language theoretic, and dynamical properties they preserve. Each set of transformations we propose induces an equivalence relation over the cellular automata rule space. We give exact results on the cardinality of the quotient sets generated by these equivalence relations. Finally, we discuss some interesting open problems.     

Decidability for Left-Linear Growing Term Rewriting Systems

A term rewriting system is called growing if each variable occurring on both the left-hand side and the right-hand side of a rewrite rule occurs at depth zero or one in the left-hand side. Jacquemard showed that the reachability and the sequentiality of linear (i.e., left-right-linear) growing term rewriting systems are decidable. In this paper we show that Jacquemard's result can be extended to left-linear growing rewriting systems that may have right-nonlinear rewrite rules. This implies that the reachability and the joinability of some class of right-linear term rewriting systems are decidable, which improves the results for right-ground term rewriting systems by Oyamaguchi. Our result extends the class of left-linear term rewriting systems having a decidable call-by-need normalizing strategy. Moreover, we prove that the termination property is decidable for almost orthogonal growing term rewriting systems.     

Detecting redundancy among production rules using term rewrite semantics

We present a general method for detecting wide classes of redundant production rules (PRs) based on the term rewrite semantics. We present the semantic account, define rule execution over both ground memories and memory schemas, and define redundancy for the PRs. From those definitions, an algorithm is developed that detects wide classes of redundant rules, and which improves upon the previously published methods.     

Non-Linear Rewrite Closure and Weak Normalization

A rewrite closure is an extension of a term rewrite system with new rules, usually deduced by transitivity. Rewrite closures have the nice property that all rewrite derivations can be transformed into derivations of a simple form. This property has been useful for proving decidability results in term rewriting. Unfortunately, when the term rewrite system is not linear, the construction of a rewrite closure is quite challenging. In this paper, we construct a rewrite closure for term rewrite systems that satisfy two properties: the right-hand side term in each rewrite rule contains no repeated variable (right-linear) and contains no variable occurring at depth greater than one (right-shallow). The left-hand side term is unrestricted, and in particular, it may be non-linear. As a consequence of the rewrite closure construction, we are able to prove decidability of the weak normalization problem for right-linear right-shallow term rewrite systems. Proving this result also requires tree automata theory. We use the fact that right-shallow right-linear term rewrite systems are regularity preserving. Moreover, their set of normal forms can be represented with a tree automaton with disequality constraints, and emptiness of this kind of automata, as well as its generalization to reduction automata, is decidable. A preliminary version of this work was presented at LICS 2009 (Creus 2009).     

On intuitionistic proof nets with additional rewrite rules and their approximations

First we present a proof nets system with eight additional rewrite rules, which concerns ordering of introductions of exponential-links and are only applied to normal forms of proof nets in the usual sense. We show that the reduction relation generated by these eight rewrite rules is strong normalizing and confluent. Second we propose an simply judged equality on intuitionistic proof nets based on the notion of the main path of an intuitionistic proof net. The notion is an analogue of Böhm-trees in λ-calculus.     

A Rewriting Calculus for Cyclic Higher-order Term Graphs

Introduced at the end of the nineties, the Rewriting Calculus (ρ-calculus, for short) is a simple calculus that fully integrates term-rewriting and λ-calculus. The rewrite rules, acting as elaborated abstractions, their application and the obtained structured results are first class objects of the calculus. The evaluation mechanism, generalizing beta-reduction, strongly relies on term matching in various theories.In this paper we propose an extension of the ρ-calculus, handling graph like structures rather than simple terms. The transformations are performed by explicit application of rewrite rules as first class entities. The possibility of expressing sharing and cycles allows one to represent and compute over regular infinite entities.The calculus over terms is naturally generalized by using unification constraints in addition to the standard ρ-calculus matching constraints. This therefore provides us with the basics for a natural extension of an explicit substitution calculus to term graphs. Several examples illustrating the introduced concepts are given.     

Generalized convex combination of triangular norms on bounded lattices

ABSTRACT

In this paper, we introduce the notions of the linear and generalized convex combination (shortly, g-convex combination) for triangular norms on bounded lattices. We investigate the conditions for the g-convex combination to be a triangular norm again. We introduce a triangular norm defined on a bounded lattice of equivalence classes and investigate some basic properties of the introduced triangular norm.     

Normalization Results for Typeable Rewrite Systems

In this paper we introduce Curryfied term rewriting systems, and a notion of partial type assignment on terms and rewrite rules that uses intersection types with sorts andω. Three operations on types—substitution, expansion, and lifting—are used to define type assignment and are proved to be sound. With this result the system is proved closed for reduction. Using a more liberal approach to recursion, we define a general scheme for recursive definitions and prove that, for all systems that satisfy this scheme, every term typeable without using the type-constantωis strongly normalizable. We also show that, under certain restrictions, all typeable terms have a (weak) head-normal form, and that terms whose type does not containωare normalizable.     

The semantics of the combination of atomized statements and parallel choice

In this paper we define a uniform language that is an extension of the language underlying the process algebraPA. One of the main extensions of this language overPA is given by so-called atomizing brackets. If we place these brackets around a statement then we treat this statement as an atomic action. Put differently, these brackets remove all interleaving points. We present a transition system for the language and derive its operational semantics. We show that there are several options for defining a transition system such that the resulting operational semantics is a conservative extension of the semantics forPA. We define a semantic domain and a denotational model for the language. Next we define a closure operator on the semantic domain and show how to use this closure operator to derive a fully abstract denotational semantics. Then the algebraic theory of the language is considered. We define a collection of axioms and a term rewrite system based on these axioms. Using this term rewrite system we are able to identify normal forms for the language. It is shown that these axioms capture the denotational equality. It follows that if two terms are provably equal then they have the same operational semantics. Finally, we show how to extend the axiomatization in order to axiomatize its operational equivalence.     

Structures for Abstract Rewriting

When rewriting is used to generate convergent and complete rewrite systems in order to answer the validity problem for some theories, all the rewriting theories rely on a same set of notions, properties, and methods. Rewriting techniques have been used mainly to answer the validity problem of equational theories, that is, to compute congruences. Recently, however, they have been extended in order to be applied to other algebraic structures such as preorders and orders. In this paper, we investigate an abstract form of rewriting, by following the paradigm of logical-system independency. To achieve this purpose, we provide a few simple conditions (or axioms) under which rewriting (and then the set of classical properties and methods) can be modeled, understood, studied, proven, and generalized. This enables us to extend rewriting techniques to other algebraic structures than congruences and preorders such as congruences closed under monotonicity and modus ponens. We introduce convergent rewrite systems that enable one to describe deduction procedures for their corresponding theory, and we propose a Knuth-Bendix–style completion procedure in this abstract framework.     

Data Mining for Inventory Item Selection with Cross-Selling Considerations

Association rule mining, studied for over ten years in the literature of data mining, aims to help enterprises with sophisticated decision making, but the resulting rules typically cannot be directly applied and require further processing. In this paper, we propose a method for actionable recommendations from itemset analysis and investigate an application of the concepts of association rules—maximal-profit item selection with cross-selling effect (MPIS). This problem is about choosing a subset of items which can give the maximal profit with the consideration of cross-selling effect. A simple approach to this problem is shown to be NP-hard. A new approach is proposed with consideration of the loss rule—a rule similar to the association rule—to model the cross-selling effect. We show that MPIS can be approximated by a quadratic programming problem. We also propose a greedy approach and a genetic algorithm to deal with this problem. Experiments are conducted, which show that our proposed approaches are highly effective and efficient.