{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,8]],"date-time":"2026-08-08T12:03:03Z","timestamp":1786190583084,"version":"3.56.0"},"reference-count":0,"publisher":"SAGE Publications","issue":"3","license":[{"start":{"date-parts":[[2022,5,5]],"date-time":"2022-05-05T00:00:00Z","timestamp":1651708800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Fundamenta Informaticae"],"published-print":{"date-parts":[[2022,5,5]]},"abstract":"<jats:p>A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. We also provide a nominal unification algorithm for higher-order expressions with recursive let and atom-variables, where we show that it also runs in nondeterministic polynomial time. In addition we prove that there is a guessing strategy for nominal unification with letrec and atom-variable that is a trade-off between exponential growth and non-determinism. Nominal matching with variables representing partial letrec-environments is also shown to be in NP.<\/jats:p>","DOI":"10.3233\/fi-222110","type":"journal-article","created":{"date-parts":[[2022,5,6]],"date-time":"2022-05-06T11:19:50Z","timestamp":1651835990000},"page":"247-283","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":5,"title":["Nominal Unification and Matching of Higher Order Expressions with Recursive Let"],"prefix":"10.1177","volume":"185","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8809-7385","authenticated-orcid":false,"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"first","affiliation":[{"name":"GU Frankfurt, Germany."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4084-7380","authenticated-orcid":false,"given":"Temur","family":"Kutsia","sequence":"additional","affiliation":[{"name":"RISC, JKU Linz, Austria."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5883-5746","authenticated-orcid":false,"given":"Jordi","family":"Levy","sequence":"additional","affiliation":[{"name":"IIIA - CSIC, Spain."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8066-3458","authenticated-orcid":false,"given":"Mateu","family":"Villaret","sequence":"additional","affiliation":[{"name":"IMA, Universitat de Girona, Spain."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5060-502X","authenticated-orcid":false,"given":"Yunus","family":"Kutz","sequence":"additional","affiliation":[{"name":"GU Frankfurt, Germany."}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"179","published-online":{"date-parts":[[2022,5,5]]},"container-title":["Fundamenta Informaticae"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-222110","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-222110","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T06:32:42Z","timestamp":1777444362000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/FI-222110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,5]]},"references-count":0,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,5,5]]}},"alternative-id":["10.3233\/FI-222110"],"URL":"https:\/\/doi.org\/10.3233\/fi-222110","relation":{},"ISSN":["0169-2968","1875-8681"],"issn-type":[{"value":"0169-2968","type":"print"},{"value":"1875-8681","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,5]]}}}