1Initial Algebra Semantics for
Cyclic Sharing Structures

Makoto Hamana
Department of Computer Science,
Gunma University, Japan
August 2009, GoI Workshop, Kyoto

http://www.cs.gunma-u.ac.jp/˜hamana/

2This WorkB How to inductively capture cylces and sharing
B Intended to apply it to functional programming

3

Introduction
B Terms are a representation of tree structures(i) Reasoning: structural induction(ii) Functional programming:
pattern matching, structural recursion(iii) Type: inductive type(iv) Initial algebra property

4Introduction
B What about tree-like structures?

B How can we represent this data in functional programming?
B Maybe: vertices and edges set, adjacency lists, etc.
B Give up to use pattern matching, structural induction
B Not inductive

5Introduction

Are really no inductive structures intree-like structures?

6This WorkB Gives an initial algebra characterisation of
cyclic sharing structures
Aim
B To derive the following from ↑ :[I] A simple term syntax that admits
structural induction / recursion[II] To give an inductive type that represents
cyclic sharing structures uniquely
in functional languages and proof assistants

7Variations of Initial Algebra Semantics
B Various computational structures are formulated as
initial algebras by varying the base category
Abstract syntax

SetADJ

1975

S-sorted abstract syntax

SetSRobinson

1994

Abstract syntax with binding

SetF

Fiore,Plotkin,Turi

1999

Recursive path ordring

LO

R. Hasegawa

2002

S-sorted 2nd-order abs. syn.

(SetF↓S )SFiore

2003

2nd-order rewriting systems

PreF

Hamana2005

Explicit substitutions[Set, Set]fGhani,Uustalu,Hamana

2006

Hamana2009

Cyclic sharing structures

T∗ T(Set )8Basic Idea

9Basic Idea: Graph Algorithmic View
B Traverse a graph in a depth-first search manner:

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

10

Formulation: Cycles by µ-terms
Idea
B Binders as pointers
B Back edges = bound variables
Cyclesµx.bin(µy1 .bin(lf(5), lf(6)), µy2 .bin( x, lf(7) ))11Formulation: Sharing via ?
Idea
B Binders as pointers
B Back edges = bound variables
B Right-to-left Cross edges = ?
Sharingµx.bin(µy1 .bin(lf(5), lf(6)), µy2 .bin(, lf(7))).

Can we fill the blank to refer the node 5 by a bound variable?

12

Formulation: Sharing via Pointer
B Cross edges = pointersby a new notationµx.bin(µy1 .bin(lf(5), lf(6)), µy2 .bin( .11↑x , lf(7)))
Pointer .11↑x means
B going back to the node x, thenB going down through the left child twice (by position 11)

13

Formulation: Sharing via Pointer
B Cross edges = pointersby a new notationµx.bin(µy1 .bin(lf(5), lf(6)), µy2 .bin( .11↑x , lf(7)))
Pointer .11↑x means Need to ensure a correct pointer only!!
B going back to the node x, thenB going down through the left child twice (by position 11)

14

Typed Abstract Syntax
forCyclic Sharing Structures

15

Shape Trees
B Skeltons of cyclic sharing trees
Shape trees τ ::= E|P|

L|

B(τ 1 , τ 2 )B Used as types
B Blue nodes represent possible positions for sharing pointers.

16Syntax and Types
Typing rulesp ∈ Pos(σ)Γ, x : σ, Γ0 ` .p↑x : Pk∈ZΓ ` lf(k) : Lx : B(E, E), Γ ` ` : σ x : B(σ, E), Γ ` r : τΓ ` µx.bin(`, r) : B(σ, τ )B A type declaration x : σ means:“σ is the shape of a subtree headed by µx”.
B Taking a position p ∈ Pos(σ) safely refers to a position inthe subtree.

17

Example: making bin-nodex:B(E, E) `µy1 .bin(5, 6) : B(L, L)

x:B(B(L, L), E) `µy2 .bin(.11↑x, 7) : B(P, L)` µx.bin(µy1 .bin(5, 6), µy2 .bin(.11↑x, 7)): B(B(L, L), B(P, L))18

Syntax and Types
Typing rules (de Bruijn version)|Γ| = i − 1 p ∈ Pos(σ)Γ, σ, Γ0 ` .p↑i : Pk∈Z
Γ ` lf(k) : L

B(E, E), Γ ` s : σ B(σ, E), Γ ` t : τΓ ` bin(s, t) : B(σ, τ )Thm.
Given rooted, connected and edge-ordered graph,
the term representation in de Bruijn is unique.

19

Cyclic Sharing Data Structures
B Sharing via cross edge

B Termbin(bin(bin(↑ 3, lf(6)), .1↑1), lf(9))

20

Initial Algebra Semantics
B Cyclic sharing trees are all well-typed terms:Tτ (Γ) = {t | Γ ` t : τ }B Need: sets indexed bycontexts T∗ and shape trees TT∗ TConsider algebras in (Set )21

Initial Algebra Semantics
B Algebra of an endofunctor Σ:Σ-algebra (A, α : ΣA → A)T∗ T

