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