{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,21]],"date-time":"2025-10-21T02:50:00Z","timestamp":1761015000018,"version":"3.41.2"},"reference-count":15,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,6]],"date-time":"2012-03-06T00:00:00Z","timestamp":1330992000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Let T be Goedel's system of primitive recursive functionals of finite type in\nthe lambda formulation. We define by constructive means using recursion on\nnested multisets a multivalued function I from the set of terms of T into the\nset of natural numbers such that if a term a reduces to a term b and if a\nnatural number I(a) is assigned to a then a natural number I(b) can be assigned\nto b such that I(a) is greater than I(b). The construction of I is based on\nHoward's 1970 ordinal assignment for T and Weiermann's 1996 treatment of T in\nthe combinatory logic version. As a corollary we obtain an optimal derivation\nlength classification for the lambda formulation of T and its fragments.\nCompared with Weiermann's 1996 exposition this article yields solutions to\nseveral non-trivial problems arising from dealing with lambda terms instead of\ncombinatory logic terms. It is expected that the methods developed here can be\napplied to other higher order rewrite systems resulting in new powerful\ntermination orderings since T is a paradigm for such systems.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:19)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":4,"title":["Derivation Lengths Classification of G\\\"odel's T Extending Howard's Assignment"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4019-9320","authenticated-orcid":false,"given":"Gunnar","family":"Wilken","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5561-5323","authenticated-orcid":false,"given":"Andreas","family":"Weiermann","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,6]]},"reference":[{"key":"10.2168\/LMCS-8(1:19)2012_BW98","unstructured":"Beckmann, A., Weiermann,A.: A term rewriting characterization of the polytime functions and related complexity classes.Archive for Mathematical Logic36: 11-30, 1996."},{"key":"10.2168\/LMCS-8(1:19)2012_BW00","doi-asserted-by":"publisher","DOI":"10.1002\/1521-3870(200010)46:4<517::AI"},{"key":"10.2168\/LMCS-8(1:19)2012_BCW94","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19940400212"},{"key":"10.2168\/LMCS-8(1:19)2012_CH","unstructured":"Cardone, F., Hindley, J.R.: History of\u00ce\u00bb-Calculus and Combinatory Logic. To appear in: Gabbay, D.M., Woods, J. (eds.)Handbook of the History of Logic, vol. 5, Elsevier."},{"key":"10.2168\/LMCS-8(1:19)2012_CW97","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(96)00015-2"},{"key":"10.2168\/LMCS-8(1:19)2012_G58","doi-asserted-by":"crossref","unstructured":"G\u00f6del, K.: \u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes.Dialectica12: 280-287, 1958.","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"10.2168\/LMCS-8(1:19)2012_HinSel86","unstructured":"Hindley, J.R., Seldin, J.P.: Introduction to Combinators and\u00ce\u00bb-Calculus. London Mathematical Society. Cambridge University Press, 1986."},{"key":"10.2168\/LMCS-8(1:19)2012_H70","doi-asserted-by":"crossref","unstructured":"Howard, W.A.: Assignment of Ordinals to Terms For Primitive Recursive Functionals of Finite Type.Intuitionism and Proof Theory, 443-458. North Holland, Amsterdam, 1970.","DOI":"10.1016\/S0049-237X(08)70770-5"},{"key":"10.2168\/LMCS-8(1:19)2012_P72","doi-asserted-by":"publisher","DOI":"10.2307\/2272731"},{"key":"10.2168\/LMCS-8(1:19)2012_P09","unstructured":"Pohlers, W.: Proof Theory. The First Step into Impredicativity. Springer, Berlin, 2009."},{"key":"10.2168\/LMCS-8(1:19)2012_S77","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-66473-1"},{"key":"10.2168\/LMCS-8(1:19)2012_Sh67","unstructured":"Shoenfield, J.R.: Mathematical Logic. Addison-Wesley, New York, 1967."},{"key":"10.2168\/LMCS-8(1:19)2012_W96","doi-asserted-by":"publisher","DOI":"10.2307\/2275597"},{"key":"10.2168\/LMCS-8(1:19)2012_W97","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050075"},{"key":"10.2168\/LMCS-8(1:19)2012_W98","doi-asserted-by":"publisher","DOI":"10.2307\/2586654"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1073\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1073\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:02:59Z","timestamp":1681243379000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1073"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,6]]},"references-count":15,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:19)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1203.0115","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1203.0115","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,3,6]]},"article-number":"1073"}}