{'fraction_non_alphanumeric': 0.05834331337325349, 'fraction_numerical': 0.010459081836327344, 'mean_word_length': 4.048468359532446, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 10, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 31, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
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 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.


Introduction
Cyclic data structures in functional programming are tricky to handle. In Haskell, one can define a cyclic data structure, such as cyclic lists by clist = 2:1:clist The feasibility of such a recursive definition of cyclic data depends on lazy evaluation. For example, one can safely take the head of the cyclic list: head clist 2 However, this encoding is not completely safe. For example, consider the sum of all elements using the above recursive encoding. of clist in Haskell. It falls into non-termination: sum clist non-termination This means that such a naive encoding of cyclic structure does not ensure safety.
The computation using our framework is guaranteed to be safe meaning that it is always terminating, i.e., strongly normalising. We provide a way to regard the sum of a cyclic list as a cyclic natural number, which is computed by the strongly normalising "fold" combinator. In this paper, we develop a framework for syntax and semantics of cyclic datatypes that makes this understanding and computation correct. Our framework of cyclic datatypes is founded on second-order algebraic theories of Fiore et al. [FH10,FM10]. Second-order algebraic theories are founded on the mathematical theory of second-order abstract syntax by Fiore, Plotkin, and Turi [FPT99,Ham04,Fio08] and have been shown to be a useful framework that models various important notions of programming languages, such as logic programming [Sta13], algebraic effects [FS14], quantum computation [Sta15]. This paper gives another application of second-order algebraic theories, namely, to cyclic datatypes and their computation. We use second-order algebraic theories to give a uniform setting for typed syntax, equational logic and computation rules for describing and reasoning about cyclic datatypes. We extract computation rules for the fold from the categorical semantics based on iteration categories [BÉ93]. Thereby the rules are correct by construction. Finally, we prove strong normalisation by using the General Schema criterion [Bla00] for second-order computation rules.
1.1. Overview of computation. As an overview of cyclic datatypes and their operations we develop in this paper, we first demonstrate descriptions and an operation of cyclic datatypes by pseudo-program codes. The code fragments correspond one-to-one to theoretical data given in later sections. Therefore, they are theoretically meaningful, while intuitively understandable without going into the detailed theory.
First we consider an example of cyclic lists. The codes below with the keyword ctype are intended to declare cyclic datatypes. Here we declare the type CNat of natural numbers and the type CList of cyclic lists having ordinary constructors in Haskell or Agda style. We assume that any ctype declared datatype has a default constructor "cy" for making a cycle. For example, we express a cyclic list of 1 as a term cy(x.1 :: x) where cy has a variable binding "x.", regarded as the "address" of the top of list. This is a fundamental idea presented in [FS96] [GHUV06].
A variable occurrence x in the body refers to the top, hence it makes a cycle. The terms built from the constructors of CList and the default constructor cy are required to satisfy the axioms AxCy (given later in Fig. 4) indicated by the keyword "with axioms" (we assume that any ctype datatype satisfies AxCy, so this is for ease of understanding). We next consider the above mentioned example of the sum of cyclic list.

sum : CList → CNat spec sum ([ ])
= 0 sum (k :: t) = plus(k, sum (t)) The above code with the keyword spec describes an equational specification of a function. It requires that the sum function from cyclic lists to cyclic natural numbers must satisfy the usual recursive properties of sum. We intend that the spec code is merely a (loose) specification, and not a definition, because it lacks the case of a cy-term. Here we assume that the plus function on CNat has already been defined (as presented later in Example 4.2). The following code with the keyword fun defines the function sum.
fun sum t = fold (0, k.x.plus(k,x)) t It is defined by the fold combinator on the cyclic datatypes. The first two arguments 0 and k.x.plus(k,x) correspond to the right-hand sides of the specification of sum, where k.x. are variable binders (as in λ-terms). The fold is actually the fold on a cyclic datatype, which knows how to cope with cy-terms. The sum of a cyclic list can be computed as follows: sum(cy(x.S 2 (0) :: S(0) :: x)) → + cy(x. fold (0, k.x.plus(k,x)) (x.S 2 (0) :: S(0) :: x;x)) → + cy(x.S(S(S(x)))) where we represent a usual natural number n by S n (0). The final term is a normal form that cannot be rewritten further. Therefore, we regard it as the computation result. The steps presented above are actual rewrite steps by the second-order rewrite rules FOLDr given later in Fig. 7. 1.2. Equational logical framework for cyclic computation. How to understand the meaning of the result cy(x.S(S(S(x)))) is arguable. The overall situation we have demonstrated is illustrated in Fig. 1. In this paper, we also provide a formal basis to understand and to reason about cyclic data, as well as computation results. We use second-order equational logic and the axioms AxCy to equate cyclic data formally ( Fig. 1 [II]). It completely characterises the notion of bisimulation on cyclic data. We can formally prove that an equation on cyclic data, such as cy(x.S(S(S(x)))) = cy(x.S(x)) (1.1) is derivable from the axioms AxCy in the second-order equational logic. Since AxCy characterises bisimulation, it means that the expression cy(x.S(S(S(x)))) is bisimilar to cy(x.S(x)), which is a minimal representation of the result regarded as ∞ (infinity). In this paper, we do not develop an explicit algorithm to extract such a minimal result from the computation result, but it is noteworthy that this equational theory generated by AxCy is decidable [BÉ93]. Consequently, it is computationally reasonable. More practical examples on cyclic datatypes and computation will be given in §7.
1.3. Proof by rewriting. In §6, we will develop a decidable proof method for equations involving functions defined by fold. We give an algorithm to prove whether an equation, e.g.
Our previous four papers [ GHUV06,Ham09,Ham10,Ham12] improved and extended it to various directions. Especially, [GHUV06,Ham09,Ham10] aimed to capture unique representations of cyclic sharing data structures (without any quotient) in order to obtain an efficient functional programming concept. In the present paper, we will assume the axioms AxCy and AxBr (Fig. 4) to equate bisimilar graphs. Uniqueness of representations is desirable, but uniqueness up to bisimilarity chosen in this paper is also desirable, because checking bisimilarity is efficiently decidable [DPP04] and reflects the meaning of cyclicity.
Oliveira and Cook [OC12] also improved [FS96] by using the parametric HOAS encoding [Chl08] of variable binding for cycle constructs (without any quotient), instead of HOAS, and developed generic fold combinators on them for functional programming.
In all the works mentioned in this subsection, bisimilarity was not used for identifications of cyclic structures.
1.5. Our recent work. In [Ham15,HMA], the author and collaborators gave algebraic and categorical semantics of a graph transformation language UnCAL [BFS00, HHI + 10] using iteration theories [BÉ93]. The graph data of UnCAL corresponds to cyclic sharing trees of type CTree in the present paper, where graphs are treated modulo bisimulation. UnCAL does not have the notion of types, thus structural recursive functions in UnCAL are always transformations from general graphs to graphs, thus typing such as sum:CList→CNat (in Introduction) or collect:FriendGraph→Names (in §7) could not be formulated. The present paper develops a suitable algebraic framework that captures datatypes supporting cycles and sharing.
1.6. Novelty of this paper. Since cyclic data structures is potentially dangerous because of cyclicity as exemplified in the begining of this section, termination of fold (or iterator) on cyclic structures should be ensured. However, none of the previous works including [FS96, GHUV06, Ham09, Ham10, Ham12, OC12, BFS00, HHI + 10, MA15] on cyclic structures have formally proved termination nor strong normalisation of fold, and the preservation of suitable equivalence on cyclic structures by fold. Moreover, these works did not developed a decidable proof method to prove equations on cyclic data with fold, such as the equation (1.2). In contrast to it, we will prove and provide a decidable proof method by showing rewriting properties of FOLDr, i.e. strong normalisation and Church-Rosser modulo bisimulation, which are new results. 1.7. Organisation. The paper is organised as follows. We first introduce cartesian secondorder algebraic theories, which give syntax and equational logic of cyclic datatypes in §2. We next give a categorical semantics of cyclic datatypes in §3. We then extract the fold function from the categorical semantics in §4. In §5, we extract second-order rewrite rules of fold and show strong normalisation. In §6, we prove Church-Rosser modulo bisimulation of the rewrite system of fold and then obtain decidability of the equational theory. In §7, we consider several examples of computing by fold on cyclic datatypes. In §9, we summarise the paper and discuss related work. This paper is the fully reworked and extended version of the conference paper [Ham16]. Besides proofs of all results, the present paper establishes Church-Rosser modulo bisimilarity (Thm. 6.8) and whence decidability of the theory of cyclic data and fold (Cor. 6.10). In addition, there is now a precise description of how primitive recursive functions are defined in our framework ( §4.4), and additional examples are provided ( §7).

Second-Order Algebraic Theory of Cyclic Datatypes
We introduce the framework of second-order cartesian algebraic theory, which is a typed and cartesian extension of second-order equational logic in [FH10] and [Ham07]. Here "cartesian" means that the target sort of a function symbol is a sequence of base types and we allow unrestricted substitution for variables. We use second-order algebraic theory as a formal framework to provide syntax and to describe axioms of algebraic datatypes enriched with cyclic constructs. The second-order feature is necessary for the cycle construct and the fold function on them. We will often omit superscripts or subscripts of a mathematical object if they are clear from contexts. We use the vector notation − → A for a sequence A 1 , · · · , A n , and | − → A | for its length.
2.1. Cartesian Second-Order Algebraic Theory. We assume that B is a set of base types (written as a, b, c, . . .), and Σ, called a signature, is a set of function symbols of the form where all a i , b i , c i are base types (thus any function symbol is of up to second-order type). A sequence of types may be empty in the above definition. The empty sequence is denoted by (), which may be omitted, e.g., b 1 , . . . , b m → c , or () → c. The latter case is simply denoted by c. A signature Σ c for type c denotes a subset of Σ, where every function symbol is of the form f : − → τ → c, which is regarded as a constructor of c. A metavariable is a variable of (at most) first-order type, declared as m : − → a → b (written as small-caps letters t, s, m, . . .).
A variable of a base type is merely called variable (written usually x, y, . . ., or sometimes written x b when it is of type b). The raw syntax is given as follows.
-Terms have the form t : The last form is called a meta-application, meaning that when we instantiate m : with a term s, free variables of s (which are of types − → a ) are replaced with (meta-)terms t 1 , . . . , t n (cf. Def. 2.1). We may write x 1 , . . . , x n . t for x 1 . · · · .x n . t, and we assume ordinary α-equivalence for bound variables. Terms are used for representing concrete cyclic data, functional programs on them and equations we want to model. A second-order equational theory is a set of proved equations built from terms (N.B. not meta-terms). Meta-terms are used for formulating equational axioms, which are expected to be instantiated to terms. A metavariable context Θ is a sequence of (metavariable:type)-pairs, and a context Γ is a sequence of (variable:base type)-pairs. A judgment is of the form If Θ is empty, we may simply write Γ t : − → b . A meta-term t is well-typed by the typing rules Fig. 2. We omit often the types for binders as . Given a meta-term t with free variables x 1 , . . . , x n , the notation t {x 1 → s 1 , . . . , x n → s n } denotes ordinary capture avoiding substitution that replaces the variables with terms s 1 , . . . , s n .
Definition 2.1. (Substitution of terms for metavariables) Let Γ = y 1 : inductively defined as follows.   Remark 2.2. The syntactic structure of meta-terms and substitution for abstract syntax with variable binding was introduced by Aczel [Acz78]. This formal language allowed him to consider a general framework of rewrite rules for calculi with variable binding. This influenced Klop's rewrite system of Combinatory Reduction System (CRS) [Klo80]. A second-order substitution in the sense of Courcelle [Cou83] is very similar to a substitution for metavariables but there are no variable binders in the language used in [Cou83] where function symbols are the targets of replacements (instead of metavariables in our framework).
For meta-terms Θ Γ s : or denoted by Γ s = t : − → b when Θ is empty. The cartesian second-order equational logic is a logic to deduce formally proved equations from a given set E of equations, regarded as axioms. The inference system of equational logic is given in Fig. 3. Note that the symmetry rule is derivable because of symmetry of (Ax1) and (Ax2).
2.2. Preliminaries for datatypes. The default signature Σ def is given by the following function symbols called default constructors: This means that any base type has default constructors. We assume that any signature Σ includes Σ def in this paper. A datatype declaration for a type c is given by a triple consisting of a base type c, signature Σ c and axioms E, where every f ∈ Σ c is of the form where − → a are types other than c (which may be empty), and any equation in E is built from Σ c -terms.
2.3. Instance (1): Cyclic Lists modulo Bisimulation. We will present an algebraic formulation of cyclic datatypes. By a cyclic datatype, we mean an algebraic datatype having the cycle construct cy satisfying the axioms that characterise cyclicity. The first example is the datatype of natural numbers. It has already been defined as CNat in Introduction as a pseudo code. We now give a formal definition using a datatype declaration. The datatype declaration for CNat is given by (CNat, Σ CNat , AxCy) where Σ CNat is 0 : CNat, S : CNat → CNat and the axioms AxCy are given in Fig. 4. The second example is the datatype of cyclic lists. It has already been defined as CList in Introduction as a pseudo code. Fix a ∈ B. The datatype declaration for CList a , the cyclic lists of type a, is given by (CList a , Σ CLista , AxCy) where Σ CLista is given by (− :: a −) : a, CList a → CList a and the axioms AxCy are given in Fig. 4. Note that CList a has also the default constructors, thus one can form a cycle (see the example below). The definition of CList in Introduction actually represents the datatype declaration (CList CNat , Σ CListCNat , AxCy). Hereafter, we often omit the type parameter subscript a of CList. The axioms AxCy mathematically characterise that cy is truly a cycle constructor in the sense of Conway fixed point operator [BÉ93]. The equational theory generated by AxCy captures the intended meaning of cyclic lists. For example, the following are identified as the same cyclic list: Axioms AxCy for cycles Axioms AxBr([ ], +) for branching Note that the axiom AxBr([ ], +) is parameterised by the function symbols [ ], +. In general, writing AxBr(ν, µ) where ν : c, µ : c, c → c ∈ Σ con , we mean the set of axioms obtained from the above axioms by replacing [ ] with ν, and + with µ.
which is an instance of the axiom (dinat) when t is identity (i.e. t → x for x : c x : c).
2.4. On axioms AxCy. We explain the intuitive meaning of the axioms in AxCy. Parameterised fixed-point axioms axiomatise cy as a fixed point operator. They (minus (CI)) are equivalent to the axioms for Conway operators of [BÉ93,Has97,SP00]. Bekic law is well-known in denotational semantics (cf. [Win93, §10.1]) to calculate the fixed point of a pair of continuous functionns. Conway operators are also arisen in work independently of Hyland and Hasegawa [Has97], who established a connection with the notion of traced cartesian categories [JSV96]. There are equalities that holds in the cpo semantics but Conway operators do not satisfy. The axiom (CI) is the commutative identities of Bloom andÉsik [BÉ93,SP00], which ensures that all equalities that hold in the cpo semantics do hold. See also [SP00, Section 2] for a useful overview about this. The equality generated by AxCy is bisimulation on cyclic lists. This is included in the equality of cyclic sharing trees given in the next subsection.
2.5. Instance (2): Cyclic Sharing Trees modulo Bisimulation. Next we consider the datatype of binary branching trees, which can involve cycle and sharing. We call them cyclic sharing trees, or simply cyclic trees. We first give the declaration of datatype CTree of cyclic trees as the style of pseudo code below, where we assume that f 1 , . . . , f n 's part denotes various unary function symbols such as a,b,c,p,q,. . ..
(cf. Fig. 5 (F)). Note that the first argument of composition has a binder (e.g. x.), which indicates a placeholder filled by the shared part after (e.g. p([])). A binder at the first argument of -term may be a sequence of variables (e.g. "x,y." in (E)), which will be filled by terms in a tuple (e.g. <p([]),q([])>). Cyclic trees are very expressive. They cover essentially XML trees with IDREF, the data model called trees with pointers [CGZ05], and arbitrary rooted directed graphs (cf. Fig. 5 (B)(E)). We denote by ∼ the equivalence relation generated by the axioms AxCy, AxBr([ ], +) in Fig. 4. Using the axioms AxCy ∪ AxBr([ ], +), we can reason this equality ∼ in the second-order equational logic. The equality ∼ gives reasonable meaning of cycles as in the case of cyclic lists. The branch + is associative, commutative and idempotent (cf. Fig. 5 (C)), thus nested + can be seen as an n-ary branch (cf. Fig. 5 (D)). Moreover, a shared term and its unfolding are also identified by ∼ because of the axiom (sub) (cf. Fig. 5 (F)). The axiom (sub) is similar to the β-reduction in the λ-calculus.
2.6. Algebraic theory of bisimulation. Actually, ∼ is exactly bisimulation on cyclic trees. Since unary f expresses a labelled edge, and + expresses a branch, cyclic sharing trees are essentially process graphs of regular behaviors, called charts by Milner in [Mil84]. Infinite unfolding of them are synchronization trees [BÉ93]. Thus the standard notion of bisimulation between graphs can be defined. Intuitively, starting from the root, bisimulation is by comparing traces of labels of two graphs along edges (more detailed definition is given
There are many other instances of cyclic datatypes, some of which will be given in §7.

Categorical Semantics of Cyclic Datatypes
In this section, we give a categorical semantics of cyclic datatypes. A reason to consider categorical semantics is to systematically obtain a "structure preserving map" on cyclic datatypes. We will formulate the "fold" function for a cyclic datatype as a functor on the category for cyclic datatypes (Thm. 3.9 and §4).
Since a cyclic datatype has cycles, the target categorical structure should have a notion of fixed point. It has been studied in iteration theories of Bloom andÉsik [BÉ93]. In particular iteration categories [Ési99] are suitable for our purpose, which are traced cartesian categories [JSV96,Has97] satisfying the commutative identities axiom [BÉ93]. We write 1 for the terminal object, × for the cartesian product, −, − for pairing, and ∆ = id, id for diagonal in a cartesian category.
Definition 3.1. [Ési99,BÉ93] A Conway operator in a cartesian category C is a family of functions (−) † : C(A × X, X) → C(A, X) satisfying: An iteration category is a cartesian category having a Conway operator satisfying the "commutative identities" law [BÉ93] f . . , π m : X m → X (see also [SP00]). An iteration functor between iteration categories is a cartesian functor that preserves Conway operators. A typical example of iteration category is the category of CPO complete partial orders (cpos) with bottom and continuous functions [BÉ93,Has97], where the least fixed point operator is a Conway operator.
We assume the following interpretations in any Σ def -structure: ] M holds. Importantly, every Σ def -structure satisfies the axioms AxCy because C is an iteration category.
Definition 3.4. A (Σ, E)-structure is a Σ-structure M in C satisfying all equations in a set E of axioms. Let N be a (Σ, E)-structure in an iteration category D. We say that an iteration functor F : Note that it induces the interpretation of every function symbol f ∈ Σ c given by . . , t n for any A in C. We say that an iteration functor F : Example 3.5. (The datatype CList a of cyclic lists of type a) We give a CList astructure in the iteration category CPO via the standard initial algebra characterisation of datatypes in the category CPO ⊥ of cpos and strict continuous functions [AJ94]. We write that 1 is the cpo {⊥} (which is the initial object of CPO ⊥ ), where ⊥ is the least element, ⊕ is the coalesced sum, and (−) ⊥ is lifting.
Let A be the interpretation [[a]] L of a base type a in CPO. We construct an initial algebra L of the functor F on CPO ⊥ defined by F (X) = 1 ⊥ ⊕ (A × X) ⊥ by using the initial algebra construction [SP82], i.e., taking the colimit of ω-chain we have a cpo L ∼ = F (L), consisting of finite and infinite possibly partial lists with continuous functions nil : 1 → L and cons : A × L → L. The order of the cpo is the usual pointwise ordering ⊥ t, and (t 1 , t 2 ) (t 1 , t 2 ) if t 1 t 1 and t 2 t 2 , etc. Then we have a and all the axioms in AxCy hold in CPO, since these are now well-known propeties of cpos [Win93,BÉ93,SP00]. Note that this construction is the same as modelling the lazy list datatype, hence this also shows that our framework covers modelling lazy datatypes as in Haskell.
Example 3.6. (The cyclic tree type CTree) A CTree-structure in an iteration category C is given by a (Σ def , AxCy ∪ AxBr It satisfies all axioms of AxBr([ ], +). Note that every CTree-structure is a degenerated commutative bialgebra (cf. [FC13]) in a cartesian category C, i.e., N forms also a comonoid (N, !, ∆) that satisfies the compatibility Thus, a CTree-structure models branch (by µ) and sharing by (∆) of cyclic sharing trees. We next give a syntactic category and a Σ-structure to prove categorical completeness. Let Σ be a signature, and E a set of axioms which is the union of AxCy and axioms for all datatype declarations of base types c. Given axioms E, all proved equations Γ s = t : − → c (which must be the empty metavariable context) by the second-order equational logic (Fig.  3), defines an equivalence relation = E on well-typed terms, where we also identify renamed terms by bijective renaming of free and bound variables. We write an equivalence class of terms by = E as [Γ t : − → c ] E . We define the category Tm(E) of term judgments modulo = E by taking Proposition 3.7. Tm(E) is an iteration category, and has a (Σ, E)-structure U.
Proof. We define a Σ-structure U by [[c]] U c for each c ∈ B, and Then these data turn Tm(E) into an iteration category, and moreover, U forms a (Σ, E)structure because of the axioms E for each c ∈ B. Moreover,

Then [[t]] U = [t]
E holds for all well-typed terms t. Using it, we have the following.
The above equations mean that Ψ is an iteration functor that sends the (Σ, E)-structure U to M . Such Ψ is uniquely determined by these equations because U is a (Σ, E)-structure.

4.1.
Axiomatising fold as a second-order algebraic theory. The fold is a function on equivalence classes of term judgments modulo E characterised by (3.2). Equivalently, we regard it as a function on terms (or term judgments) that preserves = E , i.e.
In this subsection, we axiomatise the function fold c b as the laws of fold within second-order equational logic using (3.2). Axiomatising fold. We next axiomatise the fold operation as a second-order algebraic theory. The type of fold may be chosen as where the first m-arguments correspond to the c-structure α. But in second-order algebraic theory, the codomain of function symbol must be a sequence of base types ( §2.1), so the We resolve this by simply uncurrying. We axiomatise the fold as the function symbol of the type and we will write a term of it using the notation In general, we can consider fold Hereafter, we assume that any signature Σ is divided into the default signature Σ def , a signature for constructors Σ con , and fold's: In other words, we assume that any function symbol other than a default constructor or fold is an element of Σ con .
In Fig. 6, we give the axioms FOLD, which axiomatise fold by using the characterisation (3.2) in case of a particular category C = Tm(E) and a c-structure as a second-order algebraic theory. To ease understanding, we explicitly describe an instance of (5) as (5') for the case c = CList, d = (::). Note that there is no case of fold c b (E, − → y . z; − → y ) for z ∈ { − → y }. ( Cleaning rules for c satisfying AxBr([ ], +) In (7r), | − → s | = 1 is also allowed and the part − → s is simply a single metavariable s.  We omit writing contexts and types of equations for simplicity. For example, formally the axiom (1) in FOLD is written as The arguments of fold expressing the c-structure are abbreviated as E for simplicity. We state the correctness of this axiomatisation, which holds by the above faithful construction. The following is immediate by construction.
Proposition 4.1. The following are equivalent.

4.2.
Primitive recursion by fold. The fold axiomatised above covers the ordinary fold on algebraic datatypes. Thus, we expect that various techniques on fold developed in functional programming, such as the fold fusion technique and representation of recursion principles such as [MFP91] may be transferred to the current setting. Here we consider a way to implement a particular pattern of recursion appearing often in specifications as a fold.
We suppose the following form of specification and definition.
We define π 1 (v, w. v). We assume that every e d is a closed term of type b, which may involve terms of the types f (t i ) : b t i : c for each i = 1, . . . , n, (i.e. − → t = t 1 , . . . , t n may appear solely, cf. examples in §7 in e d ). We define e d to be a term obtained from e d , by replacing every f (t i ) with v i of type b, and every t i (not in the form f (t i )) with w i of type c, and assume v 1 : b, w 1 : c, . . . , v n : b, w n : c e d : b.
The above specification can be seen as describing primitive recursion, because it is similar to the primitive recursion on natural numbers f (S(n)) = e(f (n), n), where both n and f (n) can be used at the right-hand side. In functional programming, it is known that primitive recursion on algebraic datatypes can be represented as fold, called paramorphism [Mee92]. We now take the fold where the target Σ-structure is the sequence b, c of types i.e.  The axioms FOLD in Fig. 6 is instantiated to the case of fold c b,c . For example, Other axioms for fold are instantiated similarly.
4.6. Properties. By construction, holds. Define E (v 1 , w 1 , . . . , v n , w n .e d ) d∈Σc . By induction on the typing derivations, we have fold c b,c (E, t) = f (t), t for all closed terms t of type c. By the characterisation (3.2), we have for each d ∈ Σ con , hence we have f (d( − → a , − → t )) = e d meaning that f satisfies the specification. We use this representation of primitive recursion in §7.

Strongly Normalising Computation Rules for FOLD
We expect that FOLD provides strongly normalising computation rules. An immediate idea is to regard the axioms FOLD as rewrite rules by orienting each axiom from left to right.
But proving strong normalisation (SN) of FOLD is not straightforward. The sizes of both sides of equations in FOLD are not decreasing in most axioms. So, assigning some "measure" to the rules in FOLD that is strictly decreasing is difficult for this case. Such a naive method is typically dangerous for higher-order rewrite rules and might lead one to an unintentional mistake. If the axioms regarded as second-order rules are a binding Combinatory Reduction System (CRS) [Ham05] (cf. Remark 2.2), meaning that every meta-application m[t 1 , . . . , t n ] is of the form m[ − → x ], then it is possible to use a simple polynomial interpretation to prove termination of second-order rules [Ham05]. Unfortunately, this is not the case because in (5) there is a meta-application violating the condition. Existence of meta-application means that it essentially involves the β-reduction, thus it has the same difficulty as proving strong normalisation of the simply-typed λ-calculus.
We use a general established method of the General Schema [BJO02,Bla00], which is based on Tait's computability method to show strong normalisation (SN). The General Schema has succeeded to prove SN of various recursors such as the recursor in Gödel's System T. The basic idea of the General Schema is to check whether the arguments of recursive calls in the right-hand side of a rewrite rule are "smaller" than the left-hand sides' ones. It is similar to Coquand's notion of "structurally smaller" [Coq92], but more relaxed and extended. 5.1. General Schema. We review the General Schema criterion [Bla00,Bla16]. For more details and the proofs, see the original papers [Bla00,Bla16].
The General Schema is formulated for a framework of rewrite rules called inductive datatype systems, whose second-order fragment is essentially the same as the present formulation given in §2. Minor differences are adapted as follows. We use greek letters such as α, σ, τ , . . . to denote types. Roman alphabets such as a, b, c, . . . are used for base types.
(i) The target of function symbols must be a single (not necessary base) type in an inductive datatype system. Hence we introduce the product type constructor ×, assume that b 1 × b 2 is again a base type in the sense of §2.3, and use it for the target type.
Definition 5.1. A set of rewrite rules induces the following relation on function symbols in a signature Σ: f depends on g if there is a rewrite rule defining f (i.e. whose left-hand side is headed by f ) in the right-hand side of which g occurs. Its transitive closure is denoted by > Σ .
where Acc(t) is the least set satisfying the following clauses: (a1) t ∈ Acc(t).
(a3) If c( − → s ) ∈ Acc(t) then each s i ∈ Acc(t) for a constructor c. A position p is a finite sequence of natural numbers. The order on positions is defined by p < q if there exists a non-empty p such that p p = q. Given a meta-term t, Pos(t) denotes the set of all positions of t. The notation t |p denotes a subterm of t at a position p, and t[s] p the term obtained from t by replacing the subterm at the position p by s.
Definition 5.4. A meta-term u is a covered-subterm of t, written t u, if there are two positions p ∈ Pos(t), q ∈ Pos(t |p ) such that • ∀r < p. t |r is headed by an abstraction, and • ∀r < q. t |pr is headed by a function symbol, including a constructor. Definition 5.5. Given f : is the least set CC satisfying the following clauses. We assume that all the terms below are well-typed.
where lex is the lexicographic extension of the strict part of .
If all the rules of R satisfy the General Schema, then R is strongly normalising.

5.2.
Refining second-order algebraic theory to second-order rewrite rules. In order to apply the General Schema criterion, we refine the second-order algebraic theories AxCy, AxBr and FOLD to the second-order rewrite rules FOLDr and SIMP.
Crucially, the constructors used in FOLD are not positive, as cy and involve a negative occurrence of c in (c → c). We can overcome this problem by modifying the type (c → c) to a restricted (Var c → c), where Var c is a base type having no constructor considered as the type of "variables" of type c. We assume the constructor v which embeds a "variable" into a term. We modify the types of default constructors as follows: where c's and a's are base types of the inductive datatype system (which may be product types), − − → Var a → c is short for Var a 1 → · · · → Var an → c. The type of fold is now The use of a type Var σ → τ to represent binders is well-known in the field of mechanized reasoning, sometimes called (weak) higher-order abstract syntax [DFH95].
We also modifty the type of composition as − − : (a 1 , . . . , a n → c), a 1 × · · · × a n → c which is not a constructor in the sense of Def. 5.2, hence it is allowed as not positive (when a i = c).

5.3.
Second-order rewrite systems FOLDr and SIMP. We now describe how we obtain the second-order rewrite rules FOLDr and SIMP given in Fig. 7 and 8. Note that FOLDr's "r" stands for "rewrite". The rewrite system FOLDr is an oriented version of FOLD. The axiom (5) is refined to (5r) by applying Composition rules which is need to prove SN. Because of it, a rule corresponding to (6) is not needed in FOLDr. The axiom (sub) in AxCy involves a meta-application at the right-hand side, which performs general substitution of terms for variables − → y of base types. The oriented version of it is the rule (7r).
The rewrite system SIMP is for simplification, whose rules are taken from the equational theory of AxCy ∪ AxBr. We include the Bekic law as a rewrite rule (10r), which can be depicted as: It says that the fixed point of a pair can be obtained by computing the fixed points of its components independently and composing them suitably (see the right figure). It can be seen as decreasing complexity of cyclic computation because looking at the argument of cy, the number of components of tuple is reduced. The superscript of cy in (10r) indicates the length of the tuple argument (see §2.1). Such a superscript indicating an invariant of the arguments is similar to the idea of higher-order semantic labelling [Ham07], but here we just make the existing superscript explicit rather than labelling. Hence it is suitable for rewrite rules and actually shown to be terminating (cf. the proof of Thm. 5.9).
We define the relation → FOLDr (resp. → SIMP ) on terms by the relation generated by the second-order equational logic Fig. 3 under the axioms FOLDr (resp. SIMP) without using the (Ax2), (Ref) and (Tra)-rules. Namely, "one-step rewriting" → FOLDr is equational reasoning without using symmetry, reflexivity and transitivity. By construction, we immediately see that the rewrite system FOLDr correctly implements the second-order algebraic theory FOLD. The following proposition is immediate by construction of rules. We writeť for a term that recovers the original terms t by stripping the constructor v.
Theorem 5.9. The second-order rewrite system FOLDr ∪ SIMP is strongly normalising.
Proof. We use the the General Schema criterion using the well-founded relation > Σ on function symbols fold, > cy m > cy n > any other constructors where natural numbers m > n ≥ 1. Now all constructors are positive.
In the following proof, we write f ( s. We show that FOLDr ∪ SIMP satisfies the General Schema, i.e., for each rewrite rule f ( The implication "⇐=" expresses backward inference, which is labelled with a number indicating which clause in Def. 5.3 or Def. 5.5 is applied. In what follows, for brevity, we examine mostly the cases that the length of bound variables is 1 (i.e. | − → x | = | − → y | = 1) and the arity of d is 2. General cases are proved similarly.
The first literal holds because − → s are accesible in − → s . The second literal holds by (a2)(a1).
. In what follows, unlabelled cy denotes cy m or cy n .
The first literal easily holds. The second literal holds by , cy( − → y . s), each of which holds easily.
The remaining cases are simpler and similarly proved. By Thm. 5.7, we have strong normalisation of FOLDr ∪ SIMP. is strongly normalising without imposing any reduction strategy. For (i), consider the situation that one defines a function which calls other functions. Since in this paper, our methodology is that any function on cyclic datatypes is defined using fold, this situation is realised using fold involving other fold's.

Decidability of Equational Theory
In this section, we show an important property of our framework, namely, the decidability of the equational theory generated by AxCy, AxBr and FOLDr. This is done by investigating another important rewriting property, Church-Rosser modulo bisimulation of FOLDr. SN of FOLDr established in the previous section also plays an important role to establish Church-Rosser modulo bisimulation. Note that since the rewrite rules SIMP is merely a subset of an oriented version of theorems derived from AxCy ∪ AxBr, we do not need to include SIMP for the decidability of equational theory.
Notation 6.1. Hereafter, we omit writing the variable term constructor v in terms used in FOLDr for simplicity. For example, we will simply write cy(x. x) to mean cy(x. v(x)). We may write simply → for the rewrite relation → FOLDr . We write → * for the reflexive transitive closure, → + for the transitive closure, and ← for the converse of →. We define ↔ → ∪ ←.
The notation nf(t) denotes a unique normal form of t. We write t ! → t if t → * t and t is a normal form, meaning rewriting to a normal form.
6.2. Confluence on plain terms. We consider confluence on terms without any quotient.
Note that this result does not contradict known counterexamples to confluence of graph rewriting systems [AK96], [Has97,Example 2.4.3]. Counterexamples to confluence in [AK96] use the fixed point law as a rewrite rule, while our FOLDr does not have the fixed point law.
Proposition 6.4. The normal form of a term by rewriting with FOLDr is unique.
Proof. Since FOLDr is confluent.
We analyse the structure of normal forms. We call a term a value if it follows the grammar (d ∈ Σ con ): t, t 1 , . . . , t n :: Proof. We abbreviate fold(e, − → y .t; − → y ) as fold(t). By induction on the structure of values.
Base cases: y and 's normal forms are themselves. Induction step: Case t = t 1 , t 2 is a value.
6.4. A decidable proof method for the equational theory. CR ∼ is a desirable property, because the diagram (6.1) describes a proof method of s (∼ ∪ ↔) * t, i.e., s = t is derivable from AxCy ∪ AxBr and the equational theory generated form FOLDr.
We explain the reason why CR ∼ is useful below. We suppose that CR ∼ holds. Now CR ∼ means that a proof of s (∼ ∪ ↔) * t, where s and t are connected by disordered combinations of ∼, →, ←, is always transformed to a proof s → * s ∼ t ← * t for some s , t . But this is still not good enough, because it is not clear how many times we should rewrite s and t to reach suitable s and t . For the case of FOLDr, we can further transform it to an equivalent proof (cf. Notation 6.1) which means that one first normalises the terms s, t to the unique normal forms s 0 , t 0 by FOLDr and then compares them by the equality ∼. The reasons why this method is possible are (i) → is SN, (ii) → has the unique normal form property (iii) → * preserves ∼ by CR ∼ , and (iv) the bisimulation ∼ is decidable.
Hence (6.2) gives a decidable proof method for the equational theory generated by FOLDr, AxCy and AxBr.
6.5. Establishing CR ∼ . Unfortunately, CR ∼ does not hold on unrestricted terms. For example, letting e (l, t. 2 :: t), we have the following situation, which violates CR ∼ . A waved line in the diagram denotes ∼. Note that the left-hand side rewrite applies (4r)(5r), which pushes fold into the constructor cy, and changes 1 to 2, because of the definition of e. A crucial point is that cy(x.1 :: fold(e, x)) involves a normal form fold(e, x), where x is bound by a binder placed upward. There are three possibilities that such a bound variable x appears: where a variable x is bound by one of binders − → y , and C is a context that does not bind x.
Now e = − → x 1 .e 1 , . . . , − → x m .e m . The cases (b) and (c) are no problem, i.e., they do not fall into a situation as the diagram (6.3). The only problematic case is (a). Hence, we exclude such terms from consideration. Definition 6.6. Given a term t, if nf(t) has a subterm of the form where s involves a variable x bound by one of binders − → y of cy, then we call t a bad term.
We define a set of non-bad terms as follows: T {t | Γ t : − → c with t is not bad, and every first m-arguments e of fold are closed }.
The condition that the first m-arguments e of fold (cf. 4.2) are closed is to avoid similar problems.
Proposition 6.7. The set T is closed under the rewrite relation → FOLDr and one step application of an axiom in AxCy and AxBr.
Proof. If t ∈ T then t → FOLDr t ∈ T because FOLDr does not produce a bad term if t does not involve a bad term. Similarly, an application of an axiom in AxCy and AxBr does not produce a bad term if t does not involve a bad term. Note that substitution of terms for variables are always capture-avoiding.
Note that a bad term does not simply mean that fold does not appear under cy. A term where fold appears under cy is allowed, when s does not involve the bound variables − → y of cy. For example, the right-hand side of the rule (4r) in FOLDr is not bad. We use the following theorem to show CR ∼ .
Theorem 6.8. [AT12, Cor. 2.3] Let ∼ be an equivalence relation and → a binary relation on the same set. Suppose is a symmetric relation such that * = ∼. If → is locally confluent in one step), and then → is Church-Rosser modulo ∼.
We apply the above theorem to our situation. We now take → to be → FOLDr , ∼ to be the bisimulation restricted on T , and to be a relation on T defined by: Namely, the symmetric relation is the congruence closure of one-step application of an instance of an axiom of AxCy ∪ AxBr on T . Thus * = ∼. The condition (i) of Thm. 6.8 holds by Thm. 5.9. We check the conditions (ii) and (iii) of Thm. 6.8.
Proposition 6.9. The relations → FOLDr on T is locally uniformly confluent.
Proposition 6.10. The relation → FOLDr on T is locally uniformly coherent.
Proof. Let → denote → FOLDr on T . We need to show that for an instance s = t of each axiom such that s has a reduct s , s and t commute modulo ∼. Thus we check all possible cases of the form s ← s t. This is by induction on the proof of s t. Throughout the proof, we write t { − → s } for t{ − → y → − → s }. Let − → y = y 1 , . . . , y n , − → s = s 1 , . . . , s n .
The case s i is rewritten is similar. * If the root of ( − → y .t) − → s is rewritten, then it is finally rewritten to t { − → s }.
If − → s or t is rewritten, similarly to the above case. We have where C is obtained from C replacing every y i in C with s i for 1 ≤ i ≤ n.
The converse is similar. which is bad. Therefore, this case is excluded.
(i) Case s or t is rewritten. Similarly to the case (SP).
• (Fun) and (OSub): By induction hypothesis and the fact that rewriting and equational reasoning are closed under contexts and substitutions for variables.
As discussed in §6.4, we have a remarkable result.
Corollary 6.13. The equational theory generated by FOLDr, AxCy and AxBr on terms of T is decidable.
Since FOLDr is SN and CR ∼ , we have the following fundamental property.
We define ctail by fold. Rather than the fixed point law, another important principle of cyclic structures of Bekic law plays a crucial role here.
Example 7.3. We define the datatype of cyclic strings consisting of a, b, the empty string ε, and the choice operator "|".
ctype CString where a : CString → CString b : CString → CString ε : CString | : CString,CString → CString with axioms AxCy,AxBr(ε,|) We consider the function aa? that checks whether a given closed term contains two consecutive a's, such as a(a(·)). For example, (a(b(ε)))) ) Even in case of a string containing cycle, the function must return a correct result. For example, we expect the following results.
aa?( cy(x.a(x)) ) ! → true aa?( b(cy(x.a(b(a(x))))) ) ! → true We now specify aa? by using the function head-a? which checks whether the head is a. head-a? : CString → ABool spec head-a?(a(t)) = true head-a?(b(t)) = false aa? : CString → ABool spec aa?(a(t)) = head-a?(t) aa?(b(t)) = aa?(t) aa?( ε ) = false aa?(s | t) = aa?(s) ∨ aa?(t) The results of aa? must be boolean, but it should not be the type Bool defined in Example 7.1. Now we need the type ABool of "additive" boolean, meaning that it has the conjunction "∨" with the unit false, because the specification of aa? requires that the unit ε (resp. the multiplication "|") of CString is mapped to the unit false (resp. the multiplication "∨") of the target type.
One may think that it needs expansion of the inner term of cy. We show that the rewrite system FOLDr ∪ SIMP does it without using the fixed point law, rather, by using Bekic law. We write folde for fold (v.w.<head-a?(w),a(w)>, v.w.<v,b(w)>,...).
Example 7.4. This example shows that our cyclic datatype has ability to express graphs. The graph shown below right represents friend relationship, which describes Bob knows Alice, and Carol knows Alice and Bob. To make it a rooted graph, it has the uppermost node "+" which points to the nodes of three persons. This is represented as a term (a.b.c.a+b+c) cy(a.b.c.<name("alice"), name("bob")+knows(a), name("carol")+knows(a)+knows(b)>) which we call g. The term g is of type FriendGraph defined as follows. We define a function collect that collects all names in a graph as a name list of type Names.
Nishimura and Ohori [Nis97,NO99] developed a general mechanism for programming with cyclic structures in a purely functional style using the representation of system of equations. They developed the "reduce" operation on cyclic structures based on a mechanism for data-parallelism on recursive data, which is fold in our sense, although bisimilar cyclic structures are not identified in their work. 8.2. Foundational graph rewriting calculi. There has been various work to deal with graph computation and cyclic data structures in functional programming and foundational calculi including [FS96, GHUV06, Ham09, Ham10, Ham12, OC12, HHI + 10, MA15, AK96, AB97]. Foundational graph rewriting calculi, such as equational term graph rewriting systems [AK96], are general frameworks of graph computation. The fold on a cyclic datatype in this paper is more restricted than general graph rewriting. However, our emphasis is clarification of the categorical and algebraic structures of cyclic datatypes and the computation by fold on them by regarding fold as a structure preserving map, rather than unrestricted rewriting. This was a key to obtain SN and CR ∼ of FOLDr. We also hope that it will be useful for further optimisation such as the fold fusion based on semantics as done in [HMA,§4.3]. The general study of graph rewriting was also important for our study at the foundational level. The unit "[ ]" of branching in AxBr corresponds to the black hole constant "•" considered in [AK96], due to [BÉ93]. This observation has been used to give an effective operational semantics of graph transformation in [MA15].

Conclusion
In this paper, we have developped foundations of cyclic datatypes and computation: [I] Syntax and type system supporting algebraic datatypes with cycle and sharing constructs ( §2) [II] Complete equational axioms for bisimulation of cyclic data (Fig. 4) [III] Algebraic theory FOLD of fold on cyclic datatypes and its strongly normalising rewrite system FOLDr (Fig. 7, Fig. 6) ( §4, §5), which is Church-Rosser modulo bisimulation ( §6) [IV] The framework that supports [I]-[III] based on cartesian second-order algebraic theory ( §2.1) and iteration category ( §3). The numbered items [I]-[III] in Fig. 1 in Introduction are instances of these results.
We have not assumed any particular operational semantics nor strategy to obtain strongly normalising fold on cyclic data. This point may be useful to deal with cyclic datatypes in proof assistances requiring terminating functions, such as Coq or Agda. We have shown several concrete examples of cyclic data computation in §7. In this paper, we have focused on the underlying theory of cyclic datatypes. Formal development of the programming language that realises the program codes described in this paper is left for a future work.