×

Nested term graphs (work in progress). (English) Zbl 1476.68121

Middeldorp, Aart (ed.) et al., Proceedings of the 8th international workshop on computing with terms and graphs, TERMGRAPH 2014, Vienna, Austria, July 13, 2014. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 183, 48-65 (2015).
Summary: We report on work in progress on ‘nested term graphs’ for formalizing higher-order terms (e.g. finite or infinite \(\lambda\)-terms), including those expressing recursion (e.g. terms in the \(\lambda\)-calculus with letrec). The idea is to represent the nested scope structure of a higher-order term by a nested structure of term graphs. Based on a signature that is partitioned into atomic and nested function symbols, we define nested term graphs both in a functional representation, as tree-like recursive graph specifications that associate nested symbols with usual term graphs, and in a structural representation, as enriched term graph structures. These definitions induce corresponding notions of bisimulation between nested term graphs. Our main result states that nested term graphs can be implemented faithfully by first-order term graphs.
For the entire collection see [Zbl 1446.68017].

MSC:

68Q42 Grammars and rewriting systems
68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: arXiv Link

References:

[1] B. Accattoli & S. Guerrini (2009): Jumping Boxes. In Erich Grädel & Reinhard Kahle, editors: Computer Science Logic, Lecture Notes in Computer Science 5771, Springer Berlin Heidelberg, pp. 55-70, doi:10.1007/978-3-642-04027-6 7. · Zbl 1257.03038 · doi:10.1007/978-3-642-04027-6_7
[2] A. Asperti (1995): Linear Logic, Comonads And Optimal Reductions. Fundamenta Informaticae 22(1,2), pp. 3-22, doi:10.3233/FI-1995-22121. Available at http://dl.acm.org/citation.cfm?id=2383063.2383064. · Zbl 0818.03007 · doi:10.3233/FI-1995-22121
[3] R. Bird & R. Paterson (1999): De Bruijn Notation as a Nested Datatype. Journal of Functional Programming 9(1), pp. 77-91, doi:10.1017/S0956796899003366. Available at http://www.soi.city.ac.uk/ ross/ papers/debruijn.html. · Zbl 0926.68025 · doi:10.1017/S0956796899003366
[4] S. Blom (2001): Term Graph Rewriting -Syntax and Semantics. Ph.D. thesis, Vrije Universiteit Amsterdam.
[5] N. Bourbaki (1954):Éléments de mathématiques: Théories des ensembles. Hermann. · Zbl 0055.27902
[6] N. Ghani, C. Lüth & F. de Marchi (2005): Monads of coalgebras: rational terms and term graphs. Mathematical Structures in Computer Science 15, pp. 433-451, doi:10.1017/S0960129505004743. · Zbl 1169.18303 · doi:10.1017/S0960129505004743
[7] C. Grabmayer & J. Rochel (2013): Term Graph Representations for Cyclic Lambda Terms. In: Proceedings of TERMGRAPH 2013, EPTCS 110, pp. 56-73, doi:10.4204/EPTCS.110. Extending report: arXiv:1308.1034. · Zbl 1415.68023 · doi:10.4204/EPTCS.110
[8] C. Grabmayer & J. Rochel (2014): Maximal Sharing in the Lambda Calculus with letrec. In: Proceedings of ICFP ’14, September 1-6, 2014, Gothenburg, Sweden, pp. 67-80, doi:10.1145/2628136.2628148. · Zbl 1345.68053 · doi:10.1145/2628136.2628148
[9] R.J.M. Hughes (1982): Supercombinators: A new implementation method for applicative languages. In: LFP ’82: Proceedings of the 1982 ACM symposium on LISP and functional programming, pp. 1-10, doi:10.1145/800068.802129. · doi:10.1145/800068.802129
[10] J. R. Kennaway, J. W. Klop, M. R. Sleep & F. J. de Vries (1994): On the Adequacy of Graph Rewriting for Simulating Term Rewriting. ACM Trans. Program. Lang. Syst. 16(3), pp. 493-523, doi:10.1145/177492.177577. · doi:10.1145/177492.177577
[11] E. Kohlbecker, D.P. Friedman, M. Felleisen & B. Duba (1986): Hygienic Macro Expansion. In: Proceed-ings of the 1986 ACM Conference on LISP and Functional Programming, LFP ’86, ACM, pp. 151-161, doi:10.1145/319838.319859. · doi:10.1145/319838.319859
[12] Analogous to proofnet reduction. Rewriting should ’interact nicely’ with boxes.
[13] Y. Lafont (1990): Interaction Nets. In: POPL ’90, ACM Press, pp. 95-108, doi:10.1145/96709.96718. · doi:10.1145/96709.96718
[14] C. Lüth (1997): Categorial Term Rewriting: Monads and Modularity. Ph.D. thesis, University of Edinburgh.
[15] C. Lüth & N. Ghani (1997): Monads and modular term rewriting. In E. Moggi & G. Rosolini, editors: Category Theory and Computer Science, Lecture Notes in Computer Science 1290, Springer Berlin Heidelberg, pp. 69-86, doi:10.1007/BFb0026982. · Zbl 0889.68084 · doi:10.1007/BFb0026982
[16] D. Plump (1999): Term Graph Rewriting. In H. Ehrig, G. Engels, H.-J. Kreowski & G. Rozenberg, editors: Handbook of Graph Grammars and Computing by Graph Transformation, 2, World Scientific, pp. 3-61, doi:10.1142/9789812815149 0001. · doi:10.1142/9789812815149_0001
[17] W. Van Orman Quine (1940): Mathematical Logic. Harvard University Press, Cambridge, Mass. · Zbl 0063.06360
[18] F. van Raamsdonk (1996): Confluence and Normalisation for Higher-Order Rewriting. Ph.D. thesis, Vrije Universiteit Amsterdam.
[19] M.R. Sleep, M.J. Plasmeijer & M.C.J.D. van Eekelen (1993): Term Graph Rewriting -Theory and Practice. John Wiley & Sons. · Zbl 0818.68099
[20] Terese (2003): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science 55, Cambridge University Press. · Zbl 1030.68053
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.