2026-07-24T08:24:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5979 2024-03-06T10:37:26Z ddc:004 open_access

Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories Hamana, Makoto cyclic data structures traced cartesian category fixed point functional programming fold 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Makoto Hamana 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.21 urn:nbn:de:0030-drops-59792 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.21 eng https://creativecommons.org/licenses/by/3.0/legalcode