As promised, now we extend the proof of the Ianov Scheme problem to other problems.
The problem: Strong Inequivalence for Monadic Recursion Schemes. This is problem PO17 in the appendix.
The description: Suppose we have a sequence of expressions F1..Fn. Each is of the form:
Fi(x) = if Pi(x) then Ai(x) else Bi(x)
Each Pi is a boolean predicate, each Ai and Bi are compositions of function calls from F or from a given set of “basis” functions f. This is a monadic recursion scheme. A linear monadic recursion scheme adds the requirement that each A and B composition can have at most one call to one of our F functions.
So, similar to our last problem, if we are given a set of basis functions f, a set of predicates P, and two schemes that take a start variable x0 into an initial function F0, can assign functions and predicates to the two schemes to make them have different outputs?
Example: Let’s turn our Ianov Scheme example into this format:
Scheme 1:
F1(x): If P(x) then F2(x), else f( F2(x))
F2(x): If P(x) then x else x
Scheme 2:
F1(x) If P(x) then x else x
Scheme 2 is the identity function- it always returns x. Scheme 1 is the identity when P(x) is true, or when f is itself the identity. So if we have a predicate set of {p(x) = true, p(x) = false} and a function set of {f(x) = x+1}, then we can make Scheme 1 return a different value for its starting variable and thus the two schemes are equivalent.
Reduction: This is the paper by Constable, Hunt, and Sahni again, and in fact builds off of their Ianov Scheme result from last time. The idea is that if we can take any program in that format, and convert it into a recursion scheme, then we have a reduction. So, suppose we are at instruction “j” of the program, which will map to function Fj of our scheme. Recall those programs had three kinds of instructions:
- x=f(x), where f is some function- f will be a basis function in our recursion scheme, and we will create the statement:Fj(x) = If P1(x) then Fj+1(f(x)) else Fj+1(f(x)). This will take us to the next “line” of the program sending f(x) as the variable we are working on.
- If Pk(x) goto I1 else goto I2, then we create the statement:
Fj(x) = If Pk(x) then FI1 else FI2. This will take us to the corresponding “line” of the program we will do next, based on our predicate Pk - Halt. Then we just do:
Fj(x) = x
This turns any program into an equivalent monadic recursion scheme, thus converting our Ianov Scheme problem instance into a monadic recursion scheme instance.
Difficulty: 5. The actual “Write this program as a set of function statements” task isn’t hard. As usual, wrapping your head around the definitions of what the problems are talking about is the difficult part.