Abstract
A generalization of tree matching and unification algorithms is presented. Given the equation s=t, this algorithm can often quickly determine that the rewrite rule s→t leads to an infinite sequence of “simplifications”. The rule t→s can be tested in the same way. Rules leading to infinite simplifications should not be included in a rewrite system. In general, the problem of deciding whether a set of rewrite rules leads to infinite simplifications is undecidable. The algorithm that is used for this problem is a cross between a unification algorithm for terms with overlapping variables and a matching algorithm. In the simplest case it attempts to find α, σ M and σ U such that σ M σ U =σ U t/a. In other words, is there a substitution σ U such that in the rule σ U s→σ U t the left side matches a subpart of the right side. The same basic algorithm can be used to test more complex cases of looping involving the interaction of several rules, but it is limited to those cases where each application of a rule occurs inside of the previous rule application. Experiments suggest that the simplest form of the algorithm is about 80 percent effective in eliminating bad orientations of rules. The algorithm never rules out a good orientation of a rule, and so it is most useful when one wants to consider all possible rule orientations.
Chapter PDF
Similar content being viewed by others
References
Dennis De Champeaux, About the Paterson-Wegman Linear Unification Algorithm, Journal of Computer and System Sciences 32 (1986), pp 79–90.
Nachum Dershowitz, Termination, Rewriting Techniques and Applications (Jean-Pierre Jouannaud ed.), Lecture Notes in Computer Science 202, Springer-Verlag New York (1985), pp 180–224.
Nachum Dershowitz, Computing with Rewrite Systems, Information and Control 65 (1985), pp 122–157.
Mikuláš Herman and Igor Prívara, On Nontermination of Knuth-Bendix Algorithm, 13-th Colloq. Automata, Languages and Programming, Lectures Notes in Computer Science, Springer-Verlag, New York (1986), pp 146–156.
G. Higman and B. H. Neumann, Groups as Groupoids with One Law, Publ. Math. Debrecen 2 (1952), pp 215–227.
Gérard Huet, A Complete Proof of the Correctness of the Knuth-Bendix Completion Algorithm, J. Computer and Systems Sciences 23 (1981), pp 11–21.
G. Huet and D. S. Landford, On the Uniform Halting Problem for Term Rewriting Systems, Rapport Laboria 283, IRIA (1978).
J. P. Jouannaud and H. Kirchner, Construction d'un plus petit order de simplification, Report 82-R-033, Centre de Recherche en Informatique de Nancy, Nancy, France (1982).
Claude Kirchner, Computing Unification Algorithms, Symposium on Logic in Computer Science, IEEE Computer Society (1986), pp 208–216.
Donald E. Knuth and Peter B. Bendix, Simple World Problems in Universal Algebras, Computational Problems in Abstract Algebra (J. Leech ed.) Pergamon Press, Oxford (1970), pp 263–297.
Yves Metivier, About the Rewriting Systems Produced by the Knuth-Bendix Completion Algorithm, Information Processing Letters 16 (1983), pp 31–34.
M. S. Paterson and M. N. Wegman, Linear Unification, Journal of Computer and System Sciences, 16 (1978), pp 158–167.
David A. Plaisted, A Simple Non-Termination Test for the Knuth-Bendix Method, 8-th International Conference on Automated Deduction, Lecture Notes in Computer Science 230, Springer-Verlag, New York (1986), pp 79–88.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Purdom, P.W. (1987). Detecting looping simplifications. In: Lescanne, P. (eds) Rewriting Techniques and Applications. RTA 1987. Lecture Notes in Computer Science, vol 256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-17220-3_5
Download citation
DOI: https://doi.org/10.1007/3-540-17220-3_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-17220-8
Online ISBN: 978-3-540-47421-0
eBook Packages: Springer Book Archive