 |
Discrete Mathematics & Theoretical Computer Science |
Vol. 2
1. SOUR graphs for efficient completion
We introduce a data structure called \emphSOUR graphs and present an efficient Knuth-Bendix completion procedure based on it. \emphSOUR graphs allow for a maximal structure sharing of terms in rewriting systems. The term representation is a dag representation, except that edges are labelled with equational constraints and variable renamings. The rewrite rules correspond to rewrite edges, the unification problems to unification edges. The Critical Pair and Simplification inferences are recognized as patterns in the graph and are performed as local graph transformations. Our algorithm avoids duplicating term structure while performing inferences, which causes exponential behavior in the standard procedure. This approach gives a basis to design other completion algorithms, such as goal-oriented completion, concurrent completion and group completion procedures.
2. Right-cancellability of a family of operations on binary trees
We prove some new results on a family of operations on binary trees, some of which are similar to addition, multiplication and exponentiation for natural numbers. The main result is that each operation in the family is right-cancellable.
3. Lower bounds for sparse matrix vector multiplication on hypercubic networks
In this paper we consider the problem of computing on a local memory machine the product y = Ax,where A is a random n×n sparse matrix with Θ (n) nonzero elements. To study the average case communication cost of this problem, we introduce four different probability measures on the set of sparse matrices. We prove that on most local memory machines with p processors, this computation requires Ω ((n/p) \log p) time on the average. We prove that the same lower bound also holds, in the worst case, for matrices with only 2n or 3n nonzero elements.
4. Object grammars and random generation
This paper presents a new systematic approach for the uniform random generation of combinatorial objects. The method is based on the notion of object grammars which give recursive descriptions of objects and generalize context-freegrammars. The application of particular valuations to these grammars leads to enumeration and random generation of objects according to non algebraic parameters.