Inductive Cyclic Sharing
Data Structures
Makoto Hamana
Department of Computer Science,
Gunma University, Japan

30th, June, 2008

http://www.cs.gunma-u.ac.jp/˜hamana/
1This WorkB How to inductively capture cylces and sharing
B Intend to apply it to functional programming
B Strongly related to– Masahito Hasegawa,
Models of Sharing Graphs: A Categorical Semantics of let and letrec,
PhD thesis, University of Edinburgh, 1997.

2Introduction
B Term is a convenient and concise representation of tree structuresin theoretical computer science and logics.
(i) Reasoning: structural induction(ii) Functional programming: pattern matching,structural decomposition/composition(iii) Representable by inductive datatypes(iv) Initial algebra property

B In other areas: adjacency lists, adjacency matrices, pointer structures inC, etc. more complex, not intuitive, difficult to manage
B But ...

3

Introduction
B How about “tree-like” structures?

B How can we represent this data in functional programming?
B Give up to use pattern matching, composition, structural induction
B Not inductive
4

Introduction

Are really no inductive structures in tree-like structures?

B “Almost” a tree

5Graph-Theoretic Observation
B Instead, regard it as

Depth-First Search tree

B DFS tree consists of 3 kinds of edges:(i) Tree edge(ii) Back edge(iii) Right-to-left cross edge

B Characterise pointers for back and cross edges
6This WorkI Cyclic Data Structures(i) Syntax: µ-terms(ii) Implementation: nested datatypes in Haskell(iii) Semantics: domains and traced categories(iv) Application: A syntax for Arrows with loops

B Cyclic Sharing Data Structures(i) New pointer notation(ii) Translation: ⇒ Equational term graphs ⇒ Cyclic sharing theories(iii) Semantics: cartesian-center traced monoidal categories(iv) Graph algorithms: SCC7

I. Cyclic Data Structures

8

Idea
B A syntax of fixpoint expressions by µ-terms is widely used
B Consider the simplest case: cyclic lists

B This is representable byµx.cons(5, cons(6, x))
B But: not the unique representationµx.µy.cons(5, cons(6, x))µx.cons(5, µy.cons(6, µz.x))µx.cons(5, cons(6, µx.cons(5, cons(6, x))))All are the same in the equational theory of µ-terms.

B Thus: structural induction is not available
9Idea
B µ-term may have free variable considered as a dangling pointercons(6, x)“incomplete” cyclic list

B To obtain the unique representation of cyclic and incomplete cyclic lists,
always attach a µ-binder in front of cons:µx1 .cons(5, µx2 .cons(6, x1 ))B seen as uniform addressing of cons-cells
B No axioms
B Inductive
B Initial algebra for abstract syntax with variable binding
by Fiore, Plotkin and Turi [1999]
10

Cyclic Signature and Syntax
B Cyclic signature Σnil(0) ,(1)cons(m, −)for each m ∈ Zx, y ` xx ` µy.cons(6, x)` µx.cons(5, µy.cons(6, x))
B De Bruijn notation:` cons(5, cons(6, ↑2))
B Construction rules:
1≤i≤nn `↑if (k) ∈ Σn + 1 ` t1 · · · n + 1 ` tkn ` f (t1 , . . . , tk )11

Cyclic Lists as Initial Algebra
B F: category of finite cardinals and all functions between themB Def. A binding algebra is an algebra of signature functor on SetF
B E.g. the signature functor Σ : SetF → SetF for cyclic lists
ΣA = 1 + Z × A(− + 1)
B The presheaf of variables: V(n) = n
B The initial V+Σ-algebra (C, in : V+ΣC → C)
C(n) ∼= n + 1 + Z × C(n + 1)

for each n ∈ N

B C(n): represents the set of all incomplete cyclic lists possibly containing
free variables {1, . . . , n}
B C(0): represents the set of all complete (i.e. no dangling pointers) cycliclists
12Cyclic Lists as Initial Algebra
B Examples↑2 ∈ C(2)cons(6, ↑2) ∈ C(1)cons(5, cons(6, ↑2)) ∈ C(0)B Destructor:
tail : C(n) → C(n + 1)
tail(cons(m, t)) = t
B Idioms in functional programming: map, fold
B How to follow a pointer: Huet’s Zipper
B But: following a pointer ↑n needs n-step backward Zipper operations
B One of the benefits of pointer is efficiency– want: constant time dereference13Cyclic Data Structures as Nested Datatypes
B Diving into Haskell
B Implementation: Inductive datatype indexed by natural numbers
data Zerodata Incr n = One | S ndata CList n = Ptr n| Nil| Cons Int (CList (Incr n))

B cf.

C(n) ∼= n + 1 + Z × C(n + 1)

B Examples
S One:: CList (Incr (Incr Zero ))Cons 6 (S One ):: CList (Incr Zero )Cons 5 (Cons 6 (S One)) :: CList Zero14

Cyclic Lists to Haskell’s Internally Cyclic Lists
B Translation
tra :: CList n → [[Int ]] → [Int ]tra Nil
ps = [ ]tra (Cons a as) ps = let x = a : (tra as (x : ps)) in x
tra (Ptr i )ps = nth i ps

