1

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

Makoto Hamana
Department of Computer Science,
Gunma University, Japan

FSCD’16
Porto University, Portuguese.

2Computing with Cyclic Datatypes
B Cyclic data structures in functional programming
B In Haskell, one can define a cyclic list byclist = 2:1:clist
B Why is this technique correct? — lazy evaluation
head clist

2

B Not completely safe
B E.g. what is the sum of all elements of clist?
sum clist

non-termination

B The “encoding” does not give complete understanding ofcyclic datatypes

3This Work
B Complete axiomatisation using– second-order algebraic theory [Fiore et al.’10]– iteration category [Bloom-Esik’93]
B Do not rely on lazy evaluation
B Strongly normalising fold combinator
B A framework for syntax and semantics of cyclic datatypes

4

Our Framework
ctype CList where[ ] : CList:: : CNat,CList → CListwith axioms AxCy
cy(x.2::1::x)
21clistSpecification
sum : CList → CNat
spec sum ([ ])= 0sum (k :: t) = plus(k, sum (t))
fun sum t = fold (0, k,x.plus(k,x)) t

ctype CNat where
0 : CNatS : CNat → CNatwith axioms AxCy

5Example“infinity”

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

1clistsum

[II]

SAxCy

S=Sequational theory
for bisimulation

fun sum t = fold (0, k,x.plus(k,x)) tsum(cy(x.S2 (0)::S(0):: x)) →+ cy(x.sum(x.S2 (0)::S(0)::x)@x)→+ cy(x.S(S(S(x))))B How to understand?
B Second-order equational logic and axioms AxCy
to equate cyclic dataB⇔decidable bisimulationS6

Cartesian Second-Order Algebraic Theory
B Base types a, b, c, . . .
B Signature Σ→−−→→−−→f : ( a1 → b1 ), . . . , (am → bm ) → c1 , . . . , cn .
B Metavariables (t, s, . . .) · · · variables of at most first-order−t:→a →b
B Variables · · · variables of order 0
B Syntax of meta-terms(Aczel [1978], Klop’s CRS [1980])

t ::= x | x.t | f (t1 , . . . , tn ) | t[t1 , . . . , tn ]

7Cyclic Datatypes
Default constructors−−−−h−, · · · , −i : (→c1 ), . . . , (→cn ) → →c1 , . . . , →cn−−−
Cycle constructor
cy : (→c →→c)→→c−−−−Composition¦ : (→a →→c ), →
a →→
c
Tuple

E.g.

cy(x.S(0)::x))

8

Axioms AxCy for Cycles(sub)−−(→y .t[→y ]) ¦ hs1 , . . . , sn i =(SP)−−h(→y .y1 ) ¦ t, . . . , (→y .yn ) ¦ ti =−−cy(→x .s[t[→x ]])(dinat)=t[s1 , . . . , sn ]t−−−−(→z .s[→z ]) ¦ cy(→z .t[s[→z ]])]→−→−→−bhcy(x.
(y.
t)¦cy(y .bs)),→−→−b, b(Bekic̆) cy( x , y . h ts i) =−−−−−b) ¦ cy(→cy(→y . (→x .bs) ¦ cy(→x . (→y .ty .bs))) i(CI)−cy(→y .ht[ρ1 ], . . . , t[ρm ]i) =hcy(y.t̃ ), . . . , cy(y.t̃ )iNote
B “cy” is a (Conway) parameterised fixed point operator(fix)−−cy(→x .s[→x ]) =−−−−(→z .s[→z ]) ¦ cy(→z .s[→z ]])9Example (1): Cyclic Lists modulo Bisimulation
B ctype CList where[ ] : CList:: : CNat,CList → CListwith axioms AxCy
B AxCy captures the intended meaning of cyclic listsAxCy

2

=AxCy

2cy(x.2 :: x) ==2

2 :: cy(x.2 :: x)=22

2

2 :: 2 :: cy(x.2 :: x)

10

