{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,26]],"date-time":"2025-08-26T06:38:54Z","timestamp":1756190334833,"version":"3.41.0"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,4,30]],"date-time":"2017-04-30T00:00:00Z","timestamp":1493510400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1319212, DGE-1433817 and DUE-1241772"],"award-info":[{"award-number":["CNS-1319212, DGE-1433817 and DUE-1241772"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2017,4,30]]},"abstract":"<jats:p>Uniqueness of normal forms (UN<jats:sup>=<\/jats:sup>) is an important property of term rewrite systems. UN<jats:sup>=<\/jats:sup>is decidable for ground (i.e., variable-free) systems and undecidable in general. Recently, it was shown to be decidable for linear, shallow systems. We generalize this previous result and show that this property is decidable for shallow rewrite systems, in contrast to confluence, reachability, and other related properties, which are all undecidable for flat systems. We also prove an upper bound on the complexity of our algorithm. Our decidability result is optimal in a sense, since we prove that the UN<jats:sup>=<\/jats:sup>property is undecidable for two classes of linear rewrite systems: left-flat systems in which right-hand sides are of height at most two and right-flat systems in which left-hand sides are of height at most two.<\/jats:p>","DOI":"10.1145\/3060144","type":"journal-article","created":{"date-parts":[[2017,6,5]],"date-time":"2017-06-05T12:50:00Z","timestamp":1496667000000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Uniqueness of Normal Forms for Shallow Term Rewrite Systems"],"prefix":"10.1145","volume":"18","author":[{"given":"Nicholas R.","family":"Radcliffe","sequence":"first","affiliation":[{"name":"University of Houston"}]},{"given":"Luis F. T.","family":"Moraes","sequence":"additional","affiliation":[{"name":"University of Houston"}]},{"given":"Rakesh M.","family":"Verma","sequence":"additional","affiliation":[{"name":"University of Houston"}]}],"member":"320","published-online":{"date-parts":[[2017,6,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1043"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322228"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-009-0097-1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_5"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"G. Godoy A. Tiwari and R. Verma . 2003 . On the confluence of linear shallow rewrite systems. Proceedings of the Symposium on Theoretical Aspects of Computer Science Lecture Notes in Computer Science . 85--96. G. Godoy A. Tiwari and R. Verma. 2003. On the confluence of linear shallow rewrite systems. Proceedings of the Symposium on Theoretical Aspects of Computer Science Lecture Notes in Computer Science. 85--96.","DOI":"10.1007\/3-540-36494-3_9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.04.005"},{"volume-title":"Handbook of Logic in Computer Science.","author":"Klop J. W.","key":"e_1_2_1_8_1","unstructured":"J. W. Klop . 1992. Rewrite systems . In Handbook of Logic in Computer Science. Oxford . J. W. Klop. 1992. Rewrite systems. In Handbook of Logic in Computer Science. Oxford."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803406"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/647191.720319"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11856290_8"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.12"},{"volume-title":"Proceedings of the Conference on Foundations of Software Technology 8 Theoretical Computer Science. 284--295","author":"Radcliffe N.","key":"e_1_2_1_13_1","unstructured":"N. Radcliffe and Rakesh M. Verma . 2010. Uniqueness of normal forms is decidable for shallow term rewrite systems . In Proceedings of the Conference on Foundations of Software Technology 8 Theoretical Computer Science. 284--295 . N. Radcliffe and Rakesh M. Verma. 2010. Uniqueness of normal forms is decidable for shallow term rewrite systems. In Proceedings of the Conference on Foundations of Software Technology 8 Theoretical Computer Science. 284--295."},{"volume-title":"Term Rewriting Systems","key":"e_1_2_1_14_1","unstructured":"Terese. 2003. Term Rewriting Systems . Cambridge University Press , Cambridge . Terese. 2003. Term Rewriting Systems. Cambridge University Press, Cambridge."},{"key":"e_1_2_1_15_1","first-page":"1","article-title":"Complexity of normal form problems and reductions for term rewriting problems","volume":"92","author":"Verma Rakesh","year":"2009","unstructured":"Rakesh Verma . 2009 . Complexity of normal form problems and reductions for term rewriting problems . Fund. Info. 92 , 1 -- 2 (2009), 145--168. Rakesh Verma. 2009. Complexity of normal form problems and reductions for term rewriting problems. Fund. Info. 92, 1--2 (2009), 145--168.","journal-title":"Fund. Info."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.11.012"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","first-page":"257","DOI":"10.3233\/FUN-2001-46305","article-title":"Algorithms and reductions for rewriting problems","volume":"46","author":"Verma R.M.","year":"2001","unstructured":"R.M. Verma , M. Rusinowitch , and D. Lugiez . 2001 . Algorithms and reductions for rewriting problems . Fundamenta Informaticae 46 , 3 (2001), 257 -- 276 ; also in Proceedings of the International Conference on Rewriting Techniques and Applications 1998. R.M. Verma, M. Rusinowitch, and D. Lugiez. 2001. Algorithms and reductions for rewriting problems. Fundamenta Informaticae 46, 3 (2001), 257--276; also in Proceedings of the International Conference on Rewriting Techniques and Applications 1998.","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the of 9th Workshop on Rule-based Programming (RULE\u201908)","author":"Verma Rakesh M.","year":"2008","unstructured":"Rakesh M. Verma . 2008 . New undecidability results for properties of term rewrite systems . In Proceedings of the of 9th Workshop on Rule-based Programming (RULE\u201908) . Rakesh M. Verma. 2008. New undecidability results for properties of term rewrite systems. In Proceedings of the of 9th Workshop on Rule-based Programming (RULE\u201908)."},{"volume-title":"Proceedings of the IEEE Conference on Logic in Computer Science.","author":"Zinn J.","key":"e_1_2_1_19_1","unstructured":"J. Zinn and R. Verma . 2006. A polynomial-time algorithm for uniqueness of normal forms of linear, shallow rewrite systems . In Proceedings of the IEEE Conference on Logic in Computer Science. J. Zinn and R. Verma. 2006. A polynomial-time algorithm for uniqueness of normal forms of linear, shallow rewrite systems. In Proceedings of the IEEE Conference on Logic in Computer Science."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-010-0133-1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3060144","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3060144","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3060144","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:56:38Z","timestamp":1750290998000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3060144"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,30]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,4,30]]}},"alternative-id":["10.1145\/3060144"],"URL":"https:\/\/doi.org\/10.1145\/3060144","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2017,4,30]]},"assertion":[{"value":"2016-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-06-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}