日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

Cyclic Datatypes modulo Bisimulation and
Decidable Equational Theory for Fold
Makoto Hamana

1 Introduction
Cyclic data structures in functional programming
are tricky to handle because of their cyclicity. In
Haskell, one can define a cyclic data structure, suchas cyclic lists byclist = 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. It
might fall into a non-terminating situation. For
example, what is the sum of all elements of clist?
One may think that it is non-terminating, undefined, or impossible.
The answer using our framework in this paper isdifferent. We do not rely on lazy evaluation. 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 thispaper, 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. [16][17]. Second-order algebraic theories are founded onmathematical theory of second-order abstract syntax by Fiore, Plotkin, and Turi [18] [22] [15] and have
巡回データ型とその fold のための決定可能な等式理論
This paper is unrefereed, and a revised and extended
version of a paper by the same author presented at
1st International Conference on Formal Structures
for Computation and Deduction.
Makoto Hamana, 群馬大学 理工学府, Dept. of Computer Science, Gunma University.

been shown to be a useful framework that models various important notions of programming languages, such as logic programming [38], algebraic
effects [19], quantum computation [39]. This paper
gives another application of second-order algebraic
theories, namely, to cyclic datatypes and its computation. We use second-order algebraic theories togive 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 [6]. Thereby therules are correct by construction. Finally, we provestrong normalisation by using the General Schema
criterion [3] for second-order computation rules.
Overview. As an overview of cyclic datatypes
and their operations we develop in this paper, wefirst 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 aretheoretically meaningful and more intuitive thanstarting from detailed theory.
First we consider an example of cyclic lists. The
code below with the keyword ctype is intended todeclare a cyclic datatype CList of cyclic lists having two ordinary constructors in Haskell or Agda
style.
ctype CList where[ ] : CList:: : CNat,CList → CListwith axioms AxCy
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 termcy(x.1::x)

“infinity”

cyclic natural number[I] cy(x.2::1::x)

[III]
fold

2

1
clist
図1

sum

S

[II]
AxCy

S

=

S

equational theory
for bisimulation

S

Framework: Second-order algebraic theories and iteration theories

