n this paper we study possibilities of reasoning about
functions over theories of data types which satisfy
certain recursion (or homomorphism) properties, with a
focus on emphasizing possibilities of hierarchical and
modular reasoning in such extensions and combinations thereof.
We start by considering theories of absolutely free data
structures, and continue by studying extensions of such
theories with selectors, with functions which attach scalar
data to the data structures and with additional functions
defined using a certain type of recursion axioms (possibly
having values in a different -- e.g.\ numeric -- domain).
We show that in these cases locality results can be established.
This allows us to reduce the task of reasoning about the class
of recursive functions we consider to reasoning in the
underlying theory of absolutely free data structures
(resp. in a combination of the theory of absolutely free data
structures with the theory attached with the domains of the
additional functions). We then show that similar results can be
obtained if we relax some assumptions about the absolute
freeness of the underlying theory of data types. We investigate
the applications of these ideas in verification and cryptography.