Document Open Access Logo

Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories

Author Makoto Hamana

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.21.pdf
  • Filesize: 0.68 MB
  • 18 pages

Document Identifiers

Author Details

Makoto Hamana

Cite AsGet BibTex

Makoto Hamana. Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.21

Abstract

Cyclic data structures, such as cyclic lists, in functional programming are tricky to handle because of their cyclicity. This paper presents an investigation of categorical, algebraic, and computational foundations of cyclic datatypes. Our framework of cyclic datatypes is based on second-order algebraic theories of Fiore et al., which give a uniform setting for syntax, types, and computation rules for describing and reasoning about cyclic datatypes. We extract the ``fold'' computation rules from the categorical semantics based on iteration categories of Bloom and Esik. Thereby, the rules are correct by construction. Finally, we prove strong normalisation using the General Schema criterion for second-order computation rules. Rather than the fixed point law, we particularly choose Bekic law for computation, which is a key to obtaining strong normalisation.
Keywords
  • cyclic data structures
  • traced cartesian category
  • fixed point
  • functional programming
  • fold

Metrics

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

References

  1. Z. M. Ariola and S. Blom. Cyclic lambda calculi. In Theoretical Aspects of Computer Software, LNCS 1281, pages 77-106, 1997. Google Scholar
  2. Z. M. Ariola and J. W. Klop. Equational term graph rewriting. Fundam. Inform., 26(3/4):207-240, 1996. Google Scholar
  3. F. Blanqui. Termination and confluence of higher-order rewrite systems. In Rewriting Techniques and Application (RTA 2000), LNCS 1833, pages 47-61. Springer, 2000. Google Scholar
  4. F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive data type systems. Theoretical Computer Science, 272:41-68, 2002. Google Scholar
  5. S. L. Bloom and Z. Ésik. Iteration Theories - The Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer, 1993. Google Scholar
  6. P. Buneman, M. F. Fernandez, and D. Suciu. UnQL: A query language and algebra for semistructured data based on structural recursion. VLDB J., 9(1):76-110, 2000. Google Scholar
  7. C. Calcagno, P. Gardner, and U. Zarfaty. Context logic and tree update. In Proc. of POPL'05, pages 271-282, 2005. URL: http://dx.doi.org/10.1145/1040305.1040328.
  8. T. Coquand. Pattern matching with dependent types. In Proc. of the 3rd Work. on Types for Proofs and Programs, 1992. Google Scholar
  9. J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order abstract syntax in Coq. In Typed Lambda Calculi and Applications, LNCS 902, pages 124-138, 1995. Google Scholar
  10. A. Dovier, C. Piazza, and A. Policriti. An efficient algorithm for computing bisimulation equivalence. Theoretical Computer Science, 311:221-256, 2004. Issues 1-3. Google Scholar
  11. Z. Ésik. Axiomatizing iteration categories. Acta Cybernetica, 14:65-82, 1999. Google Scholar
  12. L. Fegaras and T. Sheard. Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space). In POPL'96, pages 284-294, 1996. URL: http://dx.doi.org/10.1145/237721.237792.
  13. M. Fiore and C.-K. Hur. Second-order equational logic. In Proc. of CSL'10, LNCS 6247, pages 320-335, 2010. Google Scholar
  14. M. Fiore and O. Mahmoud. Second-order algebraic theories. In Proc. of MFCS'10, LNCS 6281, pages 368-380, 2010. Google Scholar
  15. M. Fiore and S. Staton. Substitution, jumps, and algebraic effects. In Proc. of LICS'14, 2014. Google Scholar
  16. M. P. Fiore and M. D. Campos. The algebra of directed acyclic graphs. In Computation, Logic, Games, and Quantum Foundations, LNCS 7860, pages 37-51, 2013. Google Scholar
  17. N. Ghani, M. Hamana, T. Uustalu, and V. Vene. Representing cyclic structures as nested datatypes. In Proc. of TFP'06, pages 173-188, 2006. Google Scholar
  18. M. Hamana. Universal algebra for termination of higher-order rewriting. In Proc. of RTA'05, LNCS 3467, pages 135-149, 2005. Google Scholar
  19. M. Hamana. Higher-order semantic labelling for inductive datatype systems. In Proc. of PPDP'07, pages 97-108. ACM Press, 2007. URL: http://dx.doi.org/10.1145/1273920.1273933.
  20. M. Hamana. Initial algebra semantics for cyclic sharing tree structures. Logical Methods in Computer Science, 6(3), 2010. Google Scholar
  21. M. Hamana. Iteration algebras for UnQL graphs and completeness for bisimulation. In Proc. of Fixed Points in Computer Science (FICS'15), Electronic Proceedings in Theoretical Computer Science 191, pages 75-89, 2015. Google Scholar
  22. M. Hamana, K. Matsuda, and K. Asada. The algebra of recursive graph transformation language UnCAL: Complete axiomatisation and iteration categorical semantics. submitted. Google Scholar
  23. M. Hasegawa. Models of Sharing Graphs: A Categorical Semantics of let and letrec. PhD thesis, University of Edinburgh, 1997. Google Scholar
  24. S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, and K. Nakano. Bidirectionalizing graph transformations. In Proc. of ICFP 2010, pages 205-216, 2010. Google Scholar
  25. A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119(3):447-468, 1996. Google Scholar
  26. K. Matsuda and K. Asada. Graph transformation as graph reduction: A functional reformulation of graph-transformation language UnCAL. Technical Report GRACE-TR 2015-01, National Institute of Informatics, January 2015. Google Scholar
  27. L. G. L. T. Meertens. Paramorphisms. Formal Asp. Comput., 4(5):413-424, 1992. Google Scholar
  28. E. Meijer, M. M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In Proc of FPCA'91, pages 124-144, 1991. Google Scholar
  29. R. Milner. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci., 28(3):439-466, 1984. Google Scholar
  30. B. C.d.S. Oliveira and W. R. Cook. Functional programming with structured graphs. In Proc. of ICFP'12, pages 77-88, 2012. Google Scholar
  31. A. K. Simpson and G. D. Plotkin. Complete axioms for categorical fixed-point operators. In Proc. of LICS'00, pages 30-41, 2000. Google Scholar
  32. S. Staton. An algebraic presentation of predicate logic. In Proc. of FOSSACS 201, pages 401-417, 2013. Google Scholar
  33. S. Staton. Algebraic effects, linearity, and quantum programming languages. In Proc. of POPL'15, pages 395-406, 2015. Google Scholar
  34. G. Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993. Google Scholar
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