Initial Algebra Semantics for
Cyclic Sharing Structures

Makoto Hamana
Department of Computer Science,
Gunma University, JapanJuly, 2009, TLCA’09

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

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

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

Introduction
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

Introduction

Are really no inductive structures intree-like structures?

This 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 uniquelyin functional languages and proof assistants

Variations 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]f

Ghani,Uustalu,Hamana

2006

Hamana2009

Cyclic sharing structures

T∗ T(Set )

Basic Idea

Basic 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

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) ))Formulation: 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?

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)

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)

Typed Abstract Syntax
forCyclic Sharing Structures

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.

Syntax 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.

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))

Syntax and Types
Typing rules (de Bruijn version)|Γ| = i − 1 p ∈ Pos(σ)Γ, σ, Γ0 ` .p↑i : Pk∈ZΓ ` lf(k) : LB(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.

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 )Initial Algebra Semantics
B Σ-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τ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) : LB(E, E), Γ ` s : σ B(σ, E), Γ ` t : τΓ ` bin(s, t) : B(σ, τ )Initial Algebra
B All cyclic sharing treesTτ (Γ) = {t | Γ ` t : τ }Thm. T forms an initial Σ-algebra.
[Proof]B Smith-Plotkin construction of an initial algebraPrinciples
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)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Summary
B An initial algebra characterisation
Goals
B To derive the following from ↑ :[I] A simple term syntax[II] An inductive typefor cyclic sharing structures

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 [M. Hasegawa TLCA’97]–(Equational) term graphs [Barendregt et al.’87][Ariola,Klop’96]

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 [M. Hasegawa TLCA’97]
Further applications(cyclic)-CT PPPPPqPHaskell(cartesian-center traced)∼ “arrows” with loops in Haskell(efficient implementation)