{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:11Z","timestamp":1747173431106,"version":"3.40.5"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2020,5,22]],"date-time":"2020-05-22T00:00:00Z","timestamp":1590105600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2020,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We consider matching, rewriting, critical pairs and the Knuth\u2013Bendix confluence test on rewrite rules in a nominal setting extended by atom-variables. We utilize atom-variables instead of atoms to formulate and rewrite rules on constrained expressions, which is an improvement of expressiveness over previous approaches. Nominal unification and nominal matching are correspondingly extended. Rewriting is performed using nominal matching, and computing critical pairs is done using nominal unification. We determine the complexity of several problems in a quantified freshness logic. In particular we show that nominal matching is <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129520000122_inline1.png\"\/><jats:tex-math>\n$$\\prod _2^p$$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-complete. We prove that the adapted Knuth\u2013Bendix confluence test is applicable to a nominal rewrite system with atom-variables, and thus that there is a decidable test whether confluence of the ground instance of the abstract rewrite system holds. We apply the nominal Knuth\u2013Bendix confluence criterion to the theory of monads and compute a convergent nominal rewrite system modulo alpha-equivalence.<\/jats:p>","DOI":"10.1017\/s0960129520000122","type":"journal-article","created":{"date-parts":[[2020,5,22]],"date-time":"2020-05-22T08:18:35Z","timestamp":1590135515000},"page":"710-735","source":"Crossref","is-referenced-by-count":3,"title":["Rewriting with generalized nominal unification"],"prefix":"10.1017","volume":"30","author":[{"given":"Yunus","family":"Kutz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8809-7385","authenticated-orcid":false,"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2020,5,22]]},"reference":[{"volume-title":"Haskell 98 Language and Libraries: The Revised Report","year":"2003","author":"Peyton Jones","key":"S0960129520000122_ref19"},{"key":"S0960129520000122_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9164-3"},{"key":"S0960129520000122_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673"},{"key":"S0960129520000122_ref28","unstructured":"Suzuki, T. , Kikuchi, K. , Aoto, T. and Toyama, Y. (2016). Critical pair analysis in nominal rewriting. In: SCSS, 156\u2013168."},{"key":"S0960129520000122_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"S0960129520000122_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59451-5_2"},{"key":"S0960129520000122_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_21"},{"key":"S0960129520000122_ref13","unstructured":"Hamana, M. (2017). How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation. Proceedings of the ACM on Programming Languages 1 (ICFP) 22:1\u201322:28."},{"volume-title":"Computational Complexity","year":"1994","author":"Papadimitriou","key":"S0960129520000122_ref18"},{"key":"S0960129520000122_ref27","unstructured":"Suzuki, T. , Kikuchi, K. , Aoto, T. and Toyama, Y. (2015). Confluence of orthogonal nominal rewriting systems revisited. In: 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"S0960129520000122_ref7","unstructured":"Cheney, J. (2004). Nominal Logic Programming. PhD thesis, Cornell University."},{"key":"S0960129520000122_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"S0960129520000122_ref24","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.66"},{"key":"S0960129520000122_ref25","unstructured":"Schmidt-Schau\u00df, M. and Sabel, D. (2018). Nominal unification with atom and context variables. In: Kirchner, H. (ed.) 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9\u201312, 2018, Oxford, UK, LIPIcs, vol. 108, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 28:1\u201328:20."},{"key":"S0960129520000122_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45220-1_41"},{"key":"S0960129520000122_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2003476.2003492"},{"key":"S0960129520000122_ref16","unstructured":"Knuth, D. and Bendix, P. B. (1970). Simple word problems in universal algebra. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, Pergamon Press, 263\u2013297."},{"key":"S0960129520000122_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.07.004"},{"key":"S0960129520000122_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2893582.2893594"},{"key":"S0960129520000122_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2018.04.003"},{"key":"S0960129520000122_ref20","unstructured":"Peyton Jones, S. L. , Gordon, A. and Finne, S. (1996). Concurrent Haskell. In Proceedings of 23rd ACM POPL 1996, ACM, 295\u2013308."},{"key":"S0960129520000122_ref17","unstructured":"Levy, J. and Villaret, M. (2010). An efficient nominal unification algorithm. In: Lynch, C. (ed.) Proceedings of 21st RTA, LIPIcs, vol. 6, Schloss Dagstuhl, 209\u2013226."},{"key":"S0960129520000122_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.12.002"},{"key":"S0960129520000122_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45260-5_8"},{"key":"S0960129520000122_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.06.016"},{"key":"S0960129520000122_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.05.012"},{"key":"S0960129520000122_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.06.004"},{"key":"S0960129520000122_ref14","unstructured":"Haskell-community (2019). Haskell Main Website. www.haskell.org."},{"key":"S0960129520000122_ref30","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:14)2012"},{"key":"S0960129520000122_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_12"},{"key":"S0960129520000122_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1013963.1013978"},{"key":"S0960129520000122_ref10","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.34.5"},{"key":"S0960129520000122_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_7"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129520000122","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T08:51:20Z","timestamp":1605257480000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129520000122\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,22]]},"references-count":33,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["S0960129520000122"],"URL":"https:\/\/doi.org\/10.1017\/s0960129520000122","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2020,5,22]]}}}