Context unification and traversal equations

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 λx₁ ⋯ λx_n. t where every x_i 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.