Unification Modulo Common List Functions

ABSTRACT. Reasoning about data types is an important research area with many applications, such as formal program verification. Virtually all commonly used programming languages use lists or arrays and for certain Logic Programming languages, formal analysis via unification is a natural fit. Lists are also useful in the study of satisfiability modulo theories, which unification has strong connections to. In this paper, we investigate the unification problem modulo theories of lists. The different theories are obtained by considering observer functions of increasing complexity. These observer functions are right cons, reverse, and fold right (reduce.) In practice reduce is not a first-order function; we turn it into a first-order function by treating the binary function to be "folded" over the list as an uninterpreted function, i.e., as a constructor.