Hamana, Makoto - Initial Algebra Semantics for Cyclic Sharing Tree Structures

lmcs:1060 - Logical Methods in Computer Science, September 3, 2010, Volume 6, Issue 3
Initial Algebra Semantics for Cyclic Sharing Tree Structures

Authors: Hamana, Makoto

Terms are a concise representation of tree structures. Since they can be naturally defined by an inductive type, they offer data structures in functional programming and mechanised reasoning with useful principles such as structural induction and structural recursion. However, for graphs or "tree-like" structures - trees involving cycles and sharing - it remains unclear what kind of inductive structures exists and how we can faithfully assign a term representation of them. In this paper we propose a simple term syntax for cyclic sharing structures that admits structural induction and recursion principles. We show that the obtained syntax is directly usable in the functional language Haskell and the proof assistant Agda, as well as ordinary data structures such as lists and trees. To achieve this goal, we use a categorical approach to initial algebra semantics in a presheaf category. That approach follows the line of Fiore, Plotkin and Turi's models of abstract syntax with variable binding.


Source : oai:arXiv.org:1007.4266
DOI : 10.2168/LMCS-6(3:15)2010
Volume: Volume 6, Issue 3
Published on: September 3, 2010
Submitted on: November 13, 2009
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 102 times.
This article's PDF has been downloaded 112 times.