Composition Theorems for Generalized Sum and Recursively Defined Types

Composition theorems are tools which reduce reasoning about compound data structures to reasoning about their parts. For example, the truth value of a sentence about the Cartesian product of two structures can be reduced to the truth values of sentences on the components of the product. A seminal example of a compositional theorem is the Feferman-Vaught Theorem [2]. Feferman and Vaught introduced a generalized product construct which encompasses many algebraic constructions on mathematical structures. Their main theorem reduces the first-order theory of generalized products to the first order theory of its factors and the monadic second-order theory of its index structure. Shelah [24] defined the notion of a generalized sum and provided the composition theorem which reduces the monadic second-order theory of the generalized sum to the monadic second-order theories of the summands and of its index structure. An important example of generalized sums is the ordinal sum of linearly ordered sets. In [24] the composition theorem for linear orders was one of the main tools for obtaining remarkable decidability results for the monadic theory of linear orders. In [6] several composition theorems for monadic-second order logic over trees were given. Two important applications of the compositional methods to algebra and logics are related to Electronic Notes in Theoretical Computer Science 123 (2005) 209–211