Document Open Access Logo

Finitary Corecursion for the Infinitary Lambda Calculus

Authors Stefan Milius, Thorsten Wißmann

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2015.336.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Stefan Milius
Thorsten Wißmann

Cite AsGet BibTex

Stefan Milius and Thorsten Wißmann. Finitary Corecursion for the Infinitary Lambda Calculus. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 336-351, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CALCO.2015.336

Abstract

Kurz et al. have recently shown that infinite lambda-trees with finitely many free variables modulo alpha-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational lambda-trees, i.e. those lambda-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational lambda-trees.
Keywords
  • rational trees
  • infinitary lambda calculus
  • coinduction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jiř\'ıAdámek. Introduction to coalgebra. Theory Appl. Categ., 14:157-199, 2005. Google Scholar
  2. Jiř\'ıAdámek, Stefan Milius, and Jiri Velebil. Iterative algebras at work. Math. Structures Comput. Sci, 16(6):1085-1131, 2006. Google Scholar
  3. Jiř\'ıAdámek, Stefan Milius, and Jiri Velebil. Semantics of higher-order recursion schemes. Log. Methods Comput. Sci., 7(1), 2011. Google Scholar
  4. Jiř\'ıAdámek and Jiř\'ıRosický. Locally presentable and accessible categories. Cambridge University Press, 1994. Google Scholar
  5. André Arnold and Maurice Nivat. The metric space of infinite trees. algebraic and topological properties. Fundam. Inform., 3(4):445-476, 1980. Google Scholar
  6. Hendrik Pieter Barendregt. The Lambda calculus: Its syntax and semantics. North-Holland, Amsterdam, 1984. Google Scholar
  7. Marcello M. Bonsangue, Stefan Milius, and Jurriaan Rot. On the specification of operations on the rational behaviour of systems. In Proc. EXPRESS/SOS'12, volume 89 of Electron. Proc. Theoret. Comput. Sci., pages 3-18, 2012. Google Scholar
  8. Marcello M. Bonsangue, Stefan Milius, and Alexandra Silva. Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log., 14(1:7), 2013. Google Scholar
  9. Bruno Courcelle. Fundamental properties of infinite trees. Theoret. Comput. Sci., 25:95-169, 1983. Google Scholar
  10. Calvin C. Elgot. Monadic computation and iterative algebraic theories. In H. E. Rose and J. C. Sheperdson, editors, Logic Colloquium 1973, volume 80, pages 175-230, Amsterdam, 1975. North-Holland Publishers. Google Scholar
  11. Marcelo Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proc. Logic in Computer Science 1999, pages 193-202. IEEE Press, 1999. Google Scholar
  12. Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In Proc. LICS'99, pages 214-224. IEEE Computer Society Press, 1999. Google Scholar
  13. Peter Gabriel and Friedrich Ulmer. Lokal präsentierbare Kategorien, volume 221 of Lecture Notes Math. Springer-Verlag, 1971. Google Scholar
  14. Fabio Gaducci, Marino Miculan, and Ugo Montanari. About permutation algebras, (pre)sheaved and names sets. Higher-Order Symb. Comput., 19:283-304, 2006. Google Scholar
  15. Susanna Ginali. Regular trees and the free iterative theory. J. Comput. System Sci., 18:228-242, 1979. Google Scholar
  16. Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:62-222, 1997. Google Scholar
  17. Richard Kennaway, Jan Willem Klop, Ronan Sleep, and Fer-Jan de Vries. Infinitary Lambda Calculus. Theoret. Comput. Sci., 175(1):93-125, 1997. Google Scholar
  18. Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Nominal coalgebraic data types with applications to lambda calculus. Log. Methods Comput. Sci., 9(4), 2013. Google Scholar
  19. Joachim Lambek. A fixpoint theorem for complete categories. Math. Z., 103:151-161, 1968. Google Scholar
  20. Stefan Milius. A sound and complete calculus for finite stream circuits. In Proc. LICS'10, pages 449-458. IEEE Computer Society, 2010. Google Scholar
  21. Stefan Milius, Marcello M. Bonsangue, Robert S.R. Myers, and Jurriaan Rot. Rational operation models. In Proc. MFPS XXIX, volume 298 of Electron. Notes Theor. Comput. Sci., pages 257-282, 2013. Google Scholar
  22. Stefan Milius and Thorsten Wißmann. Finitary corecursion for the infinitary lambda calculus. full version; available at http://arxiv.org/abs/1505.07736, 2015.
  23. Daniela Petrişan. Investigations into Algebra and Topology over Nominal Sets. dissertation, University of Leicester, 2011. Google Scholar
  24. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. Google Scholar
  25. Gordon D. Plotkin and Daniele Turi. Towards a mathematical operational semantics. In Proc. Logic in Computer Science (LICS'97), pages 280-291, 1997. Google Scholar
  26. Jan Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3-80, 2000. Google Scholar
  27. Jan Rutten. Rational streams coalgebraically. Log. Methods Comput. Sci., 4(3:9):22 pp., 2008. Google Scholar
  28. Thorsten Wiß mann. The rational fixed point in nominal sets and its application to infinitary lambda-calculus. Project report, available at http://thorsten-wissmann.de/theses/project-wissmann.pdf, October 2014.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact