Localizations of Unification Freedom through Matching Directions

In this paper it is performed a thorough theoretical study of unification free logic programs, that is programs in which unification can be replaced by (iterated) matching. We introduce a global framework to study unication freedom, based on the simple concept of matching direction. Furthermore, we develop some syntactical criterions to ensure a program is unification free. For the first time, also optimality of such criterions is analyzed, using the so-called localization tool, that properly formalizes the concept of clause-by-clause criterion. This allows a very precise analysis: two main classes of programs are defined which are shown to be maximal, and one of them is proved to be the greatest subsuming the previous work on the subject. Moreover, these classes result to exhibit surprising connections with functional programs as well.