can be computed as follows:
where cy has a variable binding “x.”, regarded as
the “address” of the top of list. A variable occurrence x in the body means to refer to the top, hence
it makes a cycle. The terms built from the constructors of CList and the default constructor cy isrequired to satisfy the axioms AxCy (given later in
Fig. 4) as the keyword “with axioms” mentioned(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 ofcyclic list. We define another cyclic datatype ofnatural numbers.
ctype CNat where
0 : CNatS : CNat → CNatwith axioms AxCy
sum : CList → CNat
spec sum ([ ])= 0sum (k :: t) = plus(k, sum (t))
The code with keyword spec at the right column
describes an equational specification of function. It
requires that the sum function from cyclic lists tocyclic natural numbers must satisfy the ordinary
definition. We intend that the spec code is merelya (loose) specification, and not a definition, because
it lacks the case of cy-term. We here assume thatthe 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 thecyclic datatypes, as in an ordinary fold on algebraic datatypes. The first two arguments 0 andk.x.plus(k,x) correspond to the right-hand sidesof the specification of sum. The fold is actually thefold on a cyclic datatype, which knows how to copewith cy-terms. Actually, the sum of a cyclic list

sum(cy(x.S2 (0) :: S(0) :: x))→+ cy(x. fold (0, k.x.plus(k,x))(x.S2 (0) :: S(0) :: x;x))+→ cy(x.S(S(S(x))))where we represent n by Sn (0). The final term isa 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 laterin Fig. 7.
How to understand the meaning of the resultcy(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
the computation result. We use second-order equational logic and the axioms AxCy to equate cyclic
data formally (Fig. 1 [III]). It completely characterises the notion of bisimulation on cyclic data.
The expression cy(x.S(S(S(x)))) is equal to (i.e.
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. Consequently, it is computationally reasonable. Morepractical examples on cyclic datatypes and computation will be given in §7.
Organisation. The paper is organised as follows.
We first introduce cartesian second-order algebraic
theory, which gives syntax and equational logic of
cyclic datatypes in §2. We next give a categoricalsemantics 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 therewrite system of fold and then obtain decidabilityof the equational theory. In §7, we consider several

examples of computing by fold on cyclic datatypes.
In §8, we summarise the paper and discuss relatedwork.

2 Second-Order Algebraic Theory of
Cyclic Datatypes
We introduce the framework of second-ordercartesian algebraic theory, which is a typed andcartesian extension of [16] [17] and [24]. 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 secondorder algebraic theory as a formal framework toprovide 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 mathematicalobject if they are clear from contexts. We use the−→vector notation A for a sequence A1 , · · · , An , and−→| A | for its length.
2. 1 Cartesian Second-Order Algebraic
TheoryWe assume that B is a set of base types (written
as a, b, c, . . .), and Σ, called a signature, is a set offunction symbols of the form
−
→
−
→
→
f : (−
a1 → b1 ), . . . , (−a→m → bm ) → c1 , . . . , c n .
where all ai , bi , ci are base types (thus any function
symbol is of up to second-order type). A sequenceof types may be empty in the above definition. The
empty sequence is denoted by (), which may beomitted, e.g., b1 , . . . , bm → 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 xb when
it is of type b). The raw syntax is given as follows.
- Terms have the formt ::= x | x.t | f (t1 , . . . , tn ).
- Meta-terms extend terms tot ::= x | x.t | f (t1 , . . . , tn ) | m[t1 , . . . , tn ].
The last form is called a meta-application, meaning→that when we instantiate m : −a → b with a term→s, free variables of s (which are of types −a ) are re-placed with terms t1 , . . . , tn (see Def. 2.1). We may
write x1 , . . . , xn . t for x1 . · · · .xn . t, and we assume
ordinary α-equivalence for bound variables. Terms
are used for representing concrete cyclic data, functional programs on them and equations we wantto model. A second-order equational theory is aset of proved equations built from terms (N.B. notmeta-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 isof the form−→
Θ . Γ ` t : b.
−→
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→.t , . . . , −as f ( −xx→
1 1
n .tn ). Given a meta-term t
with free variables x1 , . . . , xn , the notation s [x1 7→
s1 , . . . , xn 7→ sn ] denotes ordinary capture avoiding substitution that replaces the variables withterms s1 , . . . , sn .
Definition 2.1 (Substitution of terms for−→−→metavariables) Let Γ = y1 : b1 · · · , yk : b1 . Suppose−→niiΓ0 , x1i : a1i , . . . , xn
`si : bii : ai−→−→→→→b . Γ ` e :−→m1 : −
a1 → b1 , . . . , mk : −
a
c
k
k
→
→
i
where ni = |−ai | and −ai = a1i , . . . , an
i . Then a sub−−−−→−→
0
stitution Γ, Γ ` e [ m := s ] : c is inductively
defined as follows.
−−−−→x [ m := s ] , x−−−−→mi [t1 , . . . , tni ] [ m := s ]
−−−→
−−−−→
, si [x1 7→ t1 [ −m := s ], . . . , xni 7→ tni [ m := s ]]
−−−−→
−
→
−
→
f (y1 .s1 , . . . , ym .sm ) [ m := s ]
−−−−→
−−−→
−
→.s [ −, f (−→
y1 .s1 [ m := s ], . . . , y
m m m := s ])−−−−→where [ m := s ] denotes [m1 := s1 , . . . , mk := sk ].
−→For meta-terms Θ . Γ `s: b and−→Θ . Γ ` t : b , an equation is of the form−→
Θ . Γ ` s=t : b,−→or denoted by Γ ` s = t : b when Θ is empty.
The cartesian second-order equational logic is alogic to deduce formally proved equations from agiven set E of equations, regarded as axioms. They:b∈Γ
Θ . Γ ` y :b

−
→
−
→
→
−
→
f : (−
a1 → b1 ), · · · , (−a→m → bm ) → c ∈ Σ
−
→
−
−
−
→
Γ, xi : ai ` ti : bi (1 ≤ i ≤ m)−→−−→→
Θ . Γ ` f ( xa1 .t , . . . xam .t ) : −c−→(m : a1 , . . . , am → b ) ∈ Θ
Θ . Γ ` ti : ai (1 ≤ i ≤ m)−→
Θ . Γ ` m[t1 , . . . , tm ] : b
図2

1

1

m

m

Typing rules of meta-terms

−
→
→
→
→→−
→
(m1 : (−
a1 → b1 ), . . . , mk : (−abk ) . Γ ` t1 = t2 : −
c)∈E
k
−
→
0 −−−→0Γ , xi : ai ` si = si : bi (1 ≤ i ≤ k)
(Ax1)
−−−−→
−−−−→
→
Γ, Γ0 ` t1 [ m := s ] = t2 [ m := s0 ] : −
c
−
→
−
→
−
→
−
→
→
(m1 : (a1 → b1 ), . . . , mk : (ak → bk ) . Γ ` t1 = t2 : −c)∈E−→
0 −−−→0Γ , xi : ai ` si = si : bi (1 ≤ i ≤ k)
(Ax2)
−−−−→
−−−−→
→
Γ, Γ0 ` t [ m := s ] = t [ m := s0 ] : −
c
2

1

−
→
→
→
→→−
→
f : (−
a1 → b1 ), · · · , (−abk ) → −
c ∈Σ
k
−
→
−
−
−
→
0
Γ, xi : ai ` ti = ti : bi (1 ≤ i ≤ k)
(Fun)
−→
−→
−→
−→
→
Γ ` f (xa1 1 .t1 , . . . , xa1 1 .tk ) = f (xa1 1 .t01 , . . . , xa1 1 .t0k ) : −
c
(Ref)

(Tra)

−
→
Γ ` si = s0i : bi (1 ≤ i ≤ k)→
x1 : b1 , . . . , xk : bk ` t = t0 : −c(OSub)
−
−
−
→
−
−
−
→
→
Γ ` t [ x 7→ s ] = t0 [ x 7→ s ] : −c→Γ `s=t :−c→Γ `t=t :−c→Γ `t=u :−c−→Γ `s=u : c−−−−→
In (Ax1)(Ax2), [ m := s ] denotes [ m1 := s1 , . . . , mk := sk ].
−→s ] denotes [ x 7→ s , . . . , x 7→ s ].
In (OSub), [ −
x−7→
1
1
k
k
図3

Cartesian second-order equational logic

inference system of equational logic is given in Fig.
3. Note that the symmetry rule→Γ `s=t :−c(Sym)−Γ `t=s :→cis derivable because of symmetry of (Ax1) and(Ax2).

E, where every f ∈ Σc is of the form→f :−a , c, . . . , c → c,→
where −
a are types other than c (which may be
empty), and any equation in E is built from Σc terms.

Preliminaries for datatypes. The default signature Σdef is given by the following function symbols called default constructors:

2. 2 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 firstexample is the datatype of cyclic lists. It has already been defined as CList in Introduction as thepseudo code. We now give a formal definition using
a datatype declaration. Fix a ∈ B. The datatypedeclaration for CLista , the cyclic lists of type a, isgiven by (CLista , ΣCLista , AxCy) where ΣCLista is

Empty
hi
:()
→
→
→
→
Tuple
h−, · · · , −i:(−c1 ), . . . , (−cn ) → −c1 , . . . , −
cn
−
−
→
−
→
−
→
|→
c|
Cycle costr. cy:( c → c ) → c
→
→
→
→
−
−
Compo.
¦(→:(−a →−c ), −
a →−
c
a ,→
c)
→
→
→
→
defined for all base types −
a ,−
c ,−
c1 , . . . , −cn ∈ B.
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(c, Σc , E)consisting of a base type c, signature Σc and axioms[ ] : CLista ,(− ::a −) : a, CLista → CLista

and the axioms AxCy are given in Fig.
4.
Note that CLista has also the default constructors, thus one can form a cycle (see the exam-

Axioms AxCy for cycles
→
→
t:−
a →−
c,
. `
→
s1 , . . . , sn : −
a

(sub)
(SP)

→
t:−
c

(dinat)

→
→
s: −
a →−
c,
→
→
t: −
c →−
a

→
→
(−
y .t[−y ]) ¦ hs1 , . . . , sn i = t[s1 , . . . , sn ]

→
:−
c

→
→
. ` h(−
y .y1 ) ¦ t, . . . , (−y .yn ) ¦ ti = t

→
:−
c

→
→
→
→
→
→
cy(−
x .s[t[−x ]]) = (−z .s[−z ]) ¦ cy(−z .t[s[−z ]])]

. `

→
:−
c

→
→
→
−
→
→
→
b) ¦ cy(−h cy(−x . (−
y .t
y .b
s)),
c ,−
a →−
c , . ` cy(−
→
→
→
→
b, b
(Bekic̆) t : −x ,−y. h ts i) =
:−
c ,−
a
→
−
→
−
→
−
→
−
→
−
→
→
→
s: c, a → ab) ¦ cy(−cy( y . ( x .bs) ¦ cy( x . (−
y .t
y .b
s))) i
→
→
→
→
(CI)
t:−
a →−
a . `
cy(−
y .ht[ρ ], . . . , t[ρ ]i) = hcy(y.t̃ ), . . . , cy(y.t̃ )i
:−
a
1

m

In (CI), ρi = yi1 , . . . , yim , where i1 , . . . , im ∈ {1, . . . , m}, t̃ is short for t[y, . . . , y]. In (Bekic̆), bt and bs are short→→→→for t[−x,−y ] and s[−x ,−y ], respectively.

Axioms AxBr([ ], +) for branching(del)(unitL)(unitR)(assoc)(comm)(degen)

t:c
t:c
t:c
s, t, u : cs, t : c
t:c

. `
. `
. `
. `
. `
. `

cy(xc .x + t)[] + tt + [](s + t) + u
s+t
t+t

=
=
=
=
=
=

t
t
t
s + (t + u)
t+s
t

:c
:c
:c
:c
:c
:c

Note that the axiom AxBr([ ], +) is actually 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 µ.
図4

ple below). The definition of CList in Introduction actually represents the datatype declaration(CListCNat , ΣCListCNat , AxCy). Hereafter, we will omit
the type parameter subscript a of CList. The axioms AxCy mathematically characterise that cy istruly a cycle constructor in the sense of Conway
fixed point operator [6]. The equational theory generated by AxCy captures the intended meaning ofcyclic lists. For example, the following are identified as the same cyclic list:

AxCy

2

=

AxCy

2

2

=

2

2

2

cy(x.2 :: x) = 2 :: cy(x.2 :: x) = 2 :: 2 :: cy(x.2 :: x)These equalities come from the fixed point law of
cy:
→
→
→
→
(fix) cy(−x .s[−x ]) = s[ cy(−z .s[−z ]]) ]
which is an instance of the axiom (dinat) when t→→
is identity (i.e. t 7→ −x for −x−→: c ` h−x i : c) with(sub).

AxiomsOn axioms AxCy. We explain the intuitive meaning of the axioms in AxCy. Parameterised fixedpoint axioms axiomatise cy as a fixed point operator. They (minus (CI)) are equivalent to the axioms for Conway operators of [6] [27] [37]. Bekic̆ law
is well-known in denotational semantics (cf. [41])to calculate the fixed point of a pair of continuousfunctions. Conway operators are also arisen in work
independently of Hyland and Hasegawa [27], whoestablished a connection with the notion of traced
cartesian categories [30]. 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 Ésik [6] [37], which ensuresthat all equalities that hold in the cpo semantics
do hold. See also [37] for a useful overview about
this. The equality generated by AxCy is actuallybisimulation on cyclic lists. This is included in theequality of cyclic sharing trees given in next subsection.

2. 3 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 ofcyclic trees as the style of pseudo code below, where
we assume that f1 , . . . , fn ’s part denotes various
unary function symbols such as a,b,c,p,q,. . ..
ctype CTree where
f1 : CTree → CTree.
.
.
fn : CTree → CTree[ ] : CTree+ : CTree,CTree → CTreewith axioms AxCy,AxBr([ ],+)
Formally, it is expressed as the datatype declaration (CTree, {f1 , . . . , fn , [ ], +}, AxCy∪AxBr([ ], +)).
The binary operator + denotes a branch. For example, one can write b([])+c([]) (cf. Fig. 5 (A)).
The datatype can express sharing by the constructor ¦ of composition:(x.a(b(x) + c(x))) ¦ p([])(cf. Fig. 5 (F)). Note that the first argument ofcomposition ¦ 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, thedata model called trees with pointers [9], 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 ofcycles 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.
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 processgraphs of regular behaviors, called charts by Milnerin [35]. Infinite unfolding of them are synchronization trees [6]. 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 (moredetailed definition is given in [6] [35] or ( [26] Appendix)). Now we see that (C),(F) and (G) are
examples of bisimulation. Actually, the axioms in
Fig. 4 are sound for bisimulation, i.e. for each axiom, the left and the right-hand sides are bisimilar.
Moreover, it is complete.

x

Proposition 2.2 ( [25],( [26] 5.3)) Γ ` s = t :CTree is derivable from AxCy and AxBr([ ], +) iff if
s and t are bisimilar.
The main reason of this is that the axioms AxCyand AxBr([ ], +) are a second-order representationof Bloom and Ésik’s complete equational axioms ofbisimulation [6]. A crucial fact is that bisimulation s ∼ t is decidable [6] [8]. There is also an efficient algorithm for checking bisimulation, e.g. [12].
Hence, cyclic datatypes with the axioms AxCy, or
the axioms AxCy ∪ AxBr are computationally feasible. For example, equality on cyclic structures suchas the one we have seen in Fig. 1 can be checked
efficiently.
There are many other instances of cyclic
datatypes, some of which will be given in §7.

3 Categorical
Datatypes

SemanticsofCyclicIn this section, we give a categorical semantics ofcyclic datatypes. A reason to consider categoricalsemantics is to systematically obtain a “structure
preserving map” on cyclic datatypes. We will formulate the “fold” function for a cyclic datatype as afunctor on the category for cyclic datatypes (Thm.
3.8 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 ofBloom and Ésik [6]. In particular iteration categories [13] are suitable for our purpose, which aretraced cartesian categories [30] [27] satisfying thecommutative identities axiom [6]. We write 1 forthe terminal object, × for the cartesian product,h−, −i for pairing, and ∆ = hid, idi for diagonal ina cartesian category.
Definition 3.1 [13] [6] A Conway operator in a
cartesian category C is a family of functions (−)† :

+

(A)

b
[]

a

[]

y

+

(F)

a
x

x

b

y

p
(x,y.a(x)+x+y)

+

[]

[]

c

x

x

(x.b(x)+c(x))

図5



+

c

b

a

[]

[]

[]

bc
[]

[]

b([])+c([]) = c([])+b([])

+

b

(D)

+

c

+

b

c

p

p

[]

[]

+

(G)

=



[]

[]
<p([]),q([])>

+

b

p

q
[]

(C)

c

cy(x.a(cy(y.b(c(x)+y)))b([])+c([])
(E)

x

(B)

c

(sub)

t

t

p([]) = b(p([]))+c(p([]))

axiom (del)Examples of cyclic sharing treesC(A × X, X) → C(A, X) satisfying:(f ◦ (g × idX ))† = f † ◦ g ,(f †)† = (f ◦ (idA × ∆))† ,f ◦ hidA , (g ◦ hπ 1 , f i)†i = (f ◦ hπ 1 , gi)†.
An iteration category is a cartesian category having a Conway operator satisfying the “commutative
identities” law [6]hf ◦ (idA × ρ1 ), . . . , f ◦ (idA × ρm )i†= ∆m ◦ (f ◦ (idA × ∆m ))† : A → X
where• f : A × Xm → X• diagonal ∆m , hidX , · · · , idX i : X → X m• ρi : X m → X m such that ρi = hqi1 , . . . , qim iwhere each qij is one of projections π 1 , . . . , π m :X m → X (see also [37]).
An iteration functor between iteration categories
is a cartesian functor that preserves Conway operators.
A typical example of iteration category is the category of complete partial orders (cpos) and continuous functions [6] [27], where the least fixed point
operator is a Conway operator.
Definition 3.2 Let Σ be a signature.
A Σstructure M in an iteration category C is specified
by giving for each base type b ∈ B, an object [[b]]M(or simply written [[b]]) in C, and for each function
−
→
−
→
→
−
→
symbol f : (−a1 → b1 ), . . . , (−a→m → bm ) → c , a
−
→
M
−
→
function [[f ]]A : C(A × [[a1 ]], [[ b1 ]]) × · · · × C(A ×−→→- C(A, [[−[[−a→c ]]) which is natural inn ]], [[bn ]])A, where [[b1 , . . . , bn ]] , [[b1 ]] × . . . × [[bn ]]. Also
given a context Γ = x1 : b1 , . . . , xn : bn , we set[[Γ]] , [[b1 , . . . , bn ]]. The superscript of [[−]] may beomitted hereafter.
Interpretation. Let M be a Σ-structure in an
iteration category C. We give the categorical mean→ing of a term judgment Γ ` t : −c (where there are→no metavariables) as a morphism [[t]]M : [[Γ]] → [[−c ]]in C defined by[[Γ ` yi : c]]M = π i : [[Γ]] → [[c]]
M
−→
−−→
→
[[Γ ` f ( xa1 1 .t1 , . . . xann .tn ) : −
c ]]
−
→M
−−−−→
= [[f ]]M[[Γ]] ( [[Γ, x1 : a1 ` t1 : b1 ]] , . . . ,
−
→ M
−−→
[[Γ, −x−n : an ` tn : bn ]] ).
We assume the following interpretations in any
Σdef -structure:[[h i]]M= ! :A→1
A[[h−, . . . , −i]]M
(t
,
.
.
.
,
t
)
=
ht1 , . . . , tn i
1nA[[¦]]M(t,s)=
t ◦ hidA , siA†[[cy]]M(t)=t
A
We say a Σ-structure M satisfies an equationΓ ` s = t : c, if [[s]]M = [[t]]M holds. Importantly,
every Σdef -structure satisfies the axioms AxCy because C is an iteration category.
Definition 3.3 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 : C → D
preserves (Σ, E)-structures if F ([[−]]M ) = [[−]]N .
A c-structure (M, α) for a datatype declaration

(c, Σc , E) is a (Σc , E)-structure M with a family ofmorphisms of C; α , ( ([f ])M : [[b1 ]]×. . .×[[bn ]] →[[c]] )f :b1 ,...,bn →c∈Σc . It actually defines a (Σc , E)M
structure by [[f ]]M◦ ht1 , . . . , tn i
A (t1 , . . . , tn ) , ([f ])for any A in C. We say that an iteration functor
F : C → D preserves c-structures if F ([[c]]M ) =[[c]]N , and F (([f ])M ) = ([f ])N for every f ∈ Σc .

Example 3.4(The cyclic list datatype
CList) A CList-structure is given by a (Σdef , AxCy)structure M having the interpretations of “[ ]” and
“::”.

•

Proposition 3.6 Tm(E) is an iteration category,and has a (Σ, E)-structure U.
Proof. We define a Σ-structure U by [[c]]U , c forUeach c ∈ B and [[f ]]→−a , f for each function symbol→
f and arbitrary base types −a . We take•••

Example 3.5 (The cyclic tree type CTree)
A CTree-structure is given by a (Σdef , AxBr ∪AxBr([ ], +))-structure M where [[CTree]]M = N
and N is a commutative monoid object (N, η : 1 →N, µ : N × N → N ) in C satisfying([[ ]])M = η,([+])M = µ.
It satisfies AxBr([ ], +). Note that every CTreestructure is a degenerated commutative bialgebra(cf. [20]) in a cartesian category C, i.e. N forms
also a comonoid (N, !, ∆) that satisfies the compatibility∆◦η = η×η∆ ◦ µ = (µ × µ) ◦ (id × hπ 2 , π 1 i × id) ¦ (∆ × ∆)µ ◦ ∆ = id.
The last equation is by µ ◦ ∆ = µ ◦ hid, idi =µ ◦ hid, (µ)†i =(dinat) (µ)† = id. Thus, a CTreestructure 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 whichis the union of AxCy and axioms for all datatypedeclarations of base types c. Given axioms E, all→proved equations Γ ` s = t : −c (which must
be the empty metavariable context) by the secondorder equational logic (Fig. 3), defines an equivalence relation =E on well-typed terms, where wealso identify renamed terms by bijective renamingof free and bound variables. We write an equiva→
lence class of terms by =E as [Γ ` t : −c ]E . We define the category Tm(E) of term judgments modulo=E by taking→• objects: sequences of base types −c→→• morphisms: [Γ ` t : −c ] : [[Γ]] → [[−c ]], theE→→
identity: [−x−→: c ` h−
xi :−
c ]E
−−→
−
→
→
composition: [x : b ` s : −c ]E ◦[Γ ` t : b ]E ,→→[Γ ` (−x .s) ¦ t : −c ]E•terminal object: ()• pair: h[s]E , [t]E i ,→→[Γ ` hs , ti : −c1 , −
c2 ]E
product: concatenation of sequences→
Conway op.: ([Γ, −x−→:c `t :−c ]E )†−→c−→= [Γ ` cy(x .t) : c ]E
projections: [x1 : c1 , x2 : c2 ` xi : ci ]E

Then these data satisfy that Tm(E) is an iteration category and U forms a (Σ, E)-structure because of the axioms E for each c ∈ B. Moreover,([[c]]U , (f )f ∈Σc ) is a c-structure.
Then [[t]]U = [t]E holds for all well-typed terms t.
Using it, we have the following.
Theorem 3.7 (Categorical soundness and→completeness) Γ ` s = t : −c is derivable iffMM[[s]]C = [[t]]C holds for all iteration categories C andall (Σ, E)-structures in C.

Theorem 3.8 For a (Σ, E)-structure M in an iteration category C, there exists a unique iteration
functor ΨM : Tm(E) - C that preserves (Σ, E)structures. Pictorially, it is expressed as the following diagram, where Tm denotes the set of all terms(without quotient).
Tm[[−]]M[[−]]U- Tm(E)

¡
¡ ΨM
? ª
C

Proof. We write simply Ψ for ΨM . Since Ψ preserves (Σ, E)-structures, Ψ([[−]]U ) = [[−]]M holds.
Hence Ψ([[t]]U ) = Ψ([t]E ) = [[t]]M for any t, meaning that the mapping Ψ is required to satisfyΨ([Γ ` yi : c]E )= πi
Ψ([Γ ` h i : ()]E )=!
→→Ψ([Γ ` hs , ti : −c1 , −
c 2 ]E )−→→= hΨ[Γ ` s : c1 ]E , Ψ[Γ ` t : −c2 ]E i−→c−→Ψ([Γ ` cy(x .t) : c ]E )→= (Ψ[Γ, −x−→:c `t :−c ]E )†−→−−→
Ψ([Γ ` f ( xa1 1 .t1 , . . . , xamm .tm ) : c]E )M−−→= [[f ]][[Γ]] (Ψ[Γ, −x−
1 : a1 ` t1 : b1 ]E , . . .)−→b
Ψ([Γ ` (x .t) ¦ s : c]E )−−→−→= Ψ[Γ, x : b, ` t : c]E ◦ hid[[Γ]] , Ψ[Γ ` s : b ]E i
(1)
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 Fold on Cyclic Datatypes
Fix a cyclic datatype c (say, the type CList of
cyclic lists). By the previous theorem, for a cstructure M , the interpretation [[−]]M determinesa c-structure preserving iteration functor ΨM . If
we take the target category C as also Tm(E), M
should be another cyclic datatype b (say, the CNatof cyclic natural numbers), where the constructorsof c are interpreted as terms of type b. For example, the sum of a cyclic list in Introduction is understood in this way. Thus the functor ΨM determinedby [[−]]M can be understood as a transformation of
cyclic data from terms of type c to terms of type b.
Along this idea, we formulate the fold operation from the cyclic datatype c to another cyclic
datatype b by the functor ΨM . Let (c, Σc , Ec ) and(b, Σb , Eb ) be datatype declarations. Let E be theset of axioms collecting the axioms of all datatypedeclarations for types in B. Hence E ⊇ Eb ∪ Ec . We
define a (Σc , E)-structure (M, α) in Tm(E) by[[c]]M = b
M
and [[a]] = a for a 6= c. We write the arrow partfunction ΨM on hom-sets as the fold, i.e.
→→
foldcb (α) : Tm(E)(−c , c) - Tm(E)([[−c ]], b).
(2)→
where −
c = c1 , . . . , cn (N.B. some of ci may be c).
4. 1 Formalising fold as a second-order algebraic theory
The fold is a function on equivalence classes ofterm judgments modulo E including AxCy ∪ AxBr
characterised by (1). Equivalently, we regard it as
a function on terms (or term judgments) that pre-serves =E , i.e.
s =E t ⇒ foldcb (α)(s) =E foldcb (α)(t).
In this subsection, we axiomatise the function foldcb
as the laws of fold within second-order equational
logic using (1).
Formalising a c-structure (M, α).
To giveα = (([f ])M : [[a1 ]] × . . . × [[an ]] → [[c]])f :a1 ,...,an →c∈Σcis to give terms x1 : [[a1 ]], . . . , xn : [[an ]] ` ef : b for
all f : a1 , . . . , an → c ∈ Σc such that ([f ])M = [ef ]E .
Note that [[c]] = b. We represent α as a tuple ofterms ef according to function symbols in Σc by
the order of datatype constructors listed in a ctype
declaration of c.
Formalising fold. We next axiomatise the foldoperation as a second-order algebraic theory. The
type of fold may be chosen as
→
−
→
−
→
foldcb : ([[−
a1 ]] → b), . . . , ([[−
a→m ]] → b), ( c → c) → ([[ c ]] → b),
where the first m-arguments correspond to the cstructure α. But in second-order algebraic theory, the codomain of function symbol must be asequence of base types (§2. 1), so the codomain→([[−c ]] → b) is inappropriate. We resolve this bysimply uncurrying. We formalise the fold as thefunction symbol of the type
→
−
→
−
→
- b.
foldcb : ([[−
a1 ]] → b), . . . , ([[−
a→m ]] → b), ( c → c), [[ c ]]and we will write a term of it using the notation→.e , . . . , −−→ −→foldcb ( −xx→
1 1
m .em , y . t ; y )where each ei corresponds to ([fi ])M for fi ∈ Σc in→→
α. The last two arguments −y . t and −y may need−→
explanation. The first “ y . t” describes a term with→→variable binding “−y .” of types −c , but the second−→→“ y ” are free variables of types [[−c ]], which are different from the first bound variables, but have thesame length. We may write simply→.e , . . . , −foldcb ( −xx→
1 1
m .em , t )→by omitting the parameters after “;”, when |−y|=
0. This is a formalisation of the mathematical expression foldcb (α)([−y−→: c ` t : c]E ) at the level of semantics as a syntactic term.
→−c
In general, we can consider fold→− as the fold from
b
−
→
−
→
c to b . Hereafter, we assume that any signatureΣ is divided into the default signature Σdef , a signature for constructors Σcon , and fold’s:
→
−
→
c
−
→ −
− | c , b ∈ B}.
Σ = Σdef ∪ Σcon ∪ {fold→b

In other words, we assume that any function symbol other than a default constructor or fold is anelement of Σcon .

In Fig. 6, we give the axioms FOLD, which axiomatise fold by using the characterisation (1) incase of a particular category C = Tm(E) and ac-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 = (::).
→→
y . z; −y ) for
Note that there is no case of foldcb (E, −−→z 6∈ { y }. We omit writing contexts and types ofequations for simplicity. For example, formally theaxiom (1) in FOLD is written as→→
e1 : −
a1 → c, . . . , en : −a1 → c . `c−→→y ) = yi :foldb (e1 , . . . , en , y . yi ; −b

The arguments of fold expressing the c-structure
are abbreviated as E for simplicity. We also include the axioms and theorems (8)-(11) taken from
AxCy and AxBr for simplification. This importationof several axioms from AxCy ∪ AxBr to the secondorder algebraic theory FOLD is harmless because
our general framework is second-order equational
logic under E ∪ FOLD which includes AxCy ∪ AxBr.
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.
••

foldcb (α)([Γ ` t : c]E ) = [Γ0 ` u : b]E→.e , . . . , −→→` foldc (−xx→.e , −y. t ; −y) = u

: b
1 1
m m
b
is derived from the axioms E ∪ FOLD using thesecond-order equational logic.

where α, ei and t are fold free, Γ = y1 : c, . . . , yn :c, Γ0 = y1 : [[c]], . . . , yn : [[c]].

Example 4.2 The plus function on CNat can be
defined as fold as follows.
plus : CNat,CNat → CNat
spec plus(m, n) = pl(m)where pl(0)= npl(S(m)) = S(pl(m))
fun plus(m, n) = fold (n, x.S(x)) m
We specify plus in terms of a unary function plwhich recurses on the first argument m and gives
the second argument n if m = 0. Hence it is definedby fold where the target CNat-structure is defined
to be [[0]]M = n, [[S]]M (x) = S(x).

4. 2 Primitive recursion by fold
The fold formalised above covers the ordinary
fold on algebraic datatypes. Thus, we expect thatvarious techniques on fold developed in functional
programming, such as the fold fusion technique andrepresentation of recursion principles such as [34]may be transferred to the current setting. Here we
consider a way to implement a particular patternof recursion appearing often in specifications as a
fold.
Assumptions. Let (c, Σc , Ec ) and (b, Σb , Eb )be datatype declarations.
We suppose the following form of specificationand definition.
f
: c
→ b
−
→
→
spec f (d1 (−a , t )) = ed1
···
−
→
→
f (dn (−
a , t )) = edn
fun f (t) = π 1 ¦ foldcb,c ( (v1 , w1 , . . . , vn , wn .
→→he0d , d(−a ,−w )i)d∈Σc , t )(3)
We define π 1 , (v, w. v). We assume that every ed is a closed term of type b, which may
involve terms of the types` f (ti ) : b` ti : c−→for each i = 1, . . . , n, (i.e. t = t1 , . . . , tn may
appear solely, cf. examples in §7 in ed ). We
define e0d to be a term obtained from ed , byreplacing every f (ti ) with vi of type b, and every ti (not in the form f (ti )) with wi of typec, and assume
v1 : b, w1 : c, . . . , vn : b, wn : c ` e0d : b.
The above specification can be seen as describing primitive recursion, because it is similar theprimitive recursion on natural numbers f (S(n)) =e(f (n), n), where both n and f (n) can be usedat the right-hand side. In functional programming, it is known that primitive recursion on algebraic datatypes can be represented as fold, calledparamorphism [33]. We now take the fold where
the target Σ-structure is the sequence b, c of types
i.e. foldcb,c .
Structure. Let E be the set of axioms collecting
the axioms of all datatypes in B. Hence E ⊇ Eb ∪Ec .
We define a (Σc , E)-structure (M, α) in Tm(E) by[[c]]M = (b, c)M
and [[a]]= a, otherwise. If Ec contains axioms AxBr([ ], +), then Eb must contains axioms
AxBr(ν, µ), where ν : b, µ : b, b → b are in Σb .

Fold

−
→
; y b ) = yi b→;−y )=hi−→(1) foldcb (E, y c. yic→
y. h i(2) foldc (E, −()(for yic ∈ {y1c1 , . . . , yncn })

→
−
−
→
−
→
−
c1 ,→
c2
c1
c1
−
→ −
→
−
→
−
→
−
→ −
→ −
→
−
→ −
→ −
→
(3) fold→− →− (E, y . hs[ y ], t[ y ]i ; y ) = hfold→− (E, y . s[ y ]; y ), fold→− (E, y . t[ y ]; y )ib1 ,b1
b1
b2
→
→
→
→
→
→
→
→
→
→
→
→
(4) foldc (E, −y . cy(−x .t[−y ,−x ]) ; −y ) = cy(−x .foldc (E, −y ,−x. t[−y ,−x ]; −
y ,−
x ))
b

b

−
→
−
→ →
→
→
→
→
→
→
→
→
(5) foldcb (E, −y . d( a , t1 [−y ], . . . , tn [−y ]; −y ) = (−
x .ed [ a , −x ]) ¦ hfoldcb (E, −y . t1 [−y ]; −y ), . . .i
−
→
−
→
−
→
−
→
−
→
−
→
CList
0
CList
(E, y . t[ y ]; y ))(E, y . a :: t[ y ]; y ) = (x.e[a, x]) ¦ fold(5 ) fold
b

b

→
→
→
→
→
→
→
→
→
→
→
→
x. t[−x ]) ¦ fold(E, −y . s[−y ]; −y ); −x)y . (−
x .t[−x ]) ¦ s[−y ];−y ) = (−
x .foldcb (E, −(6) foldcb (E, −Bekic̆ and cycle cleaning for c with AxBr([ ], +)(7) cy(xc .x + t)→→b, b(8) cym+n (−x ,−y. h ts i)=t→(9) cy(−y .t)=t(10) cy(xc .x)

=[]

→
→
→
b) ¦ cyn (−= h cym (−x . (−
y .t
y .b
s)),
→
−
→
→
→
→
n −
m −
b) ¦ cyn (−cy ( y . ( x .bs) ¦ cy ( x . (−
y .t
y .b
s)))i

Composition→→(11) (−
y .t[−y ]) ¦ hs , . . . , s i1n→(N.B. t cannot contain −y)= t[s1 , . . . , sn ]Here E is a sequence (ed )d∈Σc of metavariables and d ∈ Σc . (5’) is an instance of (5) for explanation.
→→→→
In (8), bt and bs are short for t[−x ,−y ] and s[−x ,−y ], respectively.
→→
By the notation of metavariable, cy(−y .t) means that t cannot involve −y.
The axioms (7)-(10) are parameterised by the function symbols [ ], + as AxBr([ ], +).
図6

Second-order algebraic theory FOLD

Fold→(1r) foldcb (E, −y . v(yi )→(2r) foldc (E, −y. h i→;−y ) → v(yi )→;−y )→h i

()
→
− →
−

→
−

→
−

c1 ,c2
c1
c1
−
→ −
→ −
→
−
→ −
→ −
→
−
→ −
→
−
→
−
→
(3r) fold→− (E, y . t[ y ]; y )i
− (E, y . s[ y ]; y ), fold→− →− (E, y . hs[ y ], t[ y ]i ; y ) → hfold→b2
b1
b1 ,b1→→→→→→(4r) foldc (E, −y . cy1 (x.t[−y , x]) ; −y ) → cy1 (x.foldc (E, −y , x. t[−y , x]; −y , x))
b

b

−
→
−
→ →
→
→
→
→
→
foldcb (E, −y . d( a , t1 [−y ], . . . , tn [−y ]; −y ) → (−
x .ed [ a , −x ]) ¦→→→
hfoldcb (E, −y . t 1 [−y ]; −y ), . . .i
−
→
−
→
−
→
−
→
−
→
−
→
−
→
−
→
−
→
−
→
−
→
→
c
c
(6r) fold (E, y . ( x .t[ x ]) ¦ s[ y ] ; y ) → ( x .fold (E, x. t[ x ]) ¦ fold(E, y . s[ y ]; y ); −
x)

(5r)

b

b

Bekic̆ and cycle cleaning for c with AxBr([ ], +)(7r) cy(xc .v(x) + t)
0

→t

c

(7 r) cy(x .t + v(x))→→
b, b(8r) cym+n (−x ,−y. h ts i)→t→(9r) cy(−
y .t)

→t

c

(10r) cy(x .v(x))→→→b) ¦ cyn (−→ h cym (−x . (−
y .t
y .b
s)),
→
−
→
→
→
→
n −
m −
b) ¦ cyn (−cy ( y . ( x .bs) ¦ cy ( x . (−
y .t
y .b
s)))i
→[ ]

Composition−→→(11r) (−
y . v(y )) ¦ h s i→ si(for each d ∈ Σcon )
i
−
→
−
→
−
→ −
−
→
−
→
−
→
−
→
−
→
→
→
→
(12r) ( y . d( a , t1 [ y ], . . . , tk [ y ])) ¦ h s i → d( a , (→y . t 1 [−y ]) ¦ h s i, . . . , (−y . t n [−y ]) ¦ h s i)
図7Second-order rewrite system FOLDr→
For d : −a , cn → c ∈ Σcon , we define

this case. Such a naive method is typically dangerous for higher-order rewrite rules and might([ [ ] ])M=hη, [ ]i, lead one to an unintentional mistake. If the ax([+])M (hv1 , w1 i, hv2 , w2 i)= hµ(v1 , v2 ), w1 + w2 i ioms (regarded as second-order rules) are a bind→→→([d])M (−a , v1 , w1 , . . . , v n , wn ) =he0d , d(−a ,−w )i. ing CRS [23] (meaning that every meta-application→
m[t1 , . . . , tn ] is of the form m[−x ]), then it is posFormalisation. Then we have the function
sible to use a simple polynomial interpretation to→→c ]], (b, c)). prove termination of second-order rules [23]. Unfoldcb,c (α) : Tm(E)(−c , c) - Tm(E)([[−(4)
fortunately, this is not the case because in (5) andwhich is formalised as the function symbol(11) there are meta-applications violating the con−
→
−
→ −
→
→
foldcb,c : ([[−
a1 ]] → b ), . . . , ([[−
a→m ]] → b ), ( c →dition. Existence of meta-application means that→
- (b, c). The axioms FOLD in Fig. 6c), [[−c ]]it essentially involves the β-reduction, thus it has
the same difficulty as proving strong normalisation
is modified for the case of foldcb,c . For example, (1)of the simply-typed λ-calculus.
is
We use a general established method of the→General Schema [5] [3], which is based on Tait’s
x. xi ; v1 , w1 , . . . , vn , wn ) = hvi , wi i
foldcb,c (E, −computability method to show SN. The General
Schema has succeeded to prove SN of various reOther axioms for fold are modified similarly.
cursors such as the recursor in Gödel’s System T.
Properties.
By construction, ` ed=
The basic idea of the General Schema is to check(v1 , w1 , . . . , vn , wn. e0d ) ¦ hf (t1 ), t1 , . . . , f (tn ), tn i :whether the arguments of recursive calls in the theb holds. Define E , (v1 , w1 , . . . , vn , wn .e0d )d∈Σc .
right-hand side of a rewrite rule are “smaller” than
By induction on the typing derivations, we havethe left-hand sides’ ones. It is similar to Coquand’scfoldb,c (E, t) = h f (t), t i for all closed terms t ofnotion of “structurally smaller” [10], but more retype c. By the characterisation (1), we have forlaxed and extended.
each d ∈ Σcon ,−→→hf (d(−
a , t )), ti
5. 1 Refining second-order algebraic the−→→= foldcb,c (E, f (d(−a , t )))
ory to second-order rewrite rules→→= h(v1 , w1 , . . . , vn , wn .he0d , d(−
a ,−
w )i)
In order to apply the General Schema criterion,¦ h f (t1 ), t1 , . . . , f (tn ), tn i, ti = hed , ti
we refine the second-order algebraic theory FOLD
hence we haveto the second-order rewrite rule FOLDr. The Gen−→→f (d(−
a , t )) = ederal Schema in [3] is formulated for a framework
meaning that f satisfies the specification. We useof rewrite rules called inductive datatype systems,
this representation of primitive recursion in §7.
whose second-order fragment is essentially the sameas the present formulation given in §2. Minor differences are adapted as follows.
Remark 4.3 If ed constrains only recursive callsof the forms f (ti ), it is merely a pattern of struc(i) The target of function symbols must be a sintural recursion, so it can be implemented by foldgle (not necessary base) type in an inducusing the structure v.e0 where all the recursive calls
tive datatype system. Hence we introduce thef (ti ) in ed are abstracted to v as Example 4.2. product type constructor ×, assume that b1 ×b2

5 Strongly Normalising Computation
Rules for FOLD
We expect that FOLD provides strongly normalising computation rules. An immediate idea is toregard 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 ofequations in FOLD are not decreasing in most axioms. So, assigning some “measure” to the rules
in FOLDr that is strictly decreasing is difficult foris again a base type in the sense of §2. 2, anduse it for the target type.
(ii) Instead of a term x1 , . . . , xn .t of sort
a1 , . . . , an → b in a second-order algebraic theory, we use x1 . · · · .xn .t of type a1 → · · · →→an → b. Now the abbreviation −x .t denotes
x1 . · · · .xn .t.
The General Schema requires a notion of strictly
positivity of constructors.

Definition 5.1 ( [3]) Formally, a constructor is a→function symbol f : −α → σ which does not occur at the root symbol of the left-hand side of any
rewrite rule. The set of all constructors defines a→preorder ≤B on B by τ ≤B σ if τ occurs in −α for a−→constructor f : α → σ. Let =B be the equivalence
relation generated by ≤B . An (inductive) type σis strictly positive if for any type τ s.t. τ =B σ, τdoes not occur at a negative position of the type ofa constructor c for σ.
Crucially, the constructors used in FOLD are notstrictly positive, as cy and ¦ involve a negative occurrence of c in (c → c). We can overcome thisproblem by modifying the type (c → c) to a restricted (Varc → c), where Varc 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:h−, · · · , −i
cy
v
−¦−

: c1 , . . . , cn → c1 × . . . × cn ,−−→: (Varc → c) → c,
: Varc → c,−−→
: (Vara → c), a1 × · · · × an → c,

where c’s and a’s are base types of the inductive
datatype system (which may be product types),−−→
Vara → c is short for Vara1 → · · · → Varan → c.
The type of fold is now
−−−→
−−−→
foldcb : (Vara1 → b), . . . , (Varak → b),
m
- b,
(Varm
c → c), Varb
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 [11].
The General Schema has been improved after
publishing [3]. We use an improvement consideredin [4]. The condition (4) of the set Acc(v) of accessible subterms in Definition 3 of [3] can be replacedwith the following condition:(4’) Let ui be a term of type τ i for each i = 1, . . . , n.
If Acc(v) 3 f (u1 , . . . , un ) is of a base type b,
and b (possibly) occurs positively in type τ i , thenui ∈ Acc(v).
This version of the General Schema is more suitablefor our purpose.
5. 2 Second-order rewrite system FOLDr
We now describe how to refine the second-orderalgebraic theory FOLD to the second-order rewrite

rules FOLDr given in Fig. 7. For the axioms (4)and (8) in FOLD are refined to (4r)(8r) in FOLDr
by making explicit the superscripts of cy. Then we
restrict the rule (4) is only for cy1 and any othercyk with k ≥ 2 can now be decomposed by (8r).
Note that the superscript of cy in (8r) indicates thelength of the tuple argument (cf. §2. 1). Such a superscript indicating an invariant of the arguments
is similar to the idea of higher-order semantic labelling [24], but here we just make the existing superscript explicit rather than labelling.
The axiom (11) in FOLD involves a metaapplication at the right-hand side, which performs→
general substitution of terms for variables −y of base→types. But in FOLDr, since bound variables −y areof the types Varb1 , . . . , Varbn , the meta-application
can only replace variables of types Varb1 , . . . , Varbn
with variables of the same types. Therefore, instead of using meta-application, we implement a
more concrete substitution operation of terms as(11r),(12r) in FOLDr. These rules are sound byconstruction.
We define the relation →FOLDr on terms by the
relation generated by the second-order equational
logic Fig. 3 without using (Ax2),(Ref) and (Tra)rules. “One-step rewriting” is equational reasoning without using symmetry, reflexivity and transitivity. By construction, we immediately see thatthe rewrite system FOLDr correctly implements thesecond-order algebraic theory FOLD.
0
ˇ0
Proposition 5.2 If t →+FOLDr t then ť = t isderivable from FOLD without using (Ax2),(Ref )and (Tra), where ť, tˇ0 recovers the original terms
t, t0 by stripping the constructor v.

Theorem 5.3 The second-order rewrite system
FOLDr is strongly normalising.
Proof. FOLDr fits into the General Schema using
the well-founded orderfold > cym > cyn > ¦ > cy1 , any other constructors
where natural numbers m > n > 1. Namely, theabove order is compatible with the function calldependency in the rules. For example, in the rule(3r), the root of rhs is h−, −i, which is smaller than
the root in lhs, fold. A recursive call of fold occurs→→
with the argument −y .s[−y ], which is “structurally
smaller” than (more precisely, a covered subterm→→→[3] of) an argument −y . hs[−y ], t[−y ]i of lhs.
We check other rules similarly, i.e., for each rulel → r, l is in the computable closure of r. Hence it
is compatible with the General Schema. We havestrong normalisation of FOLDr.

Remark 5.4 This strong normalisation result isvery general. Not only ensuring termination of→.e , . . . , −computation of foldcb ( −xx→
1 1
m .em , t ) for−→
closed terms e , t (which is an expected result by
the semantics characterisation), the result ensures→.e , . . . , −−→ −→that any term foldcb ( −xx→
1 1
m .em , y . t ; y ) involving possibly(i) multiple fold’s, or even nested fold’s and(ii) free variables (i.e. e and t can be open terms)
is strongly normalising without imposing any reduction strategy. For (i), consider the situationthat one defines a function which calls other functions. Since it this paper, our methodology is thatany function on cyclic datatypes is defined using
fold, this situation is realised using fold involving
other fold’s. 

6 Church-Rosser modulo Bisimulationof FOLDrIn this section, we investigate another important
rewriting property, confluence and related properties of the rewrite rules FOLDr. A main reason toconsider these is to obtain decidability of the equational theory generated by AxCy, AxBr and FOLD.
See Remark 6.8. SN of FOLDr established in theprevious section also plays important roles to establish both confluence and Church-Rosser modulo. 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 meancy(x. v(x)).
Notation 6.1 Hereafter, we write simply → forthe rewrite relation →FOLDr . We write →∗ for thereflexive transitive closure, →+ for the transitive
closure, and ← for the inverse of →. We define↔ , → ∪ ←.
6. 1 Confluence on plain terms
First we consider confluence on terms without
any quotient.
Proposition 6.2 The relation → is weakly conflu-

ent.
Proof. Since every critical pair in FOLDr is joinable, it is weakly confluent [32].
Corollary 6.3 The relation → is confluent.
Proof. Since FOLDr is strongly normalising, byNewmann’s lemma [29] [2], we have confluence. Note that this result does not contradict known
counterexamples to confluence of graph rewriting
systems [1], [27]. Counterexamples to confluence in[1] use the fixed point law as a rewrite rule, while
our FOLDr does not have the fixed point law.
6. 2 Normal forms
Since FOLDr is SN and confluent, we have thefollowing.
Corollary 6.4 The normal form of a term by
rewriting with FOLDr is unique.
We write nf(t) for the unique normal form of t,
and write t →! t0 if t →∗ t0 = nf(t). We analyse
the structure of normal forms.
−→−→
Lemma 6.5 If u is of type b where n = | b | > 1,
then nf(u) is of the form ht1 , . . . , tn i.
Proof. A possible term t of such a type is either
ht1 , . . . , tn i or cym+k (hs, ti) with n = m + k. For
the latter case, applying (Bekic̆), cym+k (hs, ti) becomes a tuple involving cym (s), cyn (t) and ¦. The¦ is consumed by (11r)(12r), and applying (Bekic̆)repeatedly the subterms cym (s), cyk (t) finally become cy1 -terms. Hence the normal form of t is atuple.
We define the following classes of terms (d ∈ Σcon ):- Quasi-values−→
t ::= y | d( t ) | cy1 (x.t) | ht1 , t2 i→.t , . . . , −−→ −→| h i | fold(−x
x→
1 1
m .tm , y . t ; y )- Values−→t ::= y | d( t ) | cy1 (x.t) | ht1 , t2 i | h i−→ ` e : c, . . . , x−→ `Proposition 6.6 Suppose x
11m→.e , . . . , −→.e .
em : c and define e , −
x
x
1 1
m m
−−→
→
(i) If y : b ` t: −c is a value, then→→nf( fold(e, −y .t ; −y ) ) is a value.
−→→→(ii) If Γ ` t : c then nf( fold(e, −y .t ; −y ) ) is aquasi-value.
Note that t may contain free variables taken→from Γ, which are different from −y.
Proof. By induction of the typing derivations. 
By construction, fold is a total function (cf.
(4)). Its syntactic implementation is the rewrite
system FOLDr. Prop. 6.6 (i) shows that fold-termwith FOLDr actually reflects the semantic totality.
Moreover, Prop. 6.6 (ii) covers a more general situation than the semantic totality, where t can involve
nested or multiple fold, and variables. Importantly,
the left-hand sides of rewrite system FOLDr lackthe case→→fold(e, −y. x ; −y)−→where x is not in y . Namely, it is a normal form.
Hence we put this form into quasi-values.
6. 3 Church-Rosser modulo ∼Another important rewriting property is ChurchRosser modulo equivalence relation [29] [40]. For anequivalence relation ∼, we writes ↓∼ tif ∃s0 , t0 ∈ A. s →∗ s0 & t →∗ t0 implies s0 ∼ t0 .
A relation → is Church-Rosser modulo ∼(CR∼ ) if s (∼ ∪ ↔)∗ t implies s ↓∼ t. In diagram,s (∼ ∪ ↔)∗ t
∗

∗

?

?

s0

∼

(5)

t0

Now we take ∼ to be the equivalence relation
generated by AxCy ∪ AxBr, i.e. bisimulation. We
first state a fundamental property.
−−→→
Proposition 6.7 For z : b, Γ ` s
: −
c and
−−→
−
→
−
→
z : b, Γ ` t : c , If s ∼ t then fold( e , x1 :→→b1 , . . . , xn : bn. s; −x ) ↓∼ fold(−e , x 1 : b1 , . . . , x n :−→bn. t; x ) where Γ = x1 : b1 , . . . , xn : bn .
Proof. Since FOLD is a faithful implementation of
the characterisation (1) by Prop. 4.1, fold preserves→
bisimilarity. Note that to handle free variables −z of−→types b , we regard these as constants interpreted→
as themselves −z in computing with fold.
Remark 6.8 (On decidability of equational

theory) CR∼ is a desirable property, because thediagram (5) can be read as a proof method ofs (∼ ∪ ↔)∗ t, which is first normalising terms s, t
by FOLDr and then comparing them by ∼. Thisis meaningful because → is SN and has the uniquenormal form property, and ∼ is decidable. Hence
this gives a decidable proof method for the equational theory generated by FOLDr, AxCy and AxBr.



Unfortunately, CR∼ does not hold on unrestricted terms. For example, letting e , (l, t. 2 :: t),
we have the situation in Fig 8, which violates CR∼ .
A waved line in the diagram denotes ∼.
A crucial point is that cy(x.1 :: fold(e, x)) involves
a normal form fold(e, x), where x is bound by abinder placed upward. There are three possibilities
that such a bound variable x appears:→→→(a) cy(−y .C[ fold(e, −z . x; −z ) ])−→−→−→(b) ( y .C[ fold(e, z . x; z ) ]) ◦ t
−
→ →
→
→
(c) fold( d , −y .C[ fold(e, −z . x; −z )) ])−→
where x is taken from y and C is a context which→→
does not involve the forms cy(−y . · · · ), (−y .···) ◦→t, fold(e, −y . · · · ). The cases (b) and (c) are no problem, i.e., they do not fall into a situation as the diagram (6). The only problematic case is (a). Hence,
we exclude such terms from consideration.
Definition 6.9 Given a term t, if nf(t) has a subterm of the form
→
→
→
cy(−
y .C[ fold(e, −z . s; −z )) ]),
where s involves a variable x taken from bound vari→ables −y of cy, then we call t a bad term. We assume that a c-structure e is always closed terms to
avoid similar problems. We define a set of non-bad
terms as follows:→
T , {t | Γ ` t : −c with t is not bad,and every arguments e of fold are closed terms }.

Proposition 6.10 The set T is closed under the
FOLDr rewrite relation → and one step applicationof an axiom in AxCy and AxBr.
Proof. If t ∈ T then t → t0 ∈ T because FOLDr
does not produce a bad term if t does not involvea 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 substitutionof terms for variables are always capture-avoiding.

1 :: fold(e, cy(x.1:: fold(e,
x)))
k
)i

kk
kkk
kkk
k
k
ku kk

)i )i )i(4r)(5r)

6∼

1 :: cy(x.2 :: fold(e, fold(e, x)))(6))i )i (fix))i )i )icy(x.1 :: fold(e, x))
6

