{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T13:50:32Z","timestamp":1778766632813,"version":"3.51.4"},"reference-count":64,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4184,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2002,2]]},"DOI":"10.1016\/s0304-3975(00)00349-2","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T10:11:15Z","timestamp":1027591875000},"page":"113-175","source":"Crossref","is-referenced-by-count":33,"title":["Two applications of analytic functors"],"prefix":"10.1016","volume":"272","author":[{"given":"Ryu","family":"Hasegawa","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00349-2_BIB1","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/BF01175640","article-title":"Konstruktiver Aufbau eines Abschnitts der zweiten Cantorschen Zahlenklasse","volume":"53","author":"Ackermann","year":"1951","journal-title":"Math. Z."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB2","volume":"vol. 189","author":"Ad\u00e1mek","year":"1994"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB3","doi-asserted-by":"crossref","first-page":"227","DOI":"10.21099\/tkbjm\/1496160577","article-title":"A consistency proof of a system including Feferman's ID\u03be by Takeuti's reduction method","volume":"11","author":"Arai","year":"1987","journal-title":"Tsukuba J. Math."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB4","doi-asserted-by":"crossref","unstructured":"M. Barr, Terminal coalgebras in well-founded set theory, Theoret. Comput. Sci. 114 (1993) 299\u2013315; (Corrigendum, Additions and corrections to \u201cTerminal coalgebras in well-founded set theory\u201d 124 (1994) 189\u2013192).","DOI":"10.1016\/0304-3975(93)90076-6"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB5","volume":"vol. 141","author":"Becker","year":"1993"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB6","first-page":"75","article-title":"A term calculus for intuitionistic linear logic","volume":"vol. 664","author":"Benton","year":"1993"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB7","series-title":"Combinatorial Species and Tree-like Structures","author":"Bergeron","year":"1997"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB8","first-page":"78","article-title":"What is a categorical model of intuitionistic linear logic?","volume":"vol. 902","author":"Bierman","year":"1995"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB9","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/0168-0072(86)90052-7","article-title":"A new system of proof-theoretic ordinal functions","volume":"32","author":"Buchholz","year":"1986","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB10","series-title":"Proof Theory of Impredicative Subsystems of Analysis","author":"Buchholz","year":"1988"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB11","doi-asserted-by":"crossref","first-page":"1769","DOI":"10.1090\/S0002-9947-97-01781-9","article-title":"Reversion of power series and the extended Raney coefficients","volume":"349","author":"Cheng","year":"1997","journal-title":"Trans. Amer. Math. Soc."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB12","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/0022-247X(83)90257-3","article-title":"The Lagrange-Good inversion formula and its applications to integral equations","volume":"92","author":"de Bruijn","year":"1983","journal-title":"J. Math. Anal. Appl."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB13","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/1385-7258(77)90067-1","article-title":"Well-partial orderings and hierarchies","volume":"39","author":"de Jongh","year":"1977","journal-title":"Indagationes Math."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB14","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term-rewriting systems","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB15","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","article-title":"Proving termination with multiset orderings","volume":"22","author":"Dershowitz","year":"1979","journal-title":"Comm. ACM"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB16","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1006\/aima.1994.1011","article-title":"A bijective proof of infinite variated Good's inversion","volume":"103","author":"Ehrenborg","year":"1994","journal-title":"Adv. Math."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB17","doi-asserted-by":"crossref","unstructured":"S. Eilenberg, G.M. Kelly, Closed categories, Proc. Conf. on Categorical Algebra, La Jolla, USA, 1965, Springer, Berlin, 1966, pp. 421\u2013562.","DOI":"10.1007\/978-3-642-99902-4_22"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB18","series-title":"Intuitionism and Proof Theory, Proc. Summer Conference at Buffalo, N.Y., 1968","first-page":"303","article-title":"Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis","author":"Feferman","year":"1970"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB19","doi-asserted-by":"crossref","unstructured":"H. Friedman, N. Robertson, P. Seymour, The metamathematics of the graph minor theorem, in: Logic and Combinatorics, Contemporary Mathematics, vol. 65, 1985, AMS, Providence, RI, 1987, pp. 229\u2013261.","DOI":"10.1090\/conm\/065\/891251"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB20","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BF01360719","article-title":"An extension of Sch\u00fctte's klammersymbols","volume":"174","author":"Gerber","year":"1967","journal-title":"Math. Ann."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB21","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1016\/0097-3165(87)90013-6","article-title":"A combinatorial proof of the multivariate Lagrange inversion formula","volume":"45","author":"Gessel","year":"1987","journal-title":"J. Combin. Theory Ser. A"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB22","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0003-4843(81)90016-4","article-title":"\u03a021-logic, part I; dilators","volume":"21","author":"Girard","year":"1981","journal-title":"Ann. Math. Logic"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB23","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0168-0072(88)90025-5","article-title":"Normal functors, power series and \u03bb-calculus","volume":"37","author":"Girard","year":"1988","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB24","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1017\/S0305004100034666","article-title":"Generalization to several variables of Lagrange's expansion, with applications to stochastic processes","volume":"56","author":"Good","year":"1960","journal-title":"Proc. Cambridge Philos. Soc."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB25","series-title":"Ramsey Theory","author":"Graham","year":"1980"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB26","unstructured":"C.A. Gunter, in: Semantics of Programming Languages. Structures and Techniques, Foundations of Computing Series, MIT Press, Cambridge, MA, 1992."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB27","first-page":"133","article-title":"Well-ordering of algebras and Kruskal's theorem","volume":"vol. 792","author":"Hasegawa","year":"1994"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB28","doi-asserted-by":"crossref","unstructured":"M. Hasegawa, Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi, Proc. 3rd Internat. Conf. on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 1210, Springer, Berlin, 1997, pp. 196\u2013213.","DOI":"10.1007\/3-540-62688-3_37"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB29","unstructured":"M. Hasegawa, Models of Sharing Graphs: A categorical semantics of let and letrec, Ph.D. Thesis, The University of Edinburgh, 1997."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB30","unstructured":"R. Hasegawa, The generating function of lambda terms, a preliminary version appeared, in: D.S. Bridges, C.S. Claude, J. Gibbons, S. Reeves, I.H. Witten (Eds.), Combinatorics, Complexity & Logic, proc. DMTCS\u201996, Auckland, New Zealand, 1997, Springer, Berlin, 1997, pp. 253\u2013263, to appear."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB31","first-page":"283","article-title":"An analysis of divisibility orderings and recursive path orderings","volume":"vol. 1345","author":"Hasegawa","year":"1997"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB32","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","article-title":"Ordering by divisibility in abstract algebras","volume":"2","author":"Higman","year":"1952","journal-title":"Proc. London Math. Soc. 3rd Ser."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB33","doi-asserted-by":"crossref","first-page":"803","DOI":"10.1080\/00927879808826165","article-title":"Reversion of power series by residues","volume":"26","author":"Huang","year":"1998","journal-title":"Comm. Algebra"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB34","series-title":"Intuitionism and Proof Theory, Proc. Summer Conf. at Buffalo, New York, USA, 1968","first-page":"339","article-title":"Regular ordinals and normal forms","author":"Isles","year":"1970"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB35","series-title":"Topos Theory","author":"Johnstone","year":"1977"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB36","volume":"vol. 3","author":"Johnstone","year":"1982"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB37","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0001-8708(81)90052-9","article-title":"Une th\u00e9orie combinatoire des s\u00e9ries formelles","volume":"42","author":"Joyal","year":"1981","journal-title":"Adv. Math"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB38","first-page":"126","article-title":"Foncteurs analytiques et esp\u00e8ces de structures","volume":"vol. 1234","author":"Joyal","year":"1986"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB39","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1006\/aima.1993.1055","article-title":"Braided tensor categories","volume":"102","author":"Joyal","year":"1993","journal-title":"Adv. Math."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB40","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1017\/S0305004100074338","article-title":"Traced monoidal categories","volume":"119","author":"Joyal","year":"1996","journal-title":"Math. Proc. Cambridge Philos. Soc."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB41","first-page":"210","article-title":"Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture","volume":"95","author":"Kruskal","year":"1960","journal-title":"Trans. Amer. Math. Soc."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB42","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0012-365X(92)90371-L","article-title":"On asymmetric structures","volume":"99","author":"Labelle","year":"1992","journal-title":"Discrete Math."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB43","unstructured":"J. Lambek, P.J. Scott, in: Introduction to Higher Order Categorical Logic, Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, Cambridge, 1986."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB44","series-title":"9th Colloquium on Trees in Algebra and Programming, Bordeaux, France, 1984","first-page":"181","article-title":"Uniform termination of term rewriting systems, recursive decomposition ordering with status","author":"Lescanne","year":"1984"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB45","series-title":"Categories for the Working Mathematician","author":"Mac Lane","year":"1971"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB46","unstructured":"U. Martin, E. Scott, The order types of termination orderings on monadic terms, strings and multisets, in: Proc. 8th Annual IEEE Symp. on Logic in Computer Science, Montreal, Canada, 1992, New York, IEEE, 1993, pp. 356\u2013363."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB47","doi-asserted-by":"crossref","unstructured":"C.R. Murthy, J.R. Russell, A constructive proof of Higman's lemma, Proc. 5th Annual Symp. on Logic in Computer Science, IEEE, New York, 1990, pp. 257\u2013267.","DOI":"10.1109\/LICS.1990.113752"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB48","doi-asserted-by":"crossref","first-page":"833","DOI":"10.1017\/S0305004100003844","article-title":"On well-quasi-ordering finite trees","volume":"59","author":"Nash-Williams","year":"1963","journal-title":"Proc. Cambridge Philos. Soc."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB49","doi-asserted-by":"crossref","unstructured":"C.-H.L. Ong, Correspondence between operational and denotational semantics: the full abstraction problem for PCF, Handbook of Logic in Computer Science, vol. 4, Oxford University Press, Oxford, 1995, pp. 269\u2013356.","DOI":"10.1093\/oso\/9780198537809.003.0003"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB50","doi-asserted-by":"crossref","unstructured":"G.D. Plotkin, LCF considered as a programming language, Theoret. Comput. Sci. 5 (1977\/78) 223\u2013255.","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB51","series-title":"Proof Theory, Leeds Proof Theory, Leeds, UK, 1990","first-page":"27","article-title":"A short course in ordinal analysis","author":"Pohlers","year":"1992"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB52","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0095-8956(90)90120-O","article-title":"Graph minors, IV. Tree-width and well-quasi-ordering","volume":"48","author":"Robertson","year":"1990","journal-title":"J. Combin. Theory Ser. B"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB53","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0095-8956(90)90121-F","article-title":"Graph minors. VIII. A Kuratowski theorem for general surfaces","volume":"48","author":"Robertson","year":"1990","journal-title":"J. Combin. Th., Ser. B"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB54","series-title":"An Introduction to the Theory of Groups","author":"Rotman","year":"1995"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB55","unstructured":"K. Sakai, Knuth-Bendix algorithm for Thue system based on kachinuki ordering, ICOT Technical Memorandum: TM-0087, ICOT, Institute for New Generation Computer Technology, Dec. 1984."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB56","unstructured":"I. Satake, Linear Algebra, Suugaku Sensho, vol 1, Shoukabou, 1958 (in Japanese)."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB57","first-page":"97","article-title":"Continuous Lattices","volume":"vol. 274","author":"Scott","year":"1972"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB58","first-page":"461","article-title":"Reverse mathematics","volume":"vol. 42","author":"Simpson","year":"1985"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB59","series-title":"Harvey Friedman's Research on the Foundations of Mathematics","first-page":"87","article-title":"Nonprovability of certain combinatorial properties of finite trees","author":"Simpson","year":"1985"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB60","doi-asserted-by":"crossref","first-page":"961","DOI":"10.2307\/2274585","article-title":"Ordinal numbers and the Hilbert basis theorem","volume":"53","author":"Simpson","year":"1988","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB61","unstructured":"G. Takeuti, in: Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 81, North-Holland, Amsterdam, 1975."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB62","first-page":"155","article-title":"Quantitative domains, groupoids and linear logic","volume":"vol. 389","author":"Taylor","year":"1989"},{"key":"10.1016\/S0304-3975(00)00349-2_BIB63","unstructured":"M. Yasugi, Hyperprinciple and the functional structure of ordinal diagrams, Comment. Math. Univ. Sancti Pauli 34 (1985) 227\u2013263; Continuation 35 (1986) 1\u201338."},{"key":"10.1016\/S0304-3975(00)00349-2_BIB64","first-page":"351","article-title":"The calculus of virtual species and K-species","volume":"vol. 1234","author":"Yeh","year":"1986"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500003492?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500003492?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T17:22:28Z","timestamp":1703956948000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500003492"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,2]]},"references-count":64,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2002,2]]}},"alternative-id":["S0304397500003492"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00349-2","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2002,2]]}}}