Manipulating Tree Tuple Languages by Transforming Logic Programs

We introduce inductive definitions over language expressions as a framework for specifying tree tuple languages. Inductive definitions and their sub-classes correspond naturally to classes of logic programs, and operations on tree tuple languages correspond to the transformation of logic programs. We present an algorithm based on unfolding and definition introduction that is able to deal with several classes of tuple languages in a uniform way. Termination proofs for clause classes translate directly to closure properties of tuple languages, leading to new decidability and computability results for the latter.