{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"institution":[{"id":[{"id":"https:\/\/ror.org\/03mb6wj31","id-type":"ROR","asserted-by":"publisher"},{"id":"https:\/\/www.isni.org\/000000041937028X","id-type":"ISNI","asserted-by":"publisher"},{"id":"https:\/\/www.wikidata.org\/entity\/Q1640731","id-type":"wikidata","asserted-by":"publisher"}],"name":"Universitat Polit\u00e8cnica de Catalunya","acronym":["UPC"]}],"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T19:50:30Z","timestamp":1769889030953,"version":"3.49.0"},"reference-count":0,"publisher":"Universitat Polit\u00e8cnica de Catalunya","license":[{"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-sa\/3.0\/es\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Term unification is a basic operation in several areas of computer science, specially in those related to logic. Generally speaking, it consists on solving equations over expressions called terms. Depending on the kind of variables allowed to occur in the terms and under which conditions two terms are considered to be equal, several frameworks of unification such as first-order unification, higher-order unification, syntactic unification, and unification modulo theories can be distinguished. \r\nMoreover, other variants of term unification arise when we consider nontrivial representations for terms. In this thesis we study variants of the classic first-order syntactic term unification problem resulting from the introduction of context variables, i.e. variables standing for contexts, and\/or assuming that the input is given in some kind of compressed representation.\r\nMore specifically, we focus on two of such compressed representations: the well-known Directed Acyclic Graphs (DAGs) and Singleton Tree Grammars (STGs). Similarly as DAGs allow compression by exploiting the reusement of repeated instances of a subterm in a term, STGs are a grammar-based compression mechanism based on the reusement of repeated (multi)contexts. An interesting property of the STG formalism is that many operations on terms can be efficiently performed directly in their compressed representation thus taking advantage of the compression also when computing with the represented terms. \r\nAlthough finding a minimal STG representation of a term is computationally difficult, this limitation has been successfully overcome is practice, and several STG-compressors for terms are available. The STG representation has been applied in XML processing and analysis of Term Rewrite Systems. Moreover, STGs are a very useful concept for the analysis of unification problems since, roughly speaking, allow to represent solutions in a succinct but still efficiently verifiable form.<\/jats:p>\n                <jats:p>La unificaci\u00f3 de termes \u00e9s una operaci\u00f3n b\u00e1sica en diverses \u00e0rees de la inform\u00e1tica, especialment en aquelles relacionades amb la l\u00f3gica. En termes generals, consisteix en resoldre equacions sobre expressions anomenades termes. Depenent del tipus de variables que apareguin en els termes i de sota quines condicions dos termes s\u00f3n considerats iguals, podem definir diverses variants del problema d'unificaci\u00f3 de termes. A m\u00e9s a m\u00e9s, altres variants del problema d'unificaci\u00f3 de termes sorgeixen quan considerem representacions no trivials per als termes. S'estudia variants del problema cl\u00e0ssic d'unificaci\u00f3 sint\u00e1ctica de primer ordre resultants de la introducci\u00f3 de variables de context i\/o de l'assumpci\u00f3 de que l'entrada \u00e9s donada en format comprimit. Ens centrem en l'estudi de dues representacions comprimides: els grafs dirigits ac\u00edclics i les gram\u00e0tiques d'arbre singlet\u00f3. Similarment a com els grafs dirigits ac\u00edclics permeten compressi\u00f3 mitjan\u00e7ant el re\u00fas d'inst\u00e0ncies repetides d'un mateix subterme, les gram\u00e0tiques d'arbres singlet\u00f3 s\u00f3n un sistema de compressi\u00f3 basat en el re\u00fas de (multi)contexts. Una propietat interessant d'aquest formalisme \u00e9s que moltes de les operacions comuns sobre termes es poden realizar directament sobre la versi\u00f3 comprimida d'aquests de forma eficient, sense cap mena de descompressi\u00f3 pr\u00e8via. Tot i que trobar una representaci\u00f3 minimal d'un terme amb una gram\u00e1tica singlet\u00f3 \u00e9s una tasca computacionalment dif\u00edcil, aquesta limitaci\u00f3 ha estat resolta de forma satisfact\u00f2ria en la pr\u00e0ctica, hi ha disponibles diversos compressors per a termes. La representaci\u00f3 de termes amb gram\u00e0tiques singlet\u00f3 ha estat \u00fatil per al processament de documents XML i l'an\u00e0lisi de sistemes de reescriptura de termes. Les gram\u00e0tiques singlet\u00f3 s\u00f3n concepte molt \u00fatil per a l'an\u00e0lisi de problemas d'unificaci\u00f3, ja que permeten representar solucions de forma comprimida sense renunciar a que puguin ser verificades de forma eficient. A la primera part d'aquesta tesi s'estudien els problemas d'unificaci\u00f3 i matching de primer ordre sota l'assumpci\u00f3 de que els termes de l'entrada s\u00f3n representats fent servir gram\u00e0tiques singlet\u00f3. Presentem algorismes de temps polin\u00f2mic per a aquests problemas, aix\u00ed com propostes d'implementacions i resultats experimentals. Aquests resultats s'utilitzen m\u00e9s endevant en aquesta tesi per a l'an\u00e0lisi de problemes d'unificaci\u00f3 i matching amb variables de contexte i entrada comprimida. A la resta d'aquesta tesi ens centrem en variants d'unificaci\u00f3 amb variables de contexte, que s\u00f3n un cas particular de variables d'ordre superior. M\u00e9s concretament, a la segona part d'aquesta tesi, ens centrem en un cas particular d'unificaci\u00f3 de contextes on nom\u00e8s es permet una sola variable de context en l'entrada. Aquest problema s'anomena \"one context unification\". Mostrem que aquest problema es pot resoldre en temps polin\u00f2mic indeterminista, no nom\u00e9s quan els termes de l'entrada s\u00f3n representats de forma expl\u00edcita, sino tamb\u00e9 quan es representen fent servir grafs dirigits ac\u00edclics i gram\u00e0tiques singlet\u00f3. Tamb\u00e9 presentem un resultat parcial recent en la tasca de trobar un algorisme de temps polin\u00f2mic per a one context unification. Al final de la tesi, estudiem el problema de matching per a entrades amb variables de contexte, que \u00e9s un cas particular d'unificaci\u00f3 on nom\u00e9s un dels dos termes de cada equaci\u00f3 t\u00e9 variables. En contrast amb el problema general, matching de contextes ha estat classificat com a problema NP-complet. Mostrem que matching de contextes \u00e9s NP-complet fins i tot quan es fan servir gram\u00e0tiques com a formalisme de representaci\u00f3 de termes. Aix\u00f2 implica que afegir compressi\u00f3 no ens porta a un augment dr\u00e0stic de la complexitat del problema. Tamb\u00e9 demostrem que la restricci\u00f3 de matching de contextes on el nombre de variables de contexte est\u00e0 afitat per una constant fixa del problema es pot resoldre en temps polin\u00f2mic, fins i tot quan es fan servir grafs dirigits ac\u00edclics com formalisme de representaci\u00f3 de termes<\/jats:p>","DOI":"10.5821\/dissertation-2117-95490","type":"dissertation","created":{"date-parts":[[2023,10,7]],"date-time":"2023-10-07T01:31:36Z","timestamp":1696642296000},"approved":{"date-parts":[[2014,5,30]]},"source":"Crossref","is-referenced-by-count":0,"title":["Variants of unification considering compression and context variables"],"prefix":"10.5821","author":[{"sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adri\u00e0","family":"Gasc\u00f3n Caro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"3865","container-title":[],"original-title":[],"deposited":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T06:31:53Z","timestamp":1769841113000},"score":1,"resource":{"primary":{"URL":"https:\/\/hdl.handle.net\/2117\/95490"}},"subtitle":[],"editor":[{"given":"Guillem","family":"Godoy Balil","sequence":"first","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.5821\/dissertation-2117-95490","relation":{},"subject":[]}}