Lattice Operations on Terms over Similar Signatures

TL;DR

This paper extends unification and generalization operations to fuzzy signatures with similar functors, providing a declarative, efficient, and practical framework for fuzzy information processing.

Contribution

It introduces a declarative approach to fuzzy term operations that requires no changes to existing data structures and is efficiently executable.

Findings

Extended unification and generalization to fully fuzzy signatures

Declarative axiomatic framework for fuzzy term operations

Efficient implementation using Horn-clauses

Abstract

Unification and generalization are operations on two terms computing respectively their greatest lower bound and least upper bound when the terms are quasi-ordered by subsumption up to variable renaming (i.e., $t_1\preceq t_2$ iff $t_1 = t_2\sigma$ for some variable substitution $\sigma$). When term signatures are such that distinct functor symbols may be related with a fuzzy equivalence (called a similarity), these operations can be formally extended to tolerate mismatches on functor names and/or arity or argument order. We reformulate and extend previous work with a declarative approach defining unification and generalization as sets of axioms and rules forming a complete constraint-normalization proof system. These include the Reynolds-Plotkin term-generalization procedures, Maria Sessa's "weak" unification with partially fuzzy signatures and its corresponding generalization, as well as novel extensions of such operations to fully fuzzy signatures (i.e., similar functors with possibly different arities). One advantage of this approach is that it requires no modification of the conventional data structures for terms and substitutions. This and the fact that these declarative specifications are efficiently executable conditional Horn-clauses offers great practical potential for fuzzy information-handling applications.