Abstract
We extend the classical theory of term rewriting systems to infinite and partial terms (i.e., to the elements of algebra CT ∑ ), fully exploiting the complete partially ordered structure of CT ∑ . We show that redexes and rules, as well as other operations on terms, can be regarded as total functions on CT ∑ . As a consequence, we can study their properties of monotonicity and continuity. For rules, we show that nonleft-linear rules are in general not. monotonic, and that left-infinite rules are in general not continuous. Moreover, we show that the well-known Church-Rosser property of non-overlapping redexes holds for monotonic redexes. This property allows us to define a notion of parallel application of a finite set of monotonie redexes, and, using standard algebraic techniques, we extend the definition to the infinite case. We also suggest that infinite parallel term rewriting has interesting potential applications in the semantics of cyclic term, graph rewriting.
Research partially supported by the COMPUGRAPH Basic Research Esprit Working Group n. 7183.
Chapter PDF
References
J.A. Goguen, J.W. Tatcher, E.G. Wagner, J.R. Wright, Initial Algebra Semantics and Continuous Algebras, JACM 24 (1), 1977, pp. 68–95.
A. Arnold, M. Nivat, The metric space of infinite trees. Algebraic and topological properties, Fundamenta Informatica, 4, 1980, pp. 445–476.
H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W, Glauert, J.R. Kennaway, M.J. Plasmeijer, M.R. Sleep, Term graph reduction, in Proc. PARLE, LNCS 259, 1987, pp. 141–158.
A. Corradini, F. Rossi, Hyperedge Replacement Jungle Rewriting for Term Rewriting Systems and Logic Programming, to appear in Theoretical Computer Science.
N. Dershowitz, J.-P. Jouannaud, Rewrite Systems, Handbook of Theoretical Computer Science (ed. J. van Leeuwen), Vol. B, North Holland, 1990, pp. 243–320.
N. Dershowitz, S. Kaplan, Rewrite, Rewrite, Rewrite, Rewrite, Rewrite ..., Principles of Programming Languages, Austin 1989, pp. 250–259.
N. Dershowitz, S. Kaplan, D.A. Plaisted, Infinite Normal Forms (plus corrigendum), ICALP 1989, pp. 249–262.
H. Ehrig, M. Pfender, H.J. Schneider, Graph-grammars: an algebraic approach, Proc, IEEE Conf. on Automata and Switching Theory, 1973, pp. 167–180.
W.M. Farmer, J.D. Ramsdell, R.J. Watro, A correcteness proof for combinator reduction with cycles. Report M88-53, The MITRE Corporation, Massachussets, 1988.
W.M. Farmer, R.J. Watro, Redex capturing in term graph rewriting, in Computing with the Curry Chip, Report M89-59, The MITRE Corporation, Massachussets, 1989.
B. Hoffmann, D. Plump, Implementing Term Rewriting by Jungle Evaluation, in Informatique théorique et Applications/Theoretical Informatics and Applications, 25 (5), 1991, pp. 445–472.
G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, in Journal of the ACM, 27 (4), 1980, pp. 797–821.
J.R. Kennaway, On ‘On Graph Rewritings', Theoretical Computer Science, 52, 1987, pp. 37–58.
J.R, Kennaway, J.W. Klop, M.R. Sleep, F.J. De Vries, Transfinite Reductions in Orthogonal Term Rewriting System, Report CS-R9041, Centre for Mathematics and Computer Science, The Netherland, 1990.
J.W. Klop, Term rewriting systems, to appear in Handbook of Logic in Computer Science (eds. S. Abramsky, D. Gabbay, and T. Maibaum), Vol I, Oxford University Press, 1991.
J.C. Raoult, On Graph Rewritings, Theoretical Computer Science, 32, 1984, pp. 1–24.
B.K. Rosen, Tree maninulating systems and Church-Rosser theorems, JACM 20, 1973, pp. 160–187.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Corradini, A. (1993). Term rewriting in CTΣ . In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_83
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_83
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive