{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T16:24:02Z","timestamp":1759335842594},"reference-count":27,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2016,11,4]],"date-time":"2016-11-04T00:00:00Z","timestamp":1478217600000},"content-version":"unspecified","delay-in-days":308,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2016]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The main aim of the paper is to give a simple and conceptual account for the correspondence (originally described by Bodini, Gardy, and Jacquot) between \u03b1-equivalence classes of closed linear lambda terms and isomorphism classes of rooted trivalent maps on compact-oriented surfaces without boundary, as an instance of a more general correspondence between linear lambda terms with a context of free variables and rooted trivalent maps with a boundary of free edges. We begin by recalling a familiar diagrammatic representation for linear lambda terms, while at the same time explaining how such diagrams may be read formally as a notation for endomorphisms of a reflexive object in a symmetric monoidal closed (bi)category. From there, the \u201ceasy\u201d direction of the correspondence is a simple forgetful operation which erases annotations on the diagram of a linear lambda term to produce a rooted trivalent map. The other direction views linear lambda terms as <jats:italic>complete invariants<\/jats:italic> of their underlying rooted trivalent maps, reconstructing the missing information through a Tutte-style topological recurrence on maps with free edges. As an application in combinatorics, we use this analysis to enumerate bridgeless rooted trivalent maps as linear lambda terms containing no closed proper subterms, and conclude by giving a natural reformulation of the Four Color Theorem as a statement about typing in lambda calculus.<\/jats:p>","DOI":"10.1017\/s095679681600023x","type":"journal-article","created":{"date-parts":[[2016,11,4]],"date-time":"2016-11-04T08:51:40Z","timestamp":1478249500000},"source":"Crossref","is-referenced-by-count":5,"title":["Linear lambda terms as invariants of rooted trivalent maps"],"prefix":"10.1017","volume":"26","author":[{"given":"NOAM","family":"ZEILBERGER","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,11,4]]},"reference":[{"key":"S095679681600023X_ref24","unstructured":"Vidal S. (2010) Groupe Modulaire et Cartes Combinatoires: G\u00e9n\u00e9ration et Comptage. PhD Thesis, Universit\u00e9 Lille I, France (July)."},{"key":"S095679681600023X_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-38361-1"},{"key":"S095679681600023X_ref11","first-page":"212","volume-title":"Symposium on Semantics of Algorithmic Languages","author":"Knuth","year":"1970"},{"key":"S095679681600023X_ref18","first-page":"65","volume-title":"Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science","author":"Seely","year":"1987"},{"key":"S095679681600023X_ref23","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1968-11877-4"},{"key":"S095679681600023X_ref1","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"S095679681600023X_ref20","unstructured":"Stay M. (2013) Compact closed bicategories. Theory and Applications of Categories 31 (2016), pp. 755\u2013798."},{"key":"S095679681600023X_ref4","volume-title":"Combinatory Logic","author":"Curry","year":"1972"},{"key":"S095679681600023X_ref16","first-page":"221","volume-title":"Combinatorial Mathematics and its Application","author":"Penrose","year":"1971"},{"key":"S095679681600023X_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2013.01.008"},{"key":"S095679681600023X_ref5","unstructured":"Hyland M. (2013) Classical lambda calculus in modern dress. Mathematical Structures in Computer Science. In special issue dedicated to Corrado B\u00f6hm for his 90th birthday, pp. 1\u201320."},{"key":"S095679681600023X_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005131"},{"key":"S095679681600023X_ref26","unstructured":"Zeilberger N. (2015b) Counting isomorphism classes of \u03b2-normal linear lambda terms. arXiv:1509.07596 (25 September)"},{"key":"S095679681600023X_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569302.006"},{"key":"S095679681600023X_ref15","unstructured":"OEIS Foundation Inc. (2016) The On-Line Encyclopedia of Integer Sequences."},{"key":"S095679681600023X_ref19","first-page":"289","volume-title":"New Structures for Physics","author":"Selinger","year":"2011"},{"key":"S095679681600023X_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037107"},{"key":"S095679681600023X_ref22","doi-asserted-by":"publisher","DOI":"10.4153\/CJM-1962-032-x"},{"key":"S095679681600023X_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01196130"},{"key":"S095679681600023X_ref27","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(3:22)2015"},{"key":"S095679681600023X_ref21","first-page":"848","article-title":"An update on the four-color theorem","volume":"45","author":"Thomas","year":"1998","journal-title":"Not. Am. Math. Soc."},{"key":"S095679681600023X_ref25","unstructured":"Zeilberger N. (2015a) Balanced polymorphism and linear lambda calculus. Talk at TYPES 2015, Tallinn, Estonia (18 May)."},{"key":"S095679681600023X_ref17","first-page":"403","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism","author":"Scott","year":"1980"},{"key":"S095679681600023X_ref9","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1993.1055"},{"key":"S095679681600023X_ref7","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-37.2.273"},{"key":"S095679681600023X_ref13","first-page":"2","volume-title":"Proceedings of the 22nd Conference on Foundations of Software Technology and Theoretical Computer Science","author":"Mairson","year":"2002"},{"key":"S095679681600023X_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/0095-8956(90)90114-F"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679681600023X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T23:50:17Z","timestamp":1559951417000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679681600023X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"references-count":27,"alternative-id":["S095679681600023X"],"URL":"https:\/\/doi.org\/10.1017\/s095679681600023x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"article-number":"e21"}}