6

²
²
図8

Failure of CR∼



Note that a bad term does not simply mean thatfold does not appear under cy. A term where foldappears under cy is allowed, when s does not in→volve the bound variables −y of cy. For example,
the right-hand side of the rule (4r) in FOLDr is notbad.
We prove CR∼ on T by employing a criterion by
Huet [29]. We define the following.
(i) → is locally confluent modulo ∼b & a → c implies b ↓∼ c .
(ii) → is locally coherent modulo ∼b & a ∼ c implies b ↓∼ c.

if a →
if a →We define → / ∼ , (∼ · → · ∼) for the rewriting
modulo equivalence relation.
Theorem 6.11 (Huet [29])(i) If → is SN, locally confluent modulo ∼, andlocally coherent modulo ∼, then → is CR∼ .
(ii) Let `a be a symmetric relation such that ∼ =`a∗ . If the relation →/∼ is SN, → is locallyconfluent modulo ∼ and locally coherent modulo `a, then → is CR∼ .
Among the above two criteria of establishingCR∼ , (ii) is simpler to check than (i). In our situation, the relation `a may be taken to be a one-step
application of an instance of axiom of AxCy ∪ AxBr,
then local coherence modulo `a can be establishedjust by checking possible peaks r ← s `a w.
However, in the case of FOLDr, the rewriting
modulo bisimulation →/∼ is not SN because (dinat) can copy a redex inside cy. For example, sincecy(x.x) is a redex by (10r), we havecy(y.cy(x.x)) ∼ (y.cy(x.x)) ¦ cy(y.cy(x.x))→ (y.[ ]) ¦ cy(y.cy(x.x))∼ (y.[ ]) ¦ (y.cy(x.x)) ¦ cy(y.cy(x.x))→ (y.[ ]) ¦ (y.[ ]) ¦ cy(y.cy(x.x)) ∼ · · · .
Hence, to show CR∼ , we must use the criterion

