Abstract
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. In the case of graphs or ”tree-like” structures – trees involving cycles and sharing – however, it is not clear 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, as well as ordinary data structures such as lists and trees. To achieve this goal, we use 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aczel, P., Adámek, J., Milius, S., Velebil, J.: Infinite trees and completely iterative theories: a coalgebraic view. Theor. Comput. Sci. 300(1-3), 1–45 (2003)
Ariola, Z.M., Klop, J.W.: Equational term graph rewriting. Fundam. Inform. 26(3/4), 207–240 (1996)
Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 78–92. Springer, Heidelberg (2005)
Barendregt, H.P., van Eekelen, M.C.J.D., Glauert, J.R.W., Kennaway, R., Plasmeijer, M.J., Ronan Sleep, M.: Term graph rewriting. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.) PARLE 1987. LNCS, vol. 259, pp. 141–158. Springer, Heidelberg (1987)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Kenneth Zadeck, F.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)
Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. In: Proc. of POPL 2005, pp. 271–282 (2005)
Courcelle, B., Kahn, G., Vuillemin, J.: Algorithmes d’equivalence et de reduction a des expressions minimales dans une classe d’equations recursives simples. In: Loeckx, J. (ed.) ICALP 1974. LNCS, vol. 14, pp. 200–213. Springer, Heidelberg (1974)
Dybjer, P.: Inductive families. Formal Aspects of Computing 6, 440–465 (1994)
Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proc. of PPDP 2002, pp. 26–37 (2002)
Fiore, M.: Second-order and dependently-sorted abstract syntax. In: Proc. of LICS 2008, pp. 57–68 (2008)
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proc. of 14th Annual Symposium on Logic in Computer Science, pp. 193–202 (1999)
Ghani, N., Hamana, M., Uustalu, T., Vene, V.: Representing cyclic structures as nested datatypes. In: Proc. of TFP 2006, pp. 173–188 (2006)
Ghani, N., Johann, P.: Initial algebra semantics is enough! In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 207–222. Springer, Heidelberg (2007)
Ghani, N., Uustalu, T., Hamana, M.: Explicit substitutions and higher-order syntax. Higher-Order and Symbolic Computation 19(2/3), 263–282 (2006)
Hamana, M.: Free Σ-monoids: A higher-order syntax with metavariables. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 348–363. Springer, Heidelberg (2004)
Hasegawa, M.: Models of Sharing Graphs: A Categorical Semantics of let and letrec. PhD thesis, University of Edinburgh (1997)
Hasegawa, R.: Two applications of analytic functors. Theor. Comput. Sci. 272(1-2), 113–175 (2002)
Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf. Comput. 145(2), 107–152 (1998)
Johann, P., Ghani, N.: Foundations for structured programming with GADTs. In: Proc. of POPL 2008, pp. 297–308 (2008)
McBride, C.: Faking it: Simulating dependent types in Haskell. J. Funct. Program. 12(4&5), 375–392 (2002)
Miculan, M., Scagnetto, I.: A framework for typed HOAS and semantics. In: Proc. of PPDP 2003, pp. 184–194. ACM Press, New York (2003)
Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology (2007)
Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: Proc. of ICFP 2006, pp. 50–61 (2006)
Robinson, E.: Variations on algebra: monadicity and generalisations of equational theories. Formal Aspects of Computing 13(3-5), 308–326 (2002)
Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM J. Comput 11(4), 763–783 (1982)
Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM Journal of Computing 1(2), 146–160 (1972)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hamana, M. (2009). Initial Algebra Semantics for Cyclic Sharing Structures. In: Curien, PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02273-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-02273-9_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02272-2
Online ISBN: 978-3-642-02273-9
eBook Packages: Computer ScienceComputer Science (R0)