Tag Archives: Difficulty 5

Strong Inequivalence for Monadic Recursion Schemes

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:

  1. 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.
  2. 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
  3. 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.

Strong Inequivalence of Ianov Schemes

I’d never heard of “Ianov schemes” before, but we’ll be using them for the next couple of problems, so let’s take a look!

The problem: Strong Inequivalence of Ianov Schemes.  This is problem PO16 of the appendix.

The description: Given two programs with a single variable x and instructions:

  1. x = f(x) (where f is some function from some given set of functions F)
  2. if p(x) goto I1 else goto I2 (p(x) is a boolean predicate from some given set of predicates P, I1 and I2 are instructions in the program)
  3. Halt

Are the two programs not strongly equivalent: Can we find a function from F for each f, a predicate from P for each p, and an initial value for each variable that gives different final values for the variable in both programs?

Example: Here is one similar to what we will need in a minute:

P1:

1: if p(x) then 4 else 2
2: x =  f(x)
3: Halt
4: Halt

P2:

1: Halt

Suppose the only choice for f is f(x)= x+ 1(so, changing the variable).  Then the programs are different if we have a p(x) that will let us get to line 2 in P1.  If our only choice of p is something like “p(x) = true”, then the two programs are always equivalent.  If our set of P is (p(x) = true, p(x) = false), then we can choose a predicate that makes the programs inequivalent.

Reduction: The paper from Constable, Hunt, and Sahni basically does this in two parts.  G&J say to use 3SAT, but this looks to me like DNF Non-Tautology.

First (this is Proposition 2.11), they show how to take a DNF formula and turn it into a program.  The program works as a giant chain of if statements checking each literal in each clause.  If a literal is checked to be false, we move on to the next clause.  If all of the literals in a clause are true, we make it to the first (“+”) halting state.  If none of the clauses make it to the “+” state, we go to the second (“-“) halting state.  This means that the “-” state is only reachable if we do not start with a tautology.

Next (This is part iii of Corollary 2.14 of Theorem 2.13), they show that they can extend this into an Ianov scheme program by making the “+” state be just a halt command (so the variable never gets changed), and the “-” state be:

1: x= f(x)  (Where f is some function that changes x)
2: halt.

So the only way this program is different from the trivial “just halt” program is if we can reach the “-” instruction, which only happens if the formula is not a tautology.

Difficulty: 5. The program to test the non-tautology is not that hard.  As usual, the hardest part is parsing all of the definitions in the problem

Protected: Inequivalence of Loop Programs Without Nesting

This content is password protected. To view it please enter your password below:

Protected: First Order Theory of Equality

This content is password protected. To view it please enter your password below:

Protected: Generalized Satisfiability

This content is password protected. To view it please enter your password below:

Protected: Crossword Puzzle Construction

This content is password protected. To view it please enter your password below:

Protected: Left-Right Hackenbush for Redwood Furniture

This content is password protected. To view it please enter your password below:

Protected: Planar Geography

This content is password protected. To view it please enter your password below:

Protected: Sequential Truth Assignment

This content is password protected. To view it please enter your password below:

Protected: Algebraic Equations over GF[2]

This content is password protected. To view it please enter your password below: