Proc. Intl. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science (Mar. 1998) [with R. Treinen].
We provide a brief update on problems about which we know of significant progress.
Proc. 6th Intl. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science 914, 457-471 (Apr. 1995) [with J.-P. Jouannaud, J. W. Klop].
We give references to solutions and partial solutions of old problems, plus a few reformulations, and some new problems.
Proc. 5th Intl. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science 690, 468-487 (June 1993) [with J.-P. Jouannaud, J. W. Klop].
We report on progress made and list some new problems. We also mention a couple of long-standing open problems which have recently been answered. The last section contains a partisan list of interesting areas for future research.
Repaired version of Functional Programming, Concurrency, Simulation and Automated Reasoning, Lecture Notes in Computer Science 693, 199-228 (1993)
This survey of the theory and applications of rewriting with equations discusses the existence and uniqueness of normal forms, the Knuth-Bendix completion procedure and its variations, as well as rewriting-based (functional and logic) programming and (equational, first-order, and inductive) theorem proving. Ordinary, associative-commutative, and conditional rewriting are covered. Current areas of research are summarized and an extensive bibliography is provided.
Proc. 4th Intl. Conf. on Rewriting Techniques and Applications (Apr. 1991), Lecture Notes in Computer Science 488, 445-456 [with J.-P. Jouannaud, J. W. Klop].
To encourage and stimulate continued progress in this area, we have collected (with the help of colleagues) a number of problems that appear to us to be of interest and regarding which we do not know the answer. Questions on rewriting and other equational paradigms have been included; many have not aged sufficiently to be accorded the appellation ``open problem''. We have limited ourselves to theoretical questions, though there are certainly many additional interesting questions relating to applications and implementations.
Bull. of the European Association of Theoretical Computer Science 43 (Feb. 1991) 162-172 [with J.-P. Jouannaud].
Imprecise on-line version of chapter 6 of Handbook of Theoretical Computer Science B: Formal Methods and Semantics, J. van Leeuwen, ed., North-Holland, Amsterdam (1990) 243-320 [with J.-P. Jouannaud].
MFCS (1997).
It is important for programs to have modular correctness properties. We look at non-deterministic programs expressed as term-rewriting systems (which compute normal forms of input terms) and consider the case where individual systems share constructors, but not defined symbols. We present some old and new sufficient conditions under which termination (existence of normal forms, regardless of computation strategy) and confluence (uniqueness) are preserved by such combinations.
Rewriting Techniques and Applications (1997)
We investigate conditions under which confluence and/or termination are preserved for constructor-sharing and hierarchical combinations of rewrite systems, one of which is left-linear and convergent.
Proceedings of Fourth International Workshop on Conditional (and Typed) Rewriting Systems, Lecture Notes in Computer Science 968 (1995) 89-105
From a practical perspective, it is important for programs to have modular correctness properties. Some (largely syntactic) sufficient conditions are given here for the union of terminating rewrite systems to be terminating, particularly in the hierarchical case, when one of the systems makes no reference to functions defined by the other.
Draft of Theoretical Computer Science 142(2) 179-207 (May 1995) [with C. Hoot].
Simple rewrite systems are those for which a simplification ordering is sufficient for showing termination. Two techniques for showing termination of non-simple systems are examined. The first approach generalizes the various path orderings and the conditions under which they work. Examples of its use are given and a brief description of an implementation is presented. The second approach uses restricted derivations, called ``forward closures'' for proving termination of orthogonal and overlaying systems. Both approaches allow the use of ``natural'' interpretations under which rules rewrite terms to terms of the same value.
Proc. Spring School, Lecture Notes in Computer Science 909 (1995)
A graded sequence of examples--presented in a uniform framework--spotlights stages in the development of methods for proving termination of rewrite systems.
Ph.D. thesis (1996), Univ. of Illinois [by C. Hoot]
Theoretical Computer Science 83(1) 71-96 (1991) [with S. Kaplan, D. Plaisted].
We study properties of rewrite systems that are not necessarily terminating, but allow instead for transfinite derivations that have a limit. In particular, we give conditions for the existence of a limit and for its uniqueness and relate the operational and algebraic semantics of infinitary theories. We also consider sufficient completeness of hierarchical systems.
Report version of J. of the ACM 41 (2) 236-276 (Feb. 1994) [with L. Bachmair].
We describe the application of proof orderings--a technique for reasoning about inference systems--to various rewrite-based theorem-proving methods, including refinements of the standard Knuth-Bendix completion procedure based on critical pair criteria; Huet's procedure for rewriting modulo a congruence; ordered completion (a refutationally complete extension of standard completion); and a proof by consistency procedure for proving inductive theorems.
Proc. 3d Intl. Work. on Conditional Rewriting Systems, Lecture Notes in Computer Science 656 (Jan. 1993) 307-314
In: Words, Languages & Combinatorics, M. Ito, ed. World Scientific, Singapore (1992) 104-118
This paper presents various recent approaches to solving word problems. Term orderings are used to define a terminating rewrite relation. When confluent, that relation defines unique normal forms that can be used to decide word problems.
Proc. 12th Intl. Joint Conf. on Artificial Intelligence (Aug. 1991) 118-124
Two new theorem-proving procedures for equational Horn clauses are presented. The largest literal is selected for paramodulation in both strategies, except that one method treats positive literals as larger than negative ones and results in a unit strategy. Both use term orderings to restrict paramodulation to potentially maximal sides of equations and to increase the amount of allowable simplification (demodulation). Completeness is shown using proof orderings.
Proc. 18th Intl. Colloq. on Automata, Languages and Programming, Lecture Notes in Computer Science 510 (July 1991) 267-278
Draft of Chap. 1 in Resolution of Equations in Algebraic Structures 2: Rewriting Techniques, H. Ait-Kaci and M. Nivat, eds. pp. 1-30, Academic Press, New York (1989) [with L. Bachmair and D. A. Plaisted].
We present an ``unfailing'' extension of the standard Knuth-Bendix completion procedure that is guaranteed to produce a desired canonical system, provided certain conditions are met. We prove that this unfailing completion method is refutationally complete for theorem proving in equational theories. The method can also be applied to Horn clauses with equality, in which case it corresponds to positive unit resolution plus oriented paramodulation, with unrestricted simplification.
Function Inversion
(PDF)
To appear [with S. Mitra].
An algorithm is given for inverting functions defined by left-linear ground convergent rewrite systems, with left sides restricted in depth and right sides not having defined symbols at the top.
Draft [with S. Mitra].
`Semantic matching' is the process of generating a basis set of substitutions (of terms for variables) that makes one term equal to another in a specified theory. We restrict ourselves here to matching problems in equational theories that can be presented as programs in the form of convergent rewrite systems, that is, finite sets of equations that compute unique output values when applied (from left-to-right) to input values (a generalization of functional programs).
Decidable matching can help in program verification and synthesis. We describe a new class of programs for which matching is decidable, which--with some negative results--provide a finer characterization of decidability than was available before.
Ph.D. thesis (Aug. 1994), Univ. of Illinois [by S. Mitra]
IBM Technical Report TR ADTI-1996-001 (Jan. 1996) [with S. Mitra]
``Semantic unification'' is the process of generating a basis set of substitutions (of terms for variables) that makes two given terms equal in a specified theory. Semantic unification is an important component of some theorem provers. ``Semantic matching,'' a simpler variant of unification, where the substitution is made in only one of the terms, has potential usage in programming language interpreters.
Decidable matching is required for pattern application in pattern-directed languages, while decidable unification is useful for theorem proving modulo an equational theory.
In this paper we restrict ourselves to matching and unification problems in theories that can be presented as convergent rewrite systems, that is, finite sets of equations that compute unique output values when applied (from left-to-right) to input values. The new results presented here, together with existing results, provide a much finer characterization of decidable matching and unification than was available before.
Proc. 11th Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence 607 (1992) 589-602 [with S. Mitra and G. Sivakumar].
We describe decision procedures for certain classes of semantic matching problems, where the equational theory with respect to which the semantic matching is performed has a convergent rewrite system. We give counterexamples to show that semantic matching becomes undecidable (as it generally is) when the conditions we give are weakened.
Goal Solving as Operational Semantics
(PDF)
Proc. Intl. Logic Programming Symposium (Dec. 1995)
To combine a functional or equational programming style with logic programming, one can use an underlying logic of Horn clauses with equality (as an interpreted predicate symbol) and (typed) terms. From this point of view, the most satisfying operational semantics would search for solutions to equations or predicates. ``Narrowing'' and many of its variants are complete mechanisms for generating solutions. Such a melded language is more expressive than either paradigm alone: functional dependencies are explicit; ``multi-valued'' functions can be better expressed as predicates; nested functions can be evaluated without recourse to search (backtracking); (nonconstructor) terms can serve as arguments to predicates; functions can be inverted; nonterminating functions can be programmed in a terminating fashion; goals can be simplified in a ``don't care'' manner; ``functional'' negation can prune searches. Moreover, the availability of backtracking and existential (``logic'') variables provides an alternative to infinite data structures (``streams'').
Proc. 6th International Conference on Logic Programming (Lisbon, Portugal), MIT Press, Cambridge, MA, pp. 369-381 (June 1989) [with N. Lindenstrauss].
Abstract And-Parallel Machines (Short version)
(PDF)
Proceedings of Europar '97 [with N. Lindenstrauss].
The deterministic Turing machine, though abstract, can still be seen as a model of a realistic computer. The same cannot be said for the nondeterministic Turing machine as a model of parallel computing. We introduce several abstract machines with fine-grained parallelism---the and-parallel Turing machine, the stronger parallel rewriting machine, and extensions of both with an interrupt capability. These machines are very powerful: the parallel rewriting machine can compute the permanent in polynomial time and the and-parallel machine with interrupt can simulate nondeterministic and alternating Turing machines of polynomial time complexity in polynomial time. All the same, they may be viewed as realistic models if time and space are suitably restricted.
Abstract And-Parallel Machines
Submitted [with N. Lindenstrauss].
Several abstract models of fine-grained parallelism are introduced. The first and-parallel machine can be viewed as a generalization of the deterministic Turing machine in which the infinite tape is replaced by an infinite tree-like tape on which processors work in parallel. In this model one can express communication between processors, suspension, and synchronization. There are examples in which the processing time is polylogarithmic in the size of the input (while for a nondeterministic Turing machine that looks at its input the time must be at least of the order of magnitude of the size of the input). This model is, however, too weak for tasks such as merging and sorting in polylogarithmic time, so we introduce a stronger model, the parallel rewriting machine, in which this speed can be achieved. This second model is also easier to program since its basic transitions are based on rewrite rules. Moreover, since this machine gets the program in a form that preserves its meaning, problems of synchronization are easily handled. In both models a processor can launch other processors on subcomputations, but processing at a parent node must wait for answers from all of its ``children''. One can introduce more powerful models which contain the possibility of an interrupt--if the answer from one child (or several children) is sufficient to continue the computation at the parent, the computation started by the other children can and should be interrupted. It is shown that this interrupt machine is much more powerful than the previous two, although it does not seem to be much more difficult to implement them. Although the machines are very powerful, they can be seen as models of realistic machines if we restrict ourselves to polylogarithmic time.
Proc. Second Conference on Algebraic and Logic Programming (Nancy, France), Lecture Notes in Computer Science 463, 318-331 (Oct. 1990) [with N. Lindenstrauss].
Term rewriting corresponds to reduction in applicative languages; narrowing of terms corresponds to goal reduction in logic languages. An abstract machine is described for rewriting and narrowing. It has been implemented in Flat Concurrent Prolog, but could be coded in any system in which processes are capable of creating other processes and communicating with each other.
Proc. 5th Jerusalem Conference on Information Technology (Jerusalem, Israel), IEEE Computer Society, pp. 426-435 (Oct. 1990) [with N. Lindenstrauss].
Submitted [with D. N. Jayasimha].
Bounded fairness, a stronger notion than the usual fairness based on eventuality, can be used, for example, to relate the frequency of shared resource access of a particular process with regard to other processes that access the resource with mutual exclusion. We formalize bounded fairness by introducing a new binary operator into temporal logic. One main difference between this logic and explicit-time logics, one which we consider to be an advantage in many cases, is that time does not appear explicitly as a parameter.
The syntax and semantics for this new logic, kTL, are given. This logic is shown to be more powerful than temporal logic with the eventuality operator and as powerful as the logic with the until operator. We argue that kTL can be used to specify bounded fairness requirements in a more natural manner than is possible with until; in particular, we show properties that can be expressed more succinctly in kTL. We also give a procedure for testing satisfiability of kTL formulas.
As applications of bounded fairness, we specify requirements for some standard concurrent programming problems, and show, for example, that Dekker's mutual exclusion algorithm is fair in the conventional sense, but not bounded fair. We also give examples of bounded fair algorithms.
J. Symbolic Computation 15, 467-494 (1993) [with U. Reddy].
An equational approach to the synthesis of functional and logic program is taken. Typically, the synthesis task involves finding equations which make the given specification an inductive theorem. To synthesize such programs, induction is necessary. We formulate efficient procedures for inductive proof as well as program synthesis using the framework of ordered rewriting. We also propose heuristics for generalizing from a sequence of equational consequences. These heuristics handle cases where the deductive process alone is not adequate to come with a program.
Proc. 8th Natl. Conf. on A.I., Boston (July 1990) pp. 234-239 [with E. Pinchover].
J. Symbolic Computation 15, 745-773 (1993) [with Y-j. Lee].
We show how executable specifications may be used to generate test cases for bug discovery, locate bugs when test data cause a program to fail, and guide deductive and inductive bug correction.
Proc. Symp. on Logical Foundations of Computer Science, Lecture Notes in Computer Science 620 117-126 (July 1992). Under revision [with E. Reingold].
We provide a set of ``natural'' requirements for well-orderings of (binary) list structures. We show that the resultant order-type is the successor of the first critical epsilon number.
Proc. 4th Intl. Joint Conf. on Theory and Practice of Software Development, Lecture Notes in Computer Science 668 (Apr. 1993) 243-250
Trees are a natural representation for countable ordinals. In particular, finite trees provide a convenient notation for the predicative ones. Processes that transform trees or terms can often be proved terminating by viewing the tree or the tree representation of the term as an ordinal.
M.Sc. thesis, Univ. of Illinois [by M. Harris].
[with Sh. Zaks].
Proc. 3d Intl. Conf. on Foundations of Data Organization and Algorithms, Lecture Notes in Computer Science 367, 102-113 [with H.-W. Leong].
We present three variations of the following new sorting theme: Throughout the sort, the array is maintained in piles of sorted elements. At each step, the piles are split into two parts, so that the elements of the left piles are smaller than (or equal to) the elements of the right piles. Then, the two parts are each sorted, recursively. The theme, then, is a combination of Hoare's Quicksort idea, and the Pick algorithm, by Blum, et al., for linear selection. The variations arise from the possible choices of splitting method.
Proceedings of the Latin American Jewish Studies Association, [with S. C. Halevy].