Document Open Access Logo

A Coinductive Representation of Computable Functions

Authors Alvin Tang , Dirk Pattinson

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CALCO.2025.7.pdf
  • Filesize: 0.67 MB
  • 15 pages
HTML5 Logo HTML (experimental)
LIPIcs.CALCO.2025.7.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Streaming models
  • Theory of computation → Recursive functions
Keywords
  • Computability
  • Coinduction

Metrics

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

Abstract

We investigate a representation of computable functions as total functions over 2^∞, the set of finite and infinite sequences over {0,1}. In this model, infinite sequences are interpreted as non-terminating computations whilst finite sequences represent the sum of their digits. We introduce a new definition principle, function space corecursion, that simultaneously generalises minimisation and primitive recursion. This defines the class of computable corecursive functions that is closed under composition and function space corecursion. We prove computable corecursive functions represent all partial recursive functions, and show that all computable corecursive functions are indeed computable by translation into the untyped λ-calculus.

Cite As Get BibTex

Alvin Tang and Dirk Pattinson. A Coinductive Representation of Computable Functions. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CALCO.2025.7

Author Details

Alvin Tang
  • The Australian National University, Canberra, Australia
Dirk Pattinson
  • The Australian National University, Canberra, Australia

Acknowledgements

The term "hiaton" to describe a token that symbolises a computational step without visible observations was suggested by Thomas Streicher.

References

  1. Samson Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Inf. Comput., 105(2):159-267, 1993. URL: https://doi.org/10.1006/inco.1993.1044.
  2. Robert Atkey and Conor McBride. Productive coprogramming with guarded recursion. ACM SIGPLAN Notices, 48(9):197-208, 2013. URL: https://doi.org/10.1145/2500365.2500597.
  3. Henk Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  4. Michael Barr and Charles Wells. Category Theory for Computing Science. Prentice Hall, 1989. Google Scholar
  5. Henning Basold and Helle Hvid Hansen. Well-definedness and observational equivalence for inductive-coinductive programs. Journal of Logic and Computation, 29(4):419-468, 2019. URL: https://doi.org/10.1093/logcom/exv091.
  6. George Mark Bergman. An Invitation to General Algebra and Universal Constructions. Universitext. Springer, Cham, 2nd edition, 2015. URL: https://doi.org/10.1007/978-3-319-11478-1.
  7. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Foundational extensible corecursion: a proof assistant perspective. In Kathleen Fisher and John Reppy, editors, Proc. ICFP 2015, pages 192-204. Association for Computing Machinery, 2015. URL: https://doi.org/10.1145/2784731.2784732.
  8. Ana Bove, Alexander Krauss, and Matthieu Sozeau. Partiality and recursion in interactive theorem provers - an overview. Mathematical Structures in Computer Science, 26(1):38-88, 2014. URL: https://doi.org/10.1017/S0960129514000115.
  9. Martín Hötzel Escardó. On lazy natural numbers with applications to computability theory and functional programming. SIGACT News, 24(1):61-67, 1993. URL: https://doi.org/10.1145/152992.153008.
  10. Joel David Hamkins. A survey of infinite time turing machines. In Jérôme Olivier Durand-Lose and Maurice Margenstern, editors, Proc. MCU 2007, volume 4664 of Lecture Notes in Computer Science, pages 62-71. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74593-8_5.
  11. Bart Jacobs and Jan Rutten. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin, 62:222-259, 1997. Google Scholar
  12. Dexter Kozen. Theory of Computation. Texts in Computer Science. Springer, London, 2006. URL: https://doi.org/10.1007/1-84628-477-5_7.
  13. Rasmus Ejlers Møgelberg. A type theory for productive coprogramming via guarded recursion. In Proc. CSL-LICS 2014, pages 1-10, New York, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2603088.2603132.
  14. Dirk Pattinson and Lutz Schröder. Program Equivalence is Coinductive. In Proc. LICS 2016, pages 337-346, New York, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2934506.
  15. Anton Setzer. Partial Recursive Functions in Martin-Löf Type Theory. In Proc. CiE 2006, volume 3988 of Lecture Notes in Computer Science, pages 505-515. Springer, 2006. URL: https://doi.org/10.1007/11780342_51.
  16. Joseph Robert Shoenfield. Recursion Theory. Lecture Notes in Logic. Springer, 1993. Google Scholar
  17. Tarmo Uustalu and Varmo Vene. Primitive (Co)Recursion and Course of Value (Co)Iteration, Categorically. INFORMATICA (IMI, Lithuania), 10:5-26, 1999. URL: https://doi.org/10.3233/INF-1999-10102.
  18. Wolfgang Wechler. Universal Algebra for Computer Scientists, volume 25 of EATCS Monographs on Theoretical Computer Science. Springer, 1992. URL: https://doi.org/10.1007/978-3-642-76771-5.
  19. Klaus Weihrauch. Computable Analysis. Springer, 2000. Google Scholar
  20. Glynn Winskel. The formal semantics of programming languages: an introduction. MIT Press, 1993. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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