Example (2): Cyclic Sharing Trees modulo Bisimulation
ctype CTree wheref : CTree → CTree(f =a,b,c,p,q,. . .)[ ] : CTree+ : CTree,CTree → CTreewith axioms AxCy,AxBr
+(A)

bc[]

[]b([])+c([])x(B)

aby(C)

bccb+[]

[]

[]

[]

+cxxpb([])+c([]) =+bbcpp

[]
[]
(sub)
(x.b(x)+c(x)) o p([]) = b(p([]))+c(p([]))[]+ccy(x.a(cy(y.b(c(x+y))))(F)+c([])+b([])

11

Axioms AxBr for branching(del)(unitL)(unitR)(assoc)(comm)(degen)cy(xc .t + x) =[] + tt + [](s + t) + u
s+tt+t==ttts + (t + u)=t+s=t+=tt=axiom (del)Prop. (Completeness for bisimulation) [H. FICS’15]
Γ ` s = t : CTree is derivable from AxCy and AxBr.
iff
if s and t are bisimilar.

12Categorical Semantics of Cyclic Datatypes
B Why categorical semantics? — to obtain fold combinator
B Categorical structure
Iteration category= traced cartesian category [Joyal et al.’96][Hasegawa-Hyland’97]+ Bloom-Ésik’s Commutative Identities axiom

B Reference
Bloom, Ésik. Iteration Theories, EATCS Monographs. 1993.

13Axioms AxCy
(sub)−−(→y .t[→y ]) ¦ hs1 , . . . , sn i =(SP)−−h(→y .y1 ) ¦ t, . . . , (→y .yn ) ¦ ti =−−cy(→x .s[t[→x ]])(dinat)=t[s1 , . . . , sn ]t−−−−(→z .s[→z ]) ¦ cy(→z .t[s[→z ]])]→−→−→
−bhcy(x.
(y.
t)¦cy(y .bs)),→−→−b, b(Bekic̆) cy( x , y . h ts i) =−−−−−b) ¦ cy(→cy(→y . (→x .bs) ¦ cy(→x . (→y .ty .bs))) i(CI)
where−cy(→y .ht[ρ1 ], . . . , t[ρm ]i) =−y,ρ is a permutation of →ihcy(y.t̃ ), . . . , cy(y.t̃ )it̃ = t[y, . . . , y]

14Categorical Semantics and Completeness−Thm. Γ ` s = t : →c is derivable from E iff
M[[s]]M=[[t]]CC holds for all iteration categories C and all(Σ, E)-structures in C.

Category Tm(E)B object: sequence of types b1 , . . . , bn−
B arrow: equivalence class [Γ ` t : →c ]E of judgments modulo
axioms E = AxCy ∪ AxBr

15Universality
Thm. For a (Σ, E)-structure M in an iteration category C,- C that
there exists a unique iteration functor ΨM : Tm(E)preserves (Σ, E)-structures.
Tm[[−]]U- Tm(E)½½½[[−]]M
½½ ΨM
½?=
½C

16

Extract “Fold” from Universality
Thm. For a (Σ, E)-structure M in an iteration category C,- C that
there exists a unique iteration functor ΨM : Tm(E)preserves (Σ, E)-structures.
[[−]]U- Tm(E) 3½½½[[−]]M
½½ ΨM
½?=
½Tm

Tm(E)

3

x1 : c, . . . , xn : c ` t : c?

x1 : b, . . . , xn : b ` u : b

B where the (Σ, E)-structure M interprets a type c as type b
B ΨM gives a translation from the cyclic datatype c to b(e.g. CList to CNat)
B Extract the law of fold by formalising ΨM17

Second-Order Algebraic Theory for fold−
→fold(E, y c−fold(E, →y−fold(E, →y−fold(E, →y−fold(E, →yyi )h i)−−
hs[→y ], t[→y ]i)

−
→
= yb
−
=→
y−
=→
y−
−−−cy(→x .t[→y ,→x ])) = →yyi−(for yi ∈ {→y })

hi
−
−−−
happ(fold(E, →ys[→y ]), →y ), app(fold(E, →y−−−−−−−cy(→x .app(fold(E, →y ,→xt[→y ,→x ]), →y ,→x ))−−t[→y ]), →y→−→− −−−−−−−−d( a , t1 [→y ], . . . , tn [→y ])) = →y(→x .e d [ a , →x ]) ¦ happ(fold(E, →yt1 [→y ]), →y−−−−→−−−−−−(→y .t[→y ]) ¦ s[→x ])= →xy .app(fold(E, →yt[→y ]), →y ) ¦ app(fold(E, →xs[→x]fold(E, x−−app(→xs[→x ], z , . . . , z1m)

= s[z1 , . . . , zm ]To obtain computation rules
B Include some theorems of AxCy and AxBr for simplification
B Orient equations

18

Second-Order Rewrite System FOLDr
Fold

−−→
fold(E, y Varc. v(yi ))−fold(E, →y . h i)−−→
→ y Varb. v(yi )−→→y. h i−−−fold(E, →y . hs[→y ], t[→y ]i)−−fold(E, →y . cy1 (x.t[→y , x]))

−
−
−
−
−
−
−
→→
y . hfold(E, →y . s[→y ])@→
y , fold(E, →y . t[→y ])@→
yi−
−
−
−
→→
y . cy1 (x.fold(E, →y , x. t[→y , x])@→y , x)→−→− −−−−−−−−−
fold(E, →y . d( a , t1 [→y ], . . . , tn [→y ])) → →y . (→x .ed [ a , →x ]) ¦ h fold(E, →y . t1 [→y ])@→
y , . . .i−−−−−−−−−−−−fold(E, →x. (→y .t[→y ]) ¦ s[→x ])→→x. (→y .fold(E, →y . t[→y ])@→y ) ¦ fold(E, →x. s[→x ])@→xBekic̆ and cycle cleaning−−b, bcym+n (→x ,→y. h ts i)−cy(→y . t)−−−b) ¦ cyn (→→ h cym (→x . (→y .ty .bs)),−−−−−b) ¦ cyn (→cyn (→y . (→x .bs) ¦ cym (→x . (→y .ty .bs)))i→tcy(x.v(x))→[ ]cy(x.t + v(x))→tComposition→−−(→y . v(y )) ¦ h s i

→ sii

→
−−
→. t [→− −→(→y . d(−x1 1 y , x1 ], . . .)) ¦ h s i−→−−−−→]) ¦ h→−−→ d(→x. (→y . t1 [→y ,−xs i, . . . , (→y . tn [→y ,−x→1n ]) ¦ h s i)

B Strongly normalising by [Blanqui RTA’00]’s the General Schema

19

Fixed point law
We do not include−−(fix) cy(→x .s[→x ]) →−−−−(→z .s[→z ]) ¦ cy(→z .s[→z ]])in the rewrite system FOLDr
But includes(Beki )
tsts

20

Example: Tail of Cyclic List
ctail
12ctail : CList → CList
spec ctail ([ ])= []ctail (k :: t)= t
ctail (cy(x. t))= ??

212

21

Example: Tail of Cyclic Listctail
122

ctail : CList → CList
spec ctail ([ ])= []ctail (k :: t)= tctail (cy(x. t))= ??

12

I Primitive recursion by fold.
“paramorphism”

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)
B The step →+ uses Bekic̆ law
B Fixed point law is not used

I Not infinite unfolding

22

Summary
I. A framework for cyclic datatypes using
second-order algebraic theories
II. Semantics: iteration categories
III. Extracted SN fold by rewrite system FOLDr
Further results
B FOLDr: Confluent on plain terms
B FOLDr: Confluent modulo bisimulation ∼via Huet [1980]’s theorem using local coherence modulo ∼B A complete model of graph database language UnCAL[Buneman’96] (with Matsuda and Asada)
draft available