B Functor Σ : (Set )cyclic sharing trees is defined by(ΣA)E = 0∗- (SetT )T for(ΣA)P = PO(ΣA)L = KZ(ΣA)B(σ,τ ) = δ B(E,E) Aσ × δ B(σ,E) Aτ22

Initial Algebra Semantics
B Σ-algebra (A, α : ΣA → A)T∗ T

B Functor Σ : (Set )cyclic sharing trees is given byptr

Abin: PO → APσ,τ A∗- (SetT )T forlf

A: KZ → AL: δ B(E,E) Aσ × δ B(σ,E) Aτ → AB(σ,τ )Typing rules (de Bruijn version)|Γ| = i − 1 p ∈ Pos(σ)Γ, σ, Γ0 ` .p↑i : Pk∈Z
Γ ` lf(k) : L

B(E, E), Γ ` s : σ B(σ, E), Γ ` t : τΓ ` bin(s, t) : B(σ, τ )23Initial Algebra
B All cyclic sharing treesTτ (Γ) = {t | Γ ` t : τ }Thm. T forms an initial Σ-algebra.
[Proof]B Smith-Plotkin construction of an initial algebra

24Principles
The initial algebra characterisation derives(i) Structural recursion by the unique homomorphism(ii) Structural induction by [Hermida,Jacobs I&C’98]iii) Inductive type (in Haskell)

25

Structural Recursion Principle
Thm. The unique homomorphism φ : T- A is:AφP (Γ)(.p↑i) = ptr (Γ)(.p↑i)AφL (Γ)(lf(k)) = lf (Γ)(k)φB(σ,τ ) (Γ)(bin(s, t))
A= bin (Γ)(φσ (B(E, E), Γ)(s), φτ (B(σ, E), Γ)(t))
B “fold” in Haskell

26

Structural Induction Principle
Thm. Let P be a predicate on T .
To prove that PτΓ (t) holds for all t ∈ Tτ (Γ),
it suffices to show

Γ(i) PP (.p↑i) holds for all .p↑i ∈ PO(Γ),(ii) PLΓ (lf(k)) holds for all k ∈ Z,iii) If PσB(E,E),Γ (s) & PτB(σ,E),Γ (t) holds, thenΓPB(σ,τ) (bin(s, t)) holds.

27

Inductive Type for Cyclic Sharing Structures
T∗ T

Constructors of the initial algebra T ∈ (Set )ptrT (Γ) : PO(Γ) → TP (Γ);
lf T (Γ) : Z → TL (Γ);.p↑i 7→ .p↑i.

k 7→ lf(k).

binσ,τ T (Γ) : Tσ (B(E, E), Γ)×Tτ (B(σ, E), Γ)→ TB(σ,τ ) (Γ)
GADT in Haskell
data T :: * -> * -> * where
Ptr :: Ctx n => n -> T n P
Lf :: Ctx n => Int -> T n L
Bin :: (Ctx n, Shape s, Shape t) =>T (TyCtx (B E E) n) s -> T (TyCtx (B s E) n) t-> T n (B s t)
B Dependent type def. in Agda is more straightforward

28Summary
B An initial algebra characterisation
Goals
B To derive the following from ↑ :[I] A simple term syntax[II] An inductive typefor cyclic sharing structures
Reference M. Hamana. Initial Algebra Semantics
for Cyclic Sharing Structures, TLCA’09.

29

Connections to Other Works
There are interpretations:
T! -Equational Term Graphs-S

where S is any of(i) Coalgebraic(ii) Domain-theoretic(iii) Categorical semantics:
Traced sym. monoidal categories [Hasegawa’97]–(Equational) term graphs [Barendregt et al.’87][Ariola,Klop’96]

30

Connection to Traced Categorical Semantics
B Interpretations
T!-

Equational Term Graphs ∼= letrec-Exprs- (F : C → M)

B Cartesian-center symmetric traced monoidal category= identity-on-object functor F : C → M– Cartesian C– Symmetric traced monoidal M

31

Cyclic Sharing Data Structures
B Sharing via cross edge

B Termµx.bin(µy1 .bin(µz.bin(↑ x, lf(6)), .1↑y1 ), lf(9))

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

=bin(bin(bin(↑ 3, lf(6)), .1↑1), lf(9))

7→bin (bin1 (bin11 (↑1113, lf 112 (6)), .1↑12 1), lf 2 (9)){ |7→7→
11112111
112
2= bin(1, 2)= bin(11, 12)= bin(111, 112)= 11== lf(6)= 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 (F ∆7 ; ( [[, 1, . . . ` bin(1, 2)]]⊗

Hasegawa

7→[[, 1, . . . ` bin(11, 12)]]⊗· · · ); F ∆)); F π 1

33Connection to Traced Categorical Semantics
B How useful?
B Application: Haskell’s “arrows” [Hughes’00][Paterson’01]– Arrow-type in Haskell(or, Freyd category)is a cartesian-center premonoidal category[Heunen, Jacobs, Hasuo’06]– Arrow with loop
is a cartesian-center traced premonoidal category[Benton, Hyland’03]– Cyclic sharing theory is interpreted
in a cartesian-center traced monoidal category[Hasegawa’97]
B What impact for functional progrmming?