Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories
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 algeb...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2017-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4066/pdf |
| _version_ | 1797268620661751808 |
|---|---|
| author | Makoto Hamana |
| author_facet | Makoto Hamana |
| author_sort | Makoto Hamana |
| collection | DOAJ |
| description | 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. 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. We also prove the property of "Church-Rosser
modulo bisimulation" for the computation rules. Combining these results, we
have a remarkable decidability result of the equational theory of cyclic data
and fold. |
| first_indexed | 2024-04-25T01:35:23Z |
| format | Article |
| id | doaj.art-46ff9b7f52224615a6bb2a103001fd2b |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:23Z |
| publishDate | 2017-11-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-46ff9b7f52224615a6bb2a103001fd2b2024-03-08T09:52:12ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742017-11-01Volume 13, Issue 410.23638/LMCS-13(4:8)20174066Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic TheoriesMakoto HamanaCyclic 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. 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. We also prove the property of "Church-Rosser modulo bisimulation" for the computation rules. Combining these results, we have a remarkable decidability result of the equational theory of cyclic data and fold.https://lmcs.episciences.org/4066/pdfcomputer science - logic in computer scienced.3.2e.1f.3.2 |
| spellingShingle | Makoto Hamana Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories Logical Methods in Computer Science computer science - logic in computer science d.3.2 e.1 f.3.2 |
| title | Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories |
| title_full | Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories |
| title_fullStr | Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories |
| title_full_unstemmed | Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories |
| title_short | Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories |
| title_sort | cyclic datatypes modulo bisimulation based on second order algebraic theories |
| topic | computer science - logic in computer science d.3.2 e.1 f.3.2 |
| url | https://lmcs.episciences.org/4066/pdf |
| work_keys_str_mv | AT makotohamana cyclicdatatypesmodulobisimulationbasedonsecondorderalgebraictheories |