Title | Context unification and Traversal Equations |

Publication Type | Conference Paper |

Year of Publication | 2001 |

Authors | Levy J [1], Villaret M [2] |

Conference Name | Lecture Notes in Computer Science |

Volume | 2051 |

Publisher | Springer-Verlag |

Pagination | 169-184 |

Abstract | Context unification was originally defined 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 lambda-expresion lambda x_1...lambda x_n.t where every x_i occurs exactly once in t). 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. |