Thm. 6.11 (i). This requires to establish local coherence modulo ∼, which means we need to check
all possible peaks of the form¤s¤ ] ]
¤¤
]
¤
]
¤
r¤¢
t

This situation is complex, because ∼ is not only
one-step application of an axiom. We need to analyse various properties of the bisimulation ∼, such astransitivity of ∼ and closedness under substitution
and contexts, etc. Fortunately, we have already an
algebraic characterisation of the bisimulation:
→
s∼t
iff
Γ `s=t :−c is derivable
by Prop. 2.2. Identifying these two, this enable
us to use induction on the proof of s = t to covervarious properties of the bisimulation s ∼ t in full.
Proposition 6.12 FOLDr is locally coherent modulo ∼ on T .
Proof. We prove the following proposition:→Γ `s=t :−c is derivable ⇒ if s has a
one-step reduct r ← s then r ↓∼ t,where all terms used in the proposition are in T .
We prove by induction on the proof of s = t using
the cartesian second-order equational logic (Fig. 3).
•(Ref) Obvious.

•(Ax1)(Ax2) Let s = t be an axiom of AxCy ∪AxBr. We check that for every substitution θ
for metavariables such that sθ has a reduct r,
we have r ↓∼ t. This is done by examining
all possible unifiers between a subterm of s andthe left-hand side of a rule in FOLDr. All cases
are routine. One exception is the case (dinat),which will produce the situation (6). But wehave restricted terms as T , hence this situation
is now excluded.

