Solving Proximity Constraints

Proximity relations are binary fuzzy relations that satisfy reflexivity and symmetry properties, but are not transitive. They induce the notion of distance between function symbols, which is further extended to terms. Given two terms, we aim at bringing them “sufficiently close” to each other, by finding an appropriate substitution. We impose no extra restrictions on proximity relations, allowing a term in unification to be close to two terms that themselves are not close to each other. Our unification algorithm works in two phases: first reducing the equation solving problem to constraints over sets of function symbols, and then solving the obtained constraints. Termination, soundness and completeness of both algorithms are shown. The unification problem has finite minimal complete set of unifiers.