B The accumulating parameter ps keeps a newly introduced pointer x by let
B Exampletra (Cons 5 (Cons 6 (Ptr (S One )))) [ ]⇒ 5 : 6 : 5 : 6 : 5 : 6 : 5 : 6 : 5 : 6 : ···B Makes a true cycle in the heap memory, due to graph reduction
B Constant time dereference
B Better: semantic explanation – to more nicely understand tra15

Domain-theoretic interpretation
B Semantics of cyclic structures has been traditionally given as their infinite
expansion in a cpo
B Fits into nicely our algebraic setting
B Cppo⊥ : cpos and strict continuous functions
Cppo : cpos and continuous functions

16

Domain-theoretic interpretation
B Let Σ be the cyclic signature for lists
nil(0) ,(1)cons(m, −)for each m ∈ Z.

B The signature functor Σ1 : Cppo⊥ → Cppo⊥ is defined by
Σ1 (X) = 1⊥ ⊕ Z⊥ ⊥ ⊗ X⊥
B The initial Σ1 -algebra D is a cpo of all finite and infinite possibly partiallists
B Define a clone hD, Di ∈ SetF by
hD, Din = [D n , D] = Cppo(D n , D)
B The least fixpoint operator in Cppo: fix(F ) =B hD, Di can be a V+Σ-algebra[[−]] : C −→ hD, Di.
17FiF
(⊥)
i∈N