•(Fun) and (OSub) By induction hypothesis(I.H.) and the fact that rewriting and equational
reasoning are closed under contexts and substitutions for variables.

•(Tra) Suppose r ← s ∼ t and it is derived froms ∼ w and w ∼ t. By I.H., r ↓∼ w.
- If w is a normal form, then the situation isdepicted as the following diagram, which meansr ↓∼ t.
s /o /o /o w /o /o /o tro∗0

r²0 /o /o /o /o /o /o /o w²- If there exists a reduct r0 ← w, by I.H., wehave r0 ↓∼ t. Then, we show the following:r ← s ∼ w & r0 ← w ∼ t & r ↓∼ w⇒
r ↓∼ t& r 0 ↓∼ t

We name the assumptions of the above proposition as (A). We have the following:ros /o /o o/ ¡w /o /o o/ t
¡

¡
∗¡
¡
¡
¡
²
r0² o/ /o o/ ·Ä¡r0 (A)
∗

∗

(A)

(P)

∗

·² /o /o o/ ·² o

O

∗

CR ∗
∗

²
·² /o o/ n/o nt0nO (P) nn∗nnn
O nnnn·wnwhere CR denotes confluence on plain terms(Cor. 6.3) and (P) denotes an application of
the following proposition
P : ∀s, t, s0 , t0 ∈ T . s →∗ s0⇒ ( s ∼ t & t →∗ t0 ⇒ s0 ∼ t0 )which is established by induction on the lengthof rewrites s →∗ s0 . The diagram above actuallyshows r ↓∼ t.

