FREE MONADIC RECURSION SCHEMES

THEOREM 8.14 The strong equivalence problem for free monadic recursion schemes is decidable. 

More specifically, the basic notions of a Turing Machine, of computable functions and of undecidable properties are needed for Chapter VI (Decision Problems) the definitions of recursive, primitive recursive and partial recursive functions are helpful for Section F of Chapter IV and two of the proofs in Chapter VI. The basic facts regarding regular sets, context-free languages and pushdown store automata are helpful in Chapter VIII (Monadic Recursion Schemes) and in the proof of Theorem 3.14. For Chapter V (Correctness and Program Verification) it is useful to know the basic notation and ideas of the first order predicate calculus a highly abbreviated version of this material appears as Appendix A. 

THEOREM 8.1+ The reversal of the interpreted value language of a monadic recursion scheme is a deterministic context-free language. 

Every context-free language is the value language of sane monadic recursion scheme. 

However not every deterministic context-free language - even if it is in the right format - is the reversal of the interpreted value language of some monadic recursion scheme the regular set xO(fO) is an obvious example. 

Scheme P2 in Example VIII-3 shows that a flowchart scheme may not be translatable into a monadic recursion scheme even if the value language is context-free. The reason is that P2 really combines two schemes. If T(x) = 1, P2...

EXAMPLE VIII-4- - Flowchart scheme Pg is not strongly equivalent to any monadic recursion scheme even though (LfCPg))1 is deterministic context-free... 

It is undecidable whether a monadic program scheme is free. But it is fairly easy to see that it is decidable whether a monadic recursion scheme is free. Recall that a monadic recursion scheme S is free if and only if during every computation of S under every free interpretation of S no test T of S is twice applied to the same expression Ex. ... 

If we construct the pushdown store automaton which accepts the reversal of the interpreted value language of a monadic recursion scheme S we see that there are only two cases in which S can fail to be free ... 

THEOREM 8.13 It is decidable whether a monadic recursion scheme is free. 

If a monadic recursion scheme S is free, then neither (1) nor (2) can hold. 

Let S be a monadic recursion scheme. By methods similar to the proof of Chomsky normal form for context-free grammars we can convert the equations of S to the forms ... 

---