Domain-theoretic interpretation
B The unique homomorphism in SetF[[−]] : C −→ hD, Di[[nil]]n = λΘ.nil[[µx.cons(m, t)]]n = λΘ.fix(λx.consD (m, [[t]]n+1 (Θ, x))[[x]]n = λΘ.π x (Θ)
B Example of interpretation[[µx.cons(5, µy.cons(6, x))]]0 (²) = fix(λx.consD (5, fix(λy.consD (6, π x (x, y)))= fix(λx.consD (5, consD (6, x))= cons(5, cons(6, cons(5, cons(6, . . .
tra :: CList a → [[Int ]] → [Int ]tra Nil
ps = [ ]tra (Cons a as) ps = let x = a : (tra as (x : ps)) in x
tra (Ptr i )ps = nth i ps18

Interpretation in traced cartesian categories
B A more abstract semantics for cyclic structures in terms oftraced symmetric monoidal categories [Hasegawa PhD thesis, 1997]
B Let C be an arbitrary cartesian category having a trace operator Tr[[n ` i]] = π i[[n ` µx.f (t1 , . . . , tk )]] = Tr D (∆ ◦ [[f ]]Σ ◦ h[[n + 1 ` t1 ]], . . . , [[n + 1 ` t1 ]]i)
B This categorical interpretation is the unique homomorphism[[−]] : C −→ hD, Di
to a V+Σ-algebra of clone hD, Di defined by hD, Din = C(D n , D)

B Examples(i) C = cpos and continuous functions(ii) C = Freyd category generated by Haskell’s Arrows
19Application: A New Syntax for Arrows
B Arrows [Hughes’00] are a programming concept in Haskell to make aprogram involving complex “wiring”-like data flows easier
B Example: a counter circuit

newtype SeqMap b c = SM (Seq b -> Seq c)data Seq b= SCons b (Seq b)
counter :: SeqMap Int Int
counter = proc reset -> do-- Paterson’s notation [ICFP’01]
rec output <- returnA -< if (reset==1) then 0 else next
next<- delay 0 -< output+1
returnA -< output
20

Application: A New Syntax for Arrows
B Paterson defined an Arrow with a loop operator called ArrowLoop
class Arrow _A => ArrowLoop _A whereloop :: _A (b,d) (c,d) -> _A b c
B Arrow(or, Freyd category)is a cartesian-center premonoidal category [Heunen, Jacobs, Hasuo’06]
B ArrowLoop
is a cartesian-center traced premonoidal category [Benton, Hyland’03]
B Cyclic sharing theory is interpreted
in a cartesian-center traced monoidal category [Hasegawa’97]
B What happens when cyclic terms are interpreted as Arrows with loops?

21

Application: A New Syntax for Arrows
B Term syntax for ArrowLoop
B Example: a counter circuit

B Intended computationµx.Cond(reset, Const0, Delay0(Inc(x)))
where reset is a free variable

B term :: Syntx (Incr Zero)term = Cond(Ptr(S One),Const0,Delay0(Inc(Ptr(S(S One)))))

22

Translation from cyclic terms to Arrows with loops
tl :: (Ctx n, ArrowSigStr _A d) => Syntx n -> _A [d] dtl (Ptr i)= arr (\xs -> nth i xs)
tl (Const0)= loop (arr dup <<< const0 <<< arr (\(xs,x)->()))
tl (Inc t)= loop (arr dup <<< inc<<< tl t <<< arr supp)
tl (Delay0 t)= loop (arr dup <<< delay0 <<< tl t <<< arr supp)
tl (Cond (s,t,u)) = loop (arr dup <<< cond <<< arr(\((x,y),z)->(x,y,z))<<< (tl s &&& tl t) &&& tl u <<< arr supp)
B This is the same as Hasegawa’s interpretation of cyclic sharing structures
B Define an Arrow by term
term = Cond(Ptr(S One),Const0,Delay0(Inc(Ptr(S(S One)))))
counter’ :: SeqMap Int Int
counter’ = tl term <<< arr (\x->[x])23Simulation of circuit
B Let test_input be(1) reset (by the signal 1),(2) count +1 (by the signal 0),(3) reset,(4) count +1,(5) count +1, . . .

test_input = [1,0,1,0,0,1,0,1]
run1 = partRun counter test_input
run2 = partRun counter’ test_input
In Haskell interpreter> run1[0,1,0,1,2,0,1,0]> run2[0,1,0,1,2,0,1,0]
24-- original-- cyclic term

Summary
B Inductive characterisation of cyclic sharing terms
B Semantics
B Implementations in Haskell
B Good connections between semantics and functional programming(i) Cartesian-center traced monoidal categories [Hasegawa]
I Cyclic Sharing Data Structures with constant time dereference(ii) Monads [Moggi] I Effects [Wadler](iii) Freyd categories [Power, Robinson] I Arrows [Hughes]——————————————–B Cyclic Sharing Data Structures – more challenging, more interesting(i) New pointer notation(ii) Translation: ⇒ Equational term graphs ⇒ Cyclic sharing theories(iii) Semantics: cartesian-center traced monoidal categories(iv) Graph algorithms: SCC
25

II. Cyclic Sharing Data Structures26

Cyclic Sharing Data Structures
B Sharing via cross edge

B Termµx.bin(µy1 .bin(µz.bin(↑x, lf(6)), .1↑y1 ), lf(9)) : B(B(B(P, L), P), L)
B New construct: pointer .p↑x(p:position,B Inductive type indexed by shape trees
B Exactly implemented by GADT in Haskell
27

in addition to ↑x)Translation of Cyclic Sharing Terms
B Semantics
B To get constant time dereference
B Translations
Cyclic Sharing
Terms

attpos/Cyclic Sharing tre
Terms with pos.

/ ETG

trc

/ CST

Has.
/

(F : C → S)

B Cartesian-center traced symmetric monoidal category (F : C → Hask)
B Example of translation

28

µx.bin(µy1 .bin(µz.bin(↑x, lf(6)), .1↑y1 ), lf(9))
de Br.

=

attpos7→bin(bin(bin(↑3, lf(6)), .1↑1), lf(9))
bin² (bin1 (bin11 (↑1113, lf 1 12(6)), .1↑12 1), lf 2 (9)){² |tre7→²= bin(1, 2)

1= bin(11, 12)

11= bin(111, 112)

12= 11111 = ²112 = lf(6)
2
trc

7→

= lf(9)}letrec (², 1, 11, 12, 111, 112, 2)= (bin(1, 2), bin(1, 12), bin(111, 112), 11, ², lf(6), lf(9)) in ²
F (∆); (id ⊗ Tr

Hasegawa

7→D7(F ∆7 ; ([[², 1, . . . ` bin(1, 2)]]⊗[[², 1, . . . ` bin(11, 12)]]⊗···29); F ∆)); F π 1

Graph Algorithm: Strong Connected Components

30Graph Algorithm: Computing SCC
Strong Connected Components

B The number described in a node is a DFS number.
B The number labelled outside of a node is lowlink.
B A gray node is the root of a scc
31

SCC: Tarjan’s Algorithm in Haskell
scc :: HTree -> [[Lab]]scc t = sccs
where (lowlink, node_stack, sccs) = visit t [] []visit :: HTree -> [Lab] -> [[Lab]] -> (Lab,[Lab],[[Lab]])visit (HLf i e) vs out= (i, vs, [i]:out)
visit (HBin i s1 s2) vs out= if lowlink == ithen (lowlink, dropWhile (>=i) vs’’,
takeWhile (>=i) vs’’:out2)
else (lowlink,vs’’, out2)
where (k1, vs’, out1) = visit s1 (i:vs) out(k2, vs’’,out2) = visit s2 vs’
out1
lowlink = minimum [k1, k2, i]visit (HCross i t) vs out= if (notElem j vs)then (i,vs, [i]:out)
else (min i j, i:vs, out)
where j = lab t-- (*) dereference in O(1)32

SCC: Tarjan’s Algorithm – procedural implementation
Input: Graph G = (V, E), Start node v0
index = 0
S = empty
tarjan(v0)// DFS node number counter// An empty stack of nodes// Start a DFS at the start node

procedure tarjan(v)v.index = index// Set the depth index for v
v.lowlink = index++
S.push(v)// Push v on the stackforall (v, v’) in E do// Consider successors of v
if (v’.index is undefined) // Was successor v’ visited?
tarjan(v’)// Recursev.lowlink = min(v.lowlink, v’.lowlink)elseif (v’ in S)// Is v’ on the stack?
v.lowlink = min(v.lowlink, v’.index)
if (v.lowlink == v.index)// Is v the root of an SCC?
print "SCC:"
repeatv’ = S.pop
print v’until (v’ == v)
33