Functional Programming Seminar

Makoto Hamana (Gunma University, Japan)

Initial Algebra Semantics for Cyclic Sharing Structures 

 "Tree-like" structures -- trees involving cycles and sharing --appear very often in logic and computer science. They are usually treated as graphs, because there do not seem to exist clear inductive structures. I propose a simple term syntax for cyclicsharing structures that admits structural induction and recursion principles. I show that the obtained syntax is directly usable in Haskell and Agda, as well as ordinary data structures such as lists and trees. To achieve this goal, I use categorical approachto initial algebra semantics in a presheaf category. I will also try to relate this with traced categorical models.