Theorem 6.13 FOLDr is CR∼ on T .
Proof. We have established that FOLDr is locallycoherent modulo ∼ on T , SN and weakly confluent
on all well-typed terms. Therefore, → is weakly
confluent on T , which also implies local confluence
modulo ∼ on T . By Thm. 6.11 (i), we have CR∼
on T .
Hence, as noted in Remark 6.8, we have a remarkable result.
Corollary 6.14 The equational theory generated
by FOLDr, AxCy and AxBr on terms of T is decidable.
Remark 6.15 We introduced the notion of badterms to establish the property CR∼ . Another explanation of necessity of exclusion of bad terms isthat a bad term generates a non-rational tree. For
example, consider a function incrementing each element of a CNat-list defined bymapinc(t) = fold([ ], `.s.` + 1 :: s, t)This function itself is no problem. For example,
applying mapinc to the cyclic list of 1, we have thecyclic list of 2.
mapinc(cy(x. 1:: x))→ cy(x. mapinc(x. 1:: x; x))→ cy(x. 2 :: mapinc(x; x))→ cy(x. 2:: x)
But consider a bad term cy(z.1 :: mapinc(z)). Observe that it is a normal form with respect to
FOLDr, because mapinc(z) cannot be rewritten.
But using the cartesian second-order equational
logic with AxCy (especially (fix)) and FOLD, we
can reason ascy(z.1 :: mapinc(z))= 1 :: mapinc(cy(z.1 :: mapinc(z)))= 1 :: mapinc(1 :: mapinc(cy(z.1 :: mapinc(z)))))= 1 :: (2 :: mapinc(mapinc(cy(z.1 :: mapinc(z)))))= 1 :: 2 :: 3 :: · · ·which means that it corresponds to a non-rational
tree. Since the function fold is a map between rational trees, we excluded the bad term from T .
Note that a bad term cy(z.1 :: mapinc(z)) can be
represented in Haskell as a recursive definition oflist
z = 1:map (1+) z
which is a well-known lazy programming technique.
It looks defining a cyclic data, but actually defining
an acyclic infinite data [14], [21]. We could capture this phenomenon from a different viewpoint,
namely from the viewpoint of rewriting. From theview of functinal programming, bad terms generatate acyclic infinite data, and from the view ofrewriting, bad terms are terms preventing CR∼ . 

