@techreport{RISC6349,author = {David M. Cerna},
title = {{A Special Case of Schematic Syntactic Unification}},
language = {english},
abstract = {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 unifi-
cation 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.},
year = {2021},
institution = {CAS ICS / RISC},
length = {8}
}