ALWAYS HALTING PROGRAM SCHEME

COROLLARY 3.9 Strong equivalence is decidable for always halting program schemes. 

COROLLARY 5.4 If P is an always halting program scheme we can construct a quantifier-free well-formed formula p(P) such that P is totally correct with respect to TRUE and p(P). ... 

We can show for always halting recursion schemes as we showed for always halting program schemes that there is a uniform bound on the length of any computation and hence on the length of the output under any free interpretation. 

DEFINITION A program scheme P baits for all interpretations or P always halts if (P,I) halts everywhere for all, interpretations I. The termination problem for P is the problem of determining whether P always halts. 

Let P be any program scheme. Using our algorithm for testing whether a path is an execution sequence, we construct a tree T(P) of all possible execution sequences for P under free interpretations. The tree T(P) may be finite or infinite our main result on the subject will say that T(P) is finite if and only if P is always halting. The nodes of T(P) are labelled with execution sequences. At level n (declaring the root or initial node to be at level 1)... 

A scheme which is known to be always halting can be effectively transformed into a strongly equivalent tree program scheme. Hence ... 

THEOREM 3.12 If P is an always halting scheme we can construct a strongly equivalent free tree program scheme. 

Fact (3) is also true for lanov schemes. For arbitrary monadic one input one output program schemes it is possible to have L (S) = L (S ) with S not strongly equivalent to S even if S is lanov and S always halting. For an example consider the schemes below ... 

---