7 Computing by Fold on
Cyclic Datatypes
In this section, we demonstrate fold computation
on cyclic data by several examples.
Example 7.1 We consider the emptiness check of
cyclic sharing trees. It means to check whether agiven closed term is bisimilar to [ ]. This is not justto check whether a given term is syntactically [ ].

For example, is cy(x.x) + cy(x.[ ] + x) empty?
This requires certain computation, which we willdefine. First, we define a (cyclic) boolean datatype
having the operation ∧, satisfying the axioms AxBr.
ctype Bool where
true : Boolfalse : Bool
∧ : Bool,Bool → Boolwith axioms AxCy,AxBr(true,∧)

ously as follows:
if then else : Bool,b, b → b
spec if true then t else e = t
if false then t else e = e
Hence we can define it simply:
fun if p then t else e = fold (t,e) p

Example 7.3 As an example of primitive recursion on cyclic datatypes mentioned in §4. 2, we conisEmpty : CTree → Boolsider the tail of a cyclic list, which we call ctail.
spec isEmpty([ ])= trueIt should satisfy the specification below right. But
isEmpty(f (t)) = false
how to define the tail of a cy-term is not immediisEmpty(s + t) = isEmpty(s) ∧ isEmpty(t) ately clear. For example, what should be the resultof ctail (cy(x.1::2::x))? This case may need unfun isEmpty(t) = fold (x.true, x.false,folding of cycle as in [21]. A naive unfolding by
x.y.x ∧ y) t
using the fixed point law cy(x.t) = t [cy(x.t)/x] violates strong normalisation because it copies theoriginal term. It actually increases complexity.
We define isEmpty by fold. Examples of computation are as follows, where the cycle cleaning laws inctail : CList → CList
FOLDr are crucial.
spec ctail ([ ])= []isEmpty(cy(x.x) + cy(x.[ ] +x))
ctail (k :: t)= t→+ isEmpty([ ] +cy(x.x))
ctail (cy(x. t))= ??
→ isEmpty([ ]+[ ])Rather than the fixed point law, we chose another→+ true ∧ true → true
important principle of cyclic structures known as
Bekic̆ law, given by the axiom (Bekic̆) in AxCy or(8r) in FOLDr.
isEmpty( cy(xCtree .cy(w.x)) )→ cy(xBool . isEmpty(x.cy(w.x); x))→ cy(xBool . cy( w.isEmpty(x.w.x; x,w) ))→ cy(xBool . cy( w.x ))→ cy(xBool .x) → trues

(Beki )ts

ts

isEmpty(cy(x. a(cy(y.y+y)) + cy(w.x)))→+ isEmpty(cy(x. a([ ]) + x))→ isEmpty(a([ ])) → false
The example isEmpty(cy(x.x) + cy(x.[ ] +x))
is essentially checking null-ability of a grammar [7],which has pointed as a difficult problem for computing with cyclic data in [36]. Our rewrite system FOLDr successfully computes it in a principledmanner (i.e. without any special treatment).

Example 7.2 We show how to define the if-thenelse statement by fold. The specification is obvi-

It says that the fixed point of a pair can beobtained by computing the fixed point of each ofits components independently and composing themsuitably (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. We define ctail byfold.
fun ctail(t)= π 1 ¦ fold (<[],[]>, k,x,y.<y, k :: y>) t
ctail(cy(x.1 :: 2 :: x))→+ π 1 ¦ cy(x,y. <2 :: y, 1 :: 2 :: y>)→+ π 1 ¦ < cy(x.2 :: cy(y.1 :: 2 :: y)),cy(y.1 :: 2 :: y)>→ cy(x.2 :: cy(y.1 :: 2 :: y))→ 2 :: cy(y.1 :: 2 :: y) (Normal form)

Note that the above normal form does not meana head normal form and we do not rely on lazyevaluation. The highlighted step uses Bekic̆ law.

Example 7.4 We define the datatype of cyclic
strings consisting of a, b, the empty string ε, andthe choice operator “|”.
ctype CString wherea : CString → CStringb : CString → CString
ε : CString| : CString,CString → CStringwith 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,
aa?( b(a(a(b(ε)))) )aa?( b(b(ε))
aa?( b(ε)|a(a(ε)) )

→!
→!
→!

true
false
true

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)) )aa?( b(cy(x.a(b(a(x))))) )

→!
→!

true
true

We now specify aa? by using the function head-a?
which checks whether the head is a.
head-a? : CString → ABoolspec head-a?(a(t)) = truehead-a?(b(t)) = false

