Abstract
Cyclic sharing (cyclic graph rewriting) has been used as a practical technique for implementing recursive computation efficiently. To capture its semantic nature, we introduce categorical models for lambda calculi with cyclic sharing (cyclic lambda graphs), using notions of computation by Moggi/Power and Robinson and traced monoidal categories by Joyal, Street and Verity. The former is used for representing the notion of sharing, whereas the latter for cyclic data structures. Our new models provide a semantic framework for understanding recursion created from cyclic sharing, which includes traditional models for recursion created from fixed points as special cases. Our cyclic lambda calculus serves as a uniform language for this wider range of models of recursive computation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Abramsky, Retracing some paths in process algebra. In Proc. 7th Int. Conf. Concurrency Theory (CONCUR'96), Springer LNCS 1119, pages 1–17, 1996.
Z. Ariola and Arvind, Properties of a first-order functional language with sharing. Theoretical Computer Science 146, pages 69–108, 1995.
Z. Ariola and M. Felleisen, A call-by-need lambda calculus. Technical report CIS-TR-96-97, 1996. To appear in Journal of Functional Programming.
Z. Ariola and J. Klop, Cyclic lambda graph rewriting. In Proc. 9th Symposium on Logic in Computer Sciece (LICS'94), pages 416–425, 1994.
S. L. Bloom and Z. Ésik, Iteration Theories. EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1993.
S. L. Bloom and Z. Ésik, Fixed point operators on ccc's. Part I. Theoretical Computer Science 155, pages 1–38, 1996.
T. Braüner, The Girard translation extended with recursion. In Proc. Computer Science Logic 1994 (CSL'94), Springer LNCS 933, pages 31–45, 1995.
R. L. Crole and A. M. Pitts, New foundations for fixpoint computations: Fix hyperdoctrines and the fix logic. Information and Computation 98, pages 171–210, 1992.
P. Freyd, Algebraically complete categories. In Proc. 1990 Como Category Theory Conference, Springer LNM 1144, pages 95–104, 1991.
P. Gardner and M. Hasegawa, On higher-order action calculi and notions of computation. Draft, LFCS, University of Edinburgh, 1996.
J.-Y. Girard, Geometry of interaction I: interpretation of system F. In Logic Colloquium '88, pages 221–260, North-Holland, 1989.
A. Joyal and R. Street, The geometry of tensor calculus I. Advances in Mathematics 88, pages 55–113, 1991.
A. Joyal and R. Street, Braided tensor categories. Advances in Mathematics 102, pages 20–78, 1993.
A. Joyal, R. Street and D. Verity, Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society 119(3), pages 447–468, 1996.
M. Kelly and M. L. Laplaza, Coherence for compact closed categories. Journal of Pure and Applied Algebra 19, pages 193–213, 1980.
J. Launchbury, A natural semantics for lazy evaluation. In Proc. 21st ACM Symp. Principles of Programming Languages (POPL'93), pages 144–154, 1993.
A. Mifsud, Control structures. PhD thesis, LFCS, University of Edinburgh, 1996.
R. Milner, Higher-order action calculi. In Proc. Computer Science Logic 1992 (CSL'92), Springer LNCS 832, pages 238–260, 1994.
R. Milner, Action calculi V: reflexive molecular forms (with Appendix by O. Jensen). Third draft, July 1994.
R. Milner, Calculi for interaction. Acta Informatica 33(8), pages 707–737, 1996.
E. Moggi, Computational lambda-calculus and monads. Technical report ECS-LFCS-88-66, LFCS, University of Edinburgh, 1988.
E. Moggi, Metalanguages and applications. Draft, 1995.
A. J. Power and E. P. Robinson, Premonoidal categories and notions of computation. 1996. To appear in Mathematical Structures in Computer Science.
N. Yu. Reshetikhin and V. G. Turaev, Ribbon graphs and their invariants derived from quantum groups. Communications in Mathematical Phisics 127, pages 1–26, 1990.
A. Simpson, Recursive types in Kleisli categories. Manuscript, LFCS, University of Edinburgh, 1992.
A. Simpson, A characterisation of the least-fixed-point operator by dinaturality. Theoretical Computer Science 118, pages 301–314, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hasegawa, M. (1997). Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi. In: de Groote, P., Roger Hindley, J. (eds) Typed Lambda Calculi and Applications. TLCA 1997. Lecture Notes in Computer Science, vol 1210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62688-3_37
Download citation
DOI: https://doi.org/10.1007/3-540-62688-3_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62688-6
Online ISBN: 978-3-540-68438-1
eBook Packages: Springer Book Archive