Managing structural information by higher-order colored unification

Coloring terms (rippling) is a technique developed for inductive theorem proving that uses syntactic differences of terms to guide the proof search. Annotations (colors) to symbol occurrences in terms are used to maintain this information. This technique has several advantages; for example, it is highly goal oriented and involves little search. In this paper we give a general formalization of coloring terms in a higher-order setting. We introduce a simply typed λ calculus with color annotations and present appropriate algorithms for the general, pre-, and pattern unification problems. Our work is a formal basis to the implementation of rippling in a higher-order setting, which is required, for example, in the case of middle-out reasoning. Another application is in the construction of natural the language semantics, where the color annotations role out linguistically invalid readings that are possible using standard higher-order unification.