Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories

TL;DR

This paper develops a categorical and algebraic framework for cyclic datatypes based on second-order algebraic theories, establishing correctness, normalization, and decidability results for their computation rules.

Contribution

It introduces a novel approach using second-order algebraic theories and Bekic law to handle cyclic datatypes with strong normalization and decidability guarantees.

Findings

Correctness of fold rules derived from categorical semantics

Proven strong normalization using the General Schema

Decidability of the equational theory of cyclic data

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. 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.

Figures