Abstract
Residuals have been studied for various forms of rewriting and residual systems have been defined to capture residuals in an abstract setting. In this article we study residuals in orthogonal Pattern Rewriting Systems (PRSs). First, the rewrite relation is defined by means of a higher-order rewriting logic, and proof terms are defined that witness reductions. Then, we have the formal machinery to define a residual operator for PRSs, and we will prove that an orthogonal PRS together with the residual operator mentioned above, is a residual system. As a side-effect, all results of (abstract)residual theory are inherited by orthogonal PRSs, such as confluence, and the notion of permutation equivalence of reductions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barnaby P. Hilken. Towards a proof theory of rewriting: The simply typed 2λ-calculus. Theoretical Computer Science, 170:407–444, 1996.
Gérard Huet. Residual theory in λ-calculus: A formal development. Journal of Functional Programming, 4(3):371–394, 1994.
Gérard Huet and Jean-Jacques Lévy. Computations in orthogonal rewriting systems, part I + II. In J.L. Lassez and G.D. Plotkin, editors, Computational Logic — Essays in Honor of Alan Robinson. MIT Press, 1991.
Zurab Khasidashvili and John Glauert. Relating conflict-free stable transition systems and event models via redex families. Theoretical Computer Science, 286(1):65–95, 2002.
Cosimo Laneve and Ugo Montanari. Axiomatizing permutation equivalence. Mathematical Structures in Computer Science, 6(3):219–215, 1996.
Jean-Jacques Lévy. Réductions correctes et optimales dans le λ-calcul. Thèse de doctorat d’état, Université Paris VII, 1978.
Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192:3–29, 1998.
Paul-André Melliès. Axiomatic rewriting theory VI: Residual theory revisited. In Sophie Tison, editor, 13th International Conference on Rewriting Techniques and Applications, pages 24–50, 2002.
José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96:73–155, 1992.
Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4), 1991.
Tobias Nipkow and Christian Prehofer. Higher-order rewriting and equational reasoning. In W. Bibel and P. Schmitt, editors, Automated Deduction — A Basis. for Applications, Volume I: Foundations, number 8 in Applied Logic Series, pages 399–430. Kluwer Academic Press, 1998.
Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1994.
Vincent van Oostrom and Roel de Vrijer. Equivalence of Reductions, chapter 8 of [18]. 2003.
Vincent van Oostrom and Roel de Vrijer. Four equivalent equivalences of reductions. In Proceedings of WRS’02 (ENTCS 70.6), 2003. Downloadable at: http://www.elsevier.nl/locate/entcs/.
Femke van Raamsdonk. Confluence and Normalisation for Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1996.
Femke van Raamsdonk. Higher-order rewriting. In 10th International Conference on Rewriting Techniques and Applications, 1999.
Eugene W. Stark. Concurrent transition systems. Theoretical Computer Science, 64(3):221–269, 1989.
Terese. Term Rewriting Systems. Number 55 in Camb. Tracts in Theor. Comp. Sc. Cambridge University Press, 2003.
D. A. Wolfram. The Clausal Theory of Types. Number 21 in Camb. Tracts in Theor. Comp. Sc. Cambridge University Press, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bruggink, H.J.S. (2003). Residuals in Higher-Order Rewriting. In: Nieuwenhuis, R. (eds) Rewriting Techniques and Applications. RTA 2003. Lecture Notes in Computer Science, vol 2706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44881-0_10
Download citation
DOI: https://doi.org/10.1007/3-540-44881-0_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40254-1
Online ISBN: 978-3-540-44881-5
eBook Packages: Springer Book Archive