Abstract
λ-definability of term rewriting systems has been an open question. Berarducci and Böhm show that canonical systems are translated into the λ-calculus. However, they do not present a theory which can formalize their translation. In this paper, we adapt Böhm's separability theory for λ-definability. A term rewriting system version of separability, called separable systems, is proposed. Separable systems may includes multiple constructors in the left-hand sides, and canonical systems are a subclass of separable systems. An encoding technique of translating separable systems into the λ-calculus is presented.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Z. Ariola, J.R. Kennaway, J.W. Klop, M.R. Sleep, and F.J. de Vries. Syntactic definitions of undefined: On defining the undefined. In Theoretical Aspect of Computer Software, Lecture Notes in Computer Science 789, pages 543–544. Springer-Verlag, 1994.
H.P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North-Holland, second edition, 1984.
A. Berarducci and C. Böhm. A self-interpreter of lambda calculus having a normal form. In CSL-92, Lecture Notes in Computer Science 702, pages 85–99. Springer-Verlag, 1992.
G. Berry. Stable models of typed λ-calculi. In G. Ausiello and C. Böhm, editors, Automata and Languages and Programming, Lecture Notes in Computer Science 62, pages 72–89. Springer-Verlag, 1978.
S. Byun, J.R. Kennaway, and M.R. Sleep. Transformation of orthogonal term rewriting systems. In K. Kanchanasut and J.-J. Lévy, editors, ACSC '95: Algorithms, Concurrency and Knowledge, Lecture Notes in Computer Science 1023, pages 73–87. Springer-Verlag, 1995.
C. Böhm. Alcune proprietà delle forme β-η-normali nel λ-k-calcolo. IAC Pubbl., 696:19, 1968.
M. Coppo, M. Dezani-Ciancaglini, and S. Rocca. (Semi-) separability of finite sets of terms in Scott's D ∞ models of the λ-calculus. In ICALP '78, Lecture Notes in Computer Science 62, pages 142–164. Springer-Verlag, 1978.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Method and Semantics, chapter 15. North-Holland, 1990.
N. Dershowitz, J.-P. Jouannaud, and J.W. Klop. Open problems in rewriting — no. 1. In R. Book, editor, 4th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 488, pages 445–456. Springer-Verlag, 1991.
G. Huet and J.-J. Lévy. Computations in orthogonal rewrite systems I and II. In J.-L. Lassez and G.D. Plotkin, editors, Computational Logic: Essay in Honor of Alan Robinson, pages 394–443. MIT Press, 1991.
J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume II, pages 1–116. Oxford University Press, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Byun, S., Kennaway, R., Sleep, R. (1996). Lambda-definable term rewriting systems. In: Jaffar, J., Yap, R.H.C. (eds) Concurrency and Parallelism, Programming, Networking, and Security. ASIAN 1996. Lecture Notes in Computer Science, vol 1179. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027784
Download citation
DOI: https://doi.org/10.1007/BFb0027784
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62031-0
Online ISBN: 978-3-540-49626-7
eBook Packages: Springer Book Archive