{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:13:55Z","timestamp":1759637635373,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:p>\n            We study confluence and the Church-Rosser property in term rewriting and \u03bb-calculus with explicit bounds on term sizes and reduction lengths. Given a system\n            <jats:italic>R<\/jats:italic>\n            , we are interested in the lengths of the reductions in the smallest valleys\n            <jats:italic>t<\/jats:italic>\n            \u2192 *\n            <jats:italic>s<\/jats:italic>\n            \u2032 * \u2190\n            <jats:italic>t<\/jats:italic>\n            \u2032 expressed as a function:\n          <\/jats:p>\n          <jats:p>\n            \u2014for confluence a function vs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            (\n            <jats:italic>m<\/jats:italic>\n            ,\n            <jats:italic>n<\/jats:italic>\n            ) where the valleys are for peaks\n            <jats:italic>t<\/jats:italic>\n            \u2190\n            <jats:italic>s<\/jats:italic>\n            \u2192 *\n            <jats:italic>t<\/jats:italic>\n            \u2032 with\n            <jats:italic>s<\/jats:italic>\n            of size at most\n            <jats:italic>m<\/jats:italic>\n            and the reductions of maximum length\n            <jats:italic>n<\/jats:italic>\n            , and\n          <\/jats:p>\n          <jats:p>\n            \u2014for the Church-Rosser property a function cvs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            (\n            <jats:italic>m<\/jats:italic>\n            ,\n            <jats:italic>n<\/jats:italic>\n            ) where the valleys are for conversions\n            <jats:italic>t<\/jats:italic>\n            \u2194 *\n            <jats:italic>t<\/jats:italic>\n            \u2032 with\n            <jats:italic>t<\/jats:italic>\n            and\n            <jats:italic>t<\/jats:italic>\n            \u2032 of size at most\n            <jats:italic>m<\/jats:italic>\n            and the conversion of maximum length\n            <jats:italic>n<\/jats:italic>\n            .\n          <\/jats:p>\n          <jats:p>\n            For confluent Term Rewriting Systems (TRSs), we prove that vs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            is a total computable function, and for linear such systems that cvs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            is a total computable function. Conversely, we show that every total computable function is the lower bound on the functions vs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            (\n            <jats:italic>m<\/jats:italic>\n            ,\n            <jats:italic>n<\/jats:italic>\n            ) and cvs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            (\n            <jats:italic>m<\/jats:italic>\n            ,\n            <jats:italic>n<\/jats:italic>\n            ) for some TRS\n            <jats:italic>R<\/jats:italic>\n            : In particular, we show that for every total computable function \u03c6: N \u2192 N there is a TRS\n            <jats:italic>R<\/jats:italic>\n            with a single term\n            <jats:italic>s<\/jats:italic>\n            such that vs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            (|\n            <jats:italic>s<\/jats:italic>\n            |,\n            <jats:italic>n<\/jats:italic>\n            ) \u2265 \u03c6(\n            <jats:italic>n<\/jats:italic>\n            ) and cvs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            (\n            <jats:italic>n<\/jats:italic>\n            ,\n            <jats:italic>n<\/jats:italic>\n            ) \u2265 \u03c6(\n            <jats:italic>n<\/jats:italic>\n            ) for all\n            <jats:italic>n<\/jats:italic>\n            . For orthogonal TRSs\n            <jats:italic>R<\/jats:italic>\n            we prove that there is a constant\n            <jats:italic>k<\/jats:italic>\n            such that: (a) vs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            (\n            <jats:italic>m<\/jats:italic>\n            ,\n            <jats:italic>n<\/jats:italic>\n            ) is bounded from above by a function exponential in\n            <jats:italic>k<\/jats:italic>\n            and (b) cvs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            (\n            <jats:italic>m<\/jats:italic>\n            ,\n            <jats:italic>n<\/jats:italic>\n            ) is bounded from above by a function in the fourth level of the Grzegorczyk hierarchy. Similarly, for \u03bb-calculus, we show that vs\n            <jats:sub>\n              <jats:italic>R<\/jats:italic>\n            <\/jats:sub>\n            (\n            <jats:italic>m<\/jats:italic>\n            ,\n            <jats:italic>n<\/jats:italic>\n            ) is bounded from above by a function in the fourth level of the Grzegorczyk hierarchy.\n          <\/jats:p>","DOI":"10.1145\/2528934","type":"journal-article","created":{"date-parts":[[2013,12,4]],"date-time":"2013-12-04T14:04:47Z","timestamp":1386165887000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Least upper bounds on the size of confluence and church-rosser diagrams in term rewriting and \u03bb-calculus"],"prefix":"10.1145","volume":"14","author":[{"given":"Jeroen","family":"Ketema","sequence":"first","affiliation":[{"name":"Imperial College London, London, UK"}]},{"given":"Jakob Grue","family":"Simonsen","sequence":"additional","affiliation":[{"name":"University of Copenhagen, Copenhagen, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2013,11,28]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press.   Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press.","key":"e_1_2_1_1_1","DOI":"10.1017\/CBO9781139172752"},{"unstructured":"Barendregt H. P. 1985. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Vol. 103 North-Holland Amsterdam.  Barendregt H. P. 1985. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Vol. 103 North-Holland Amsterdam.","key":"e_1_2_1_2_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.2307\/2695106"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1016\/j.tcs.2008.01.044"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1007\/978-3-642-02930-1_14"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.2307\/2274219"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.5555\/1807662.1807685"},{"doi-asserted-by":"crossref","unstructured":"Fernandez M. 2009. Models of Computation: An Introduction to Computability Theory. Springer.   Fernandez M. 2009. Models of Computation: An Introduction to Computability Theory. Springer.","key":"e_1_2_1_8_1","DOI":"10.1007\/978-1-84882-434-8"},{"unstructured":"Grzegorczyk A. 1953. Some classes of recursive functions. Rozprawy Matematyczne (=Dissertationes Mathematicae). Vol. 4 Polish Academy of Sciences Warsaw.  Grzegorczyk A. 1953. Some classes of recursive functions. Rozprawy Matematyczne (=Dissertationes Mathematicae). Vol. 4 Polish Academy of Sciences Warsaw.","key":"e_1_2_1_9_1"},{"doi-asserted-by":"crossref","unstructured":"Jones N. D. 1997. Computability and Complexity from a Programming Perspective. The MIT Press Cambridge MA.   Jones N. D. 1997. Computability and Complexity from a Programming Perspective. The MIT Press Cambridge MA.","key":"e_1_2_1_10_1","DOI":"10.7551\/mitpress\/2003.001.0001"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1007\/978-3-642-12251-4_20"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the International the Conference on Computer Logic (COLOG'88)","volume":"417","author":"Khasidashvili Z.","year":"1988"},{"volume-title":"Handbook of Logic in Computer Science","author":"Klop J. W.","key":"e_1_2_1_13_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1145\/232627.232639"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/258948.258966"},{"unstructured":"Odifreddi P. 1999. Classical Recursion Theory. Studies in Logic and the Foundations of Mathematics. vol. 143 North-Holland Amsterdam.  Odifreddi P. 1999. Classical Recursion Theory. Studies in Logic and the Foundations of Mathematics. vol. 143 North-Holland Amsterdam.","key":"e_1_2_1_16_1"},{"unstructured":"Papadimitriou C. 1994. Computational Complexity. Addison-Wesley Reading MA.  Papadimitriou C. 1994. Computational Complexity. Addison-Wesley Reading MA.","key":"e_1_2_1_17_1"},{"unstructured":"Rogers H. Jr. 1987. Theory of Recursive Functions and Effective Computability. The MIT Press Cambridge MA.   Rogers H. Jr. 1987. Theory of Recursive Functions and Effective Computability. The MIT Press Cambridge MA.","key":"e_1_2_1_18_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1016\/S0049-237X(09)70143-0"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1007\/BF01621476"},{"unstructured":"Sipser M. 2006. Introduction to the Theory of Computation 2nd Ed. Thomson Course Technology Boston MA.  Sipser M. 2006. Introduction to the Theory of Computation 2 nd Ed. Thomson Course Technology Boston MA.","key":"e_1_2_1_21_1"},{"volume-title":"Proceedings of the 21st International Colloquium on Trees and Algebra in Programming (CAAP'96)","author":"S\u00f8rensen M. H.","series-title":"Lecture Notes in Computer Science","key":"e_1_2_1_22_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.2168\/LMCS-3(4:2)2007"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.5555\/645891.671428"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1016\/0304-3975(79)90007-0"},{"key":"e_1_2_1_26_1","volume-title":"Cambridge Tracts in Theoretical Computer Science","volume":"55","author":"Terese","year":"2003"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1016\/S0304-3975(02)00548-0"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.2307\/2586765"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2528934","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2528934","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:45Z","timestamp":1750231725000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2528934"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1145\/2528934"],"URL":"https:\/\/doi.org\/10.1145\/2528934","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2013,11]]},"assertion":[{"value":"2012-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}