aa? : CString → ABoolspec aa?(a(t)) = head-a?(t)aa?(b(t)) = aa?(t)aa?( ε ) = falseaa?(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 theunit false, because the specification of aa? requires that the unit ε (resp. the multiplication “|”)of CString is mapped to the unit false (resp. themultiplication “∨”) of the target type.
ctype ABool where
true : ABoolfalse : ABool∨: ABool,ABool → ABool
with axioms AxCy,AxBr(false,∨)Then we can define the functions head-a? and aa?
by fold.
fun head-a?(t)= fold (x.true,x.false,false,x.y.x∨y) t
fun aa?(t)= π 1 ¦ fold (v,w.<head-a?(w),a(w)>,v,w.<v,b(w)><false,ε>,v1 .w1 .v2 .w2 .<v1 ∨v2 ,w1 |w2 >) t
We demonstrate how FOLDr correctly computes
aa?(cy(x.a(x))) →! true.
A One may think that it needs expansion of theinner term of cy. We show that the rewrite system FOLDr 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)>,...).
aa?(cy(x.a(x))) = π 1 ¦ folde cy(x.a(x))→ π 1 ¦ cy(v.w.(folde a(v); v,w))→+ π 1 ¦ <cy(v.head-a?(cy(w.a(w)))),
cy(w.a(w))>→+ head-a?(cy(w.a(w))→ cy(w.head-a?(w.a(w);w) )→+ cy(w.true) → true
Again, the highlighted step uses Bekic̆ law. Moreover, we expectaa?(cy(x.b(x))) →! false
without falling into non-termination. This is actually obtained without any special treatment.
aa?(cy(x.b(x))) = π 1 ¦ folde cy(x.b(x))→ π 1 ¦ cy(v.w. (folde b(v); v,w))→+ π 1 ¦ <cy(v.v),cy(w.b(w))>→+ cy(vABool .v) → false
A crucial point is that since we chose the target
type as ABool, the rule (10r) in FOLDr rewritescy(vABool .v) to false, which is the unit of ABool.
If we chose the target type as Bool in Example 7.1,
this become an incorrect result true. But the specification forced us to choose ABool.

Example 7.5 This example shows that our cyclic

datatype has ability to express graphs. The graphshown 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 nodesof three persons. This is represented as a term

In this paper, we have developped foundations ofcyclic datatypes and computation:(a.b.c.a+b+c)¦ cy(a.b.c.<name("alice"),
name("bob")+knows(a),name("carol")+knows(a)+knows(b)>)[II] Complete equational axioms for bisimulationof cyclic data (Fig. 4)

which we call g. The term g is of type FriendGraphdefined as follows.

8 Summary and Related Work[I] Syntax and type system supporting algebraic
datatypes with cycle and sharing constructs(§2)[III] Algebraic theory FOLD of fold on cyclic
datatypes and its strongly normalising rewrite
system FOLDr (Fig. 6, Fig. 7) (§4, §5), whichis Church-Rosser modulo bisimulation (§6)

ctype FriendGraph whereknows : FriendGraph → FriendGraph[IV] The framework that supports [I]-[III] based onname : String → FriendGraph
cartesian second-order algebraic theory (§2. 1)[ ] : FriendGraphand iteration category (§3). The numbered+ : FriendGraph,FriendGraph → FriendGraph
items [I]-[III] in Fig. 1 in Introduction are inwith axioms AxCy,AxBr([ ],+)
stances of these results.

+
alice

bob

carol
knows

We define a function collect that collects allnames in a graph as a name list of type Names.

ctype Names where
nm : String → Names[ ] : Names+ : Names,Names → Names
with axioms AxCy,AxBr([ ],+)
collect : FriendGraph → Names
spec collect (knows(t)) = collect(t)collect (name(p)) = nm(p)fun collect t= π 1 ¦ folde (x,y.<x,knows(y)>,x,y.<nm(y),name(y)>,<[ ],[ ]>,v1 .w1 .v2 .w2 .<v1 +v2 ,w1 +w2 >) t
Then we collect certainly all names by FOLDr
as follows, where folde is short for fold(x,y.<x,knows(y)>, x,y.<nm(y),name(y)>,...).
An example of rewrite steps is given in Fig. 9.

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 languagethat realises the program codes described in thispaper is left for a future work.
Related work.
There has been various work
to deal with graph computation and cyclic data
structures in functional programming and foundational calculi including [14] [36] [8] [28] [31] ?[] ?[]. Several work [14] [36] [31] relies on lazy evaluation todeal with cycles. The present paper is different inthis respect. We do not assume 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 a proof assistance requiring terminating functions, such as Coq
or Agda.
Foundational graph rewriting calculi, such as
equational term graph rewriting systems [1], aregeneral frameworks of graph computation. The foldon 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
fold on them by regarding fold as a structure preserving map, rather than unrestricted rewriting. It
was a key to obtain SN and CR∼ of FOLDr. We also
hope that it will be useful for further optimisationsuch as the fold fusion based on semantics as donein [26]. The general study of graph rewriting was
also important for our study at the foundational

collect g = π 1 ¦ folde g→ π 1 ¦ (a.a’.b.b’.c.c’.<a+b+c,a’+b’+c’>) ¦ (cy(a.a’.b.b’.c.c’.
<folde(a.b.c.name("alice")), folde(a.b.c.name("bob")+knows(a)),
folde(a.b.c.name("carol")+knows(a)+knows(b)>)))→+ π 1 ¦ (a.a’.b.b’.c.c’.<a+b+c,a’+b’+c’>) ¦ (cy(a.a’.b.b’.c.c’.
< <nm("alice"),name("alice")>, <nm("bob"),name("bob")>, <nm("carol"),name("carol")> >)→+ nm("alice")+nm("bob")+nm("carol")
図9

An example of rewrite steps

level. The unit “[ ]” of branching in AxBr corresponds to the black hole constant “•” consideredin [1], due to [6]. This observation has been used
to give an effective operational semantics of graphtransformation in [31].
In [21] ?[], the present author aimed to capture
unique representations of cyclic sharing data structures (without any quotient) in order to obtain an
efficient functional programming concept. The approach taken in this paper is different. We have assumed the axioms AxCy and AxBr to equate bisimilar graphs. The point is that bisimulation ongraphs can be efficiently decidable [12], thus now
we regard that uniqueness of representation is notquite serious.
In [25] [26], the author and collaborators gave algebraic and categorical semantics of graph transformation language UnCAL [8] [28] using iteration theories [6]. The graph data of UnCAL corresponds tocyclic sharing trees of type CTree in the present paper. 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 advanced one step further by developing a suitablealgebraic framework that captures datatypes supporting cycles and sharing. We have proved important rewriting properties, strong normalisation
and Church-Rosser modulo bisimulation. We usedrewriting techniques to them, namely, the General
Schema [3] for strong normalisation (not merely
termination of a particular computation strategy
or algorithm) of fold and Huet’s abstract theory for
rewriting modulo equivalence relation. Combining
these, we obtained a remarkable result on decidability of the equational theory generated by FOLDr,
AxCy and AxBr. These precise rewriting analysesof the fold computation on cyclic datatypes modulo
bisimulation have not been pursued so far, hence
these are completely new results.

Acknowledgments. I am grateful to Kazutaka
Matsuda and Kazuyuki Asada for various discussions about calculi and programming languages
about graphs and cyclic structures, and Frédéric
Blanqui for clarifying some details of the General
Schema.
参 考 文 献[ 1 ] Z. M. Ariola and J. W. Klop. Equational term
graph rewriting. Fundam. Inform., 26(3/4):207–
240, 1996.
[ 2 ] F. Baader and T. Nipkow. Term Rewriting and
All That. Cambridge University Press, 1998.
[ 3 ] F. Blanqui. Termination and confluence of
higher-order rewrite systems. In Rewriting Techniques and Application (RTA 2000), LNCS 1833,
pages 47–61. Springer, 2000.
[ 4 ] F. Blanqui. Termination of rewrite relations on
λ-terms based on Girard’s notion of reducibility.
Theor. Comput. Sci., 611:50–86, 2016.
[ 5 ] F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive data type systems. Theoretical Computer
Science, 272:41–68, 2002.
[ 6 ] S. L. Bloom and Z. Ésik. Iteration Theories - The Equational Logic of Iterative Processes.
EATCS Monographs on Theoretical Computer Science. Springer, 1993.
[ 7 ] J. A. Brzozowski. Derivatives of regular expressions. J. ACM, 11, 1964.
[ 8 ] P. Buneman, M. F. Fernandez, and D. Suciu.
UnQL: A query language and algebra for semistructured data based on structural recursion. VLDB J.,
9(1):76–110, 2000.
[ 9 ] C. Calcagno, P. Gardner, and U. Zarfaty. Context logic and tree update. In Proc. of POPL’05,
pages 271–282, 2005.
[10] T. Coquand. Pattern matching with dependent
types. In Proc. of the 3rd Work. on Types for Proofs
and Programs, 1992.
[11] J. Despeyroux, A. Felty, and A. Hirschowitz.
Higher-order abstract syntax in Coq. In Typed
Lambda Calculi and Applications, LNCS 902, pages
124–138, 1995.
[12] A. Dovier, C. Piazza, and A. Policriti. An efficient algorithm for computing bisimulation equivalence. Theoretical Computer Science, 311:221–256,

2004. Issues 1-3.
[13] Z. Ésik. Axiomatizing iteration categories. Acta
Cybernetica, 14:65–82, 1999.
[14] L. Fegaras and T. Sheard. Revisiting catamorphisms over datatypes with embedded functions (or,programs from outer space). In POPL’96, pages
284–294, 1996.
[15] M. Fiore. Second-order and dependently-sorted
abstract syntax. In Proc. of LICS’08, pages 57–68,
2008.
[16] M. Fiore and C.-K. Hur. Second-order equational logic. In Proc. of CSL’10, LNCS 6247, pages
320–335, 2010.
[17] M. Fiore and O. Mahmoud. Second-order algebraic theories. In Proc. of MFCS’10, LNCS 6281,
pages 368–380, 2010.
[18] M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proc. of LICS’99, pages
193–202, 1999.
[19] M. Fiore and S. Staton. Substitution, jumps,
and algebraic effects. In Proc. of LICS’14, 2014.
[20] M. P. Fiore and M. D. Campos. The algebraof directed acyclic graphs. In Computation, Logic,
Games, and Quantum Foundations, LNCS 7860,
pages 37–51, 2013.
[21] N. Ghani, M. Hamana, T. Uustalu, and V. Vene.
Representing cyclic structures as nested datatypes.
In Proceedings of Trends in Functional Programming, pages 173–188, 2006.
[22] M. Hamana. Free Σ-monoids: A higher-ordersyntax with metavariables. In Proc. of APLAS’04,
LNCS 3302, pages 348–363, 2004.
[23] M. Hamana. Universal algebra for termination ofhigher-order rewriting. In Proc. of RTA’05, LNCS
3467, pages 135–149, 2005.
[24] M. Hamana. Higher-order semantic labelling for
inductive datatype systems. In Proc. of PPDP’07,
pages 97–108. ACM Press, 2007.
[25] M. Hamana. Iteration algebras for UnQL graphs
and completeness for bisimulation. In Proc. of Fixed
Points in Computer Science (FICS’15), Electronic
Proceedings in Theoretical Computer Science 191,
pages 75–89, 2015.
[26] M. Hamana, K. Matsuda, and K. Asada. The
algebra of recursive graph transformation language
UnCAL: Complete axiomatisation and iteration categorical semantics. submitted.
[27] M. Hasegawa. Models of Sharing Graphs: A

Categorical Semantics of let and letrec. PhD thesis,
University of Edinburgh, 1997.
[28] S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, and K. Nakano. Bidirectionalizing graphtransformations. In Proc. of ICFP 2010, pages 205–
216, 2010.
[29] G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems.
Journal of ACM, 27(4):797–821, 1980.
[30] A. Joyal, R. Street, and D. Verity. Traced
monoidal categories. Mathematical Proceedings of
the Cambridge Philosophical Society, 119(3):447–
468, 1996.
[31] K. Matsuda and K. Asada. Graph transformation as graph reduction: A functional reformulationof graph-transformation language UnCAL. Technical Report GRACE-TR 2015-01, National Instituteof Informatics, January 2015.
[32] R. Mayr and T. Nipkow. Higher-order rewrite
systems and their confluence. Theor. Comput. Sci.,
192(1):3–29, 1998.
[33] L. G. L. T. Meertens. Paramorphisms. Formal
Asp. Comput., 4(5):413–424, 1992.
[34] E. Meijer, M. M. Fokkinga, and R. Paterson.
Functional programming with bananas, lenses, envelopes and barbed wire. In Proc of FPCA’91, pages
124–144, 1991.
[35] R. Milner. A complete inference system for aclass of regular behaviours. J. Comput. Syst. Sci.,
28(3):439–466, 1984.
[36] B. C.d.S. Oliveira and W. R. Cook. Functional
programming with structured graphs. In Proc. of
ICFP’12, pages 77–88, 2012.
[37] A. K. Simpson and G. D. Plotkin. Complete axioms for categorical fixed-point operators. In Proc.
of LICS’00, pages 30–41, 2000.
[38] S. Staton. An algebraic presentation of predicate
logic. In Proc. of FOSSACS 201, pages 401–417,
2013.
[39] S. Staton. Algebraic effects, linearity, and quantum programming languages. In Proc. of POPL’15,
pages 395–406, 2015.
[40] Terese. Term Rewriting Systems. Number 55 in
Cambridge Tracts in Theoretical Computer Science.
Cambridge University Press, 2003.
[41] G. Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993.