A Special Case of Schematic Syntactic Unification

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F21%3A00555404" target="_blank" >RIV/67985807:_____/21:00555404 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1109/SYNASC54541.2021.00024" target="_blank" >http://dx.doi.org/10.1109/SYNASC54541.2021.00024</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/SYNASC54541.2021.00024" target="_blank" >10.1109/SYNASC54541.2021.00024</a>

Jazyk výsledku

angličtina

Název v původním jazyce

A Special Case of Schematic Syntactic Unification

Popis výsledku v původním jazyce

We present a unification problem based on first-order syntactic unification which ask whether every problem in a schematically-defined sequence of unification problems is unifiable, so called loop unification. Alternatively, our problem may be formulated as a recursive procedure calling first-order syntactic unification on certain bindings occurring in the solved form resulting from unification. Loop unification is closely related to Narrowing as the schematic constructions can be seen as a rewrite rule applied during unification, and primal grammars, as we deal with recursive term constructions. However, loop unification relaxes the restrictions put on variables as fresh as well as used extra variables may be introduced by rewriting. In this work we consider an important special case, so called semiloop unification. We provide a sufficient condition for unifiability of the entire sequence based on the structure of a sufficiently long initial segment. It remains an open question whether this condition is also necessary for semiloop unification and how it may be extended to loop unification.

Název v anglickém jazyce

A Special Case of Schematic Syntactic Unification

Popis výsledku anglicky

We present a unification problem based on first-order syntactic unification which ask whether every problem in a schematically-defined sequence of unification problems is unifiable, so called loop unification. Alternatively, our problem may be formulated as a recursive procedure calling first-order syntactic unification on certain bindings occurring in the solved form resulting from unification. Loop unification is closely related to Narrowing as the schematic constructions can be seen as a rewrite rule applied during unification, and primal grammars, as we deal with recursive term constructions. However, loop unification relaxes the restrictions put on variables as fresh as well as used extra variables may be introduced by rewriting. In this work we consider an important special case, so called semiloop unification. We provide a sufficient condition for unifiability of the entire sequence based on the structure of a sufficiently long initial segment. It remains an open question whether this condition is also necessary for semiloop unification and how it may be extended to loop unification.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)

ISBN

978-1-6654-0650-5

ISSN

—

e-ISSN

—

Počet stran výsledku

8

Strana od-do

75-82

Název nakladatele

IEEE

Místo vydání

Piscataway

Místo konání akce

Timisoara / Virtual

Datum konání akce

7. 12. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000786477000013