Abstract
The present paper studies the semantics of linear and non-overlapping TRSs. To treat possibly non-terminating reduction, the limit of such a reduction is formalized using Scott's order-theoretic approach. An interpretation of the function symbols of a TRS as a continuous algebra, namely, continuous functions on a cpo, is given, and universality properties of this interpretation are discussed. Also a measure for computational complexity of possibly non-terminating reduction is proposed. The space of complexity forms a cpo and function symbols can be interpreted as monotone functions on it.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
ADJ, ”Initial Algebra Semantics and Continuous Algebras,” J.ACM 24, pp. 68–95 (1977).
J. Avenhaus, ”On the Descriptive Power of Term Rewriting Systems,” J. of Symbolic Computation 2, pp. 109–122 (1986).
G. Boudol, ”Computational Semantics of Term Rewriting Systems,” [16, pp. 167–236].
B. Courcelle, ”Infinite Trees in Normal Form and Recursive Equations Having a Unique Solution,” Math. Systems Theory 13, pp. 131–180 (1979).
B. Courcelle, ”Fundamental Properties of Infinite Trees,” Theor. Comput. Sci. 25, pp. 95–169(1983).
I. Guessarian, ”Algebraic Semantics,” LNCS 99, Springer-Verlag (1978).
I. Guessarian, ”Survey on Classes of Interpretations and Some of Their Applications,” [16, pp. 383–410].
G. Huet, ”Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,” J. ACM 27, pp. 797–821 (1980).
G. Huet and J.-J. Lévy, ”Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems,” Raport Laboria 359, IRIA (1979).
M.R. Levy and T.S.E. Maibaum, ”Continuous data types,” SIAM J. Comput. 11, pp. 201–216(1982).
J.-J. Lévy, ”An Algebraic Interpretation of the λβK-calculus and a Labeled λ-calculus,” Theor. Comp. Sci. 2, pp. 97–114(1976).
T. Naoi and Y. Inagaki, ”The Conservative Extension and Behavioral Semantics of Term Rewriting Systems,” Technical Research Report No.8604, Department of Information Science, Nagoya University(1986).
T. Naoi and Y. Inagaki, ”The Relation between Algebraic and Fixedpoint Semantics of Term Rewriting Systems,” Technical Report COMP86-37, IEICE (1986).
T. Naoi and Y. Inagaki, ”Time-Cost of Infinite Computation in Term Rewriting Systems”, Technical Report COMP88-34, IEICE (1988).
M. Nivat, ”On the Interpretation of Recursive Polyadic Program Schemes,” Symposia Mathematics 15, Rome, pp. 255–281(1975).
M. Nivat and J.C. Reynolds, Eds., ”Algebraic Methods in Semantics,” Cambridge University Press (1985).
M. J. O'Donnell, ”Computing in Systems Described by Equations,” LNCS 58, Springer-Verlag (1977).
J.-C. Raoult and J. Vuillemin, ”Operational and Semantic Equivalence Between Recursive Programs,” J.ACM 27, pp.772–796(1980).
D. Scott, ”Data Types as Lattices,” SIAM J. Comput 5, pp. 522–587(1976).
D. Scott, ”Domains for Denotational Semantics,” in: ”ICALP 82,” M. Nielson and E.M. Schmidt, Eds., LNCS 140, pp. 577–613, Springer-Verlag (1982).
C.P. Wadsworth, ”The Relation between Computational and Denotational Properties for Scott's D ∞-Models of the Lambda-Calculus,” SIAM J. Comput. 5, pp. 488–521(1976).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Naoi, T., Inagaki, Y. (1989). Algebraic semantics and complexity of term rewriting systems. In: Dershowitz, N. (eds) Rewriting Techniques and Applications. RTA 1989. Lecture Notes in Computer Science, vol 355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51081-8_116
Download citation
DOI: https://doi.org/10.1007/3-540-51081-8_116
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51081-9
Online ISBN: 978-3-540-46149-4
eBook Packages: Springer Book Archive