TY - GEN
T1 - Context unification and traversal equations
AU - Levy, Jordi
AU - Villaret, Mateu
PY - 2001
Y1 - 2001
N2 - Context unification was originally denned by H. Comon in ICALP'92, as the problem of finding a unifier for a set of equations containing first-order variables and context variables. These context variables have arguments, and can be instantiated by contexts. In other words, they are second-order variables that are restricted to be instantiated by linear terms (a linear term is a λ-expression λx1 ⋯ λxn. t where every xi occurs exactly once in i). In this paper, we prove that, if the so called rank-bound conjecture is true, then the context unification problem is decidable. This is done reducing context unification to solvability of traversal equations (a kind of word unification modulo certain permutations) and then, reducing traversal equations to word equations with regular constraints.
AB - Context unification was originally denned by H. Comon in ICALP'92, as the problem of finding a unifier for a set of equations containing first-order variables and context variables. These context variables have arguments, and can be instantiated by contexts. In other words, they are second-order variables that are restricted to be instantiated by linear terms (a linear term is a λ-expression λx1 ⋯ λxn. t where every xi occurs exactly once in i). In this paper, we prove that, if the so called rank-bound conjecture is true, then the context unification problem is decidable. This is done reducing context unification to solvability of traversal equations (a kind of word unification modulo certain permutations) and then, reducing traversal equations to word equations with regular constraints.
UR - https://www.scopus.com/pages/publications/33745150214
U2 - 10.1007/3-540-45127-7_14
DO - 10.1007/3-540-45127-7_14
M3 - Conference proceeding
AN - SCOPUS:33745150214
SN - 3540421173
SN - 9783540421177
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 169
EP - 184
BT - Rewriting Techniques and Applications - 12th International Conference, RTA 2001, Proceedings
A2 - Middeldorp, Aart
PB - Springer Verlag
T2 - 12th International Conference on Rewriting Techniques and Applications, RTA 2001
Y2 - 22 May 2001 through 24 May 2001
ER -