License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.21
URN: urn:nbn:de:0030-drops-59792
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5979/
Go to the corresponding LIPIcs Volume Portal

Hamana, Makoto

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

pdf-format:
LIPIcs-FSCD-2016-21.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{hamana:LIPIcs:2016:5979,
  author =	{Makoto Hamana},
  title =	{{Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5979},
  URN =		{urn:nbn:de:0030-drops-59792},
  doi =		{10.4230/LIPIcs.FSCD.2016.21},
  annote =	{Keywords: cyclic data structures, traced cartesian category, fixed point, functional programming, fold}
}

Keywords: cyclic data structures, traced cartesian category, fixed point, functional programming, fold
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI