Makoto Hamana - Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories

lmcs:4066 - Logical Methods in Computer Science, November 15, 2017, Volume 13, Issue 4 -
Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories

Authors: Makoto Hamana

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.

Volume: Volume 13, Issue 4
Published on: November 15, 2017
Accepted on: November 15, 2017
Submitted on: November 15, 2017
Keywords: Computer Science - Logic in Computer Science,D.3.2,E.1,F.3.2


Consultation statistics

This page has been seen 480 times.
This article's PDF has been downloaded 271 times.