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:
- x = f(x) (where f is some function from some given set of functions F)
- 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)
- 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