Interpolation theorems for program schemata

A schema is thought of as determining a class of structures—namely, those interpretations for the schema for which a convergent computation occurs. (This view is analogous to the ordinary use of first-order formulas to determine a class of structures.) Model theoretic questions, such as compactness, have been explored in this context. This paper answers the question of whether or not the Craig Interpolation Theorem holds for program schemata, and for several extensions of program schemata. It is shown that, in a certain setting, there is a trade-off between implicit versus explicit definition and bounded versus unbounded storage requirements