On Classes of Program Schemata

We define the following classes of program schemata: P = class of schemes using a finite number of simple variables; PA = class of schemes using simple and subscripted variables (arrays); P_Ae = class of schemes in PA =, with the addition of an equality test on subscript values; PR = class of schemes allowing recursive functions; PL = class of schemes allowing labels as values; PM = class of schemes allowing a finite number of special markers as values; P_pds = class of schemes using pushdown stores. With these, we can also discuss, for example, P_AM, the class of schemes allowing arrays, and special markers as values ; and P_AL, the class of schemes allowing arrays, and labels as values. We argue that PA, PR, and PL faithfully represent mechanisms of subscripting, recursion, and labels as values, that are present in many “real” programming languages. We show that \[ {P} < {P}R < {P}A ≡ {P}_{{AM}} ≡ {P}_{{pdsM}} ≡ {P}_{{Ae}} ≡ {EF}, \] where EF is Strong’s class of effective functionals, assuming total functions and predicates. The inclusions P < PR < PA and equivalences P_AL ≡ P_AM ≡ P_pdsM ≡ P_Ae are effective. For example, given a program scheme in P_AM we can construct an equivalent one in P_AL. However, we show that for any scheme in P_AM an equivalent PA scheme exists, but also prove it cannot (in general) be constructed! We conjecture that P_A, P_AL, and equivalent classes are indeed “universal.” The above results assume that the uninterpreted functions and predicates are total. We discuss the problems which arise when they are partial. We define the class of multischemes and outline the relationship between the class P_Ae, multischemes, and Strong’s nondeterministic and deterministic effective functionals.