Tag Archives: Difficulty 5

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

Inequivalence of Loop Programs Without Nesting

This is another one of those “mainly ignore most of the problem” reductions.

The Problem: Inequivalence of Loop Programs Without Nesting.  This is problem PO14 of the appendix.

The description: Given:

  • a set of X variables,
  • a subset Y of X which are “input” variables,
  • a specific output variable x0
  • Two programs P1 and P2 with the commands:
    • x <- y (x gets a copy of y)
    • x <- 0  (x gets set to 0)
    • x<- x + 1 (x is incremented by 1)
    • DO xi {S1 S2..Sn} END  (see below)

.. is there a way to assign the variablse in Y so that P1 and P2 produce different outputs in our output variable x0?

Example: The semantics of the “DO” statement are (they’re better described by Tsichrtizis in his paper) that we execute the loop body a number of times equal to the value of xi (if it is 0, we do not execute the loop at all).  The Si statements can be any program statement except another loop (since we are looking at programs without nesting- even allowing one level of nesting makes this problem undecidable).

So, here are two programs x1 is our input variable and x0 is our output variable:

P1:

x0 <- 0
DO x1
x0 <- x0 + 1
END

P2:

x0 <- x1

These programs are equivalent as long as we do not allow our input values to be negative (which seems to be the convention) because both programs will copy the integer value in x1 into x0 (though P1 does it more slowly).  Suppose we used the alternate P1

P1′:

x0 <- 0
DO x1
x0 <- x0 + 1
x0 <- x0 + 1
END

..this has the effect of making x0‘s value twice the value of x1.  While P1 and P2 will still have the same value in x0 if x1=0, any other value in x1 will result in different outputs, making our programs inequivalent.

Reduction: Constable, Hunt, and Sahni use 3SAT.  The basic idea is to use loops that execute at most once as if statements.  (I don’t think they have a loop that iterates more than once in the whole program).  So for example, they will set up a clause variable Ci that will be set to 1 if any of its literal variables are true with a subprogram like:

Ci <- 0
DO Ci1  (Ci1 is the first literal of clause i)
Ci <- 1 (Technically this is Ci <- 0 followed by Ci <- Ci +1)
END

DO Ci2
Ci <- 1
END

DO Ci3
Ci <- 1
END

..each of the loops will set Ci to 1 if the literal is true, and leave it alone if the literal is false.

So, with that in mind, we take a 3SAT formula and write a program:

  • Our input variables are the variables to the formula.
  • We create the negations of all of the variables in an if statement  (this way we have both positive and negative literals for each variable)
  • We compute all of the Ci variables as above
  • We compute the negations of all of the Ci variables. (we need this because our loop-based if statement can only do things if a variable is 1, not 0)
  • We create a variable P that is initially 1.  If any of the negated Ci variables are 1 (so the regular Ci variable was 0, so the clause was not satisfied), we reset P to 0.  P is our output variable.

This program will output P to 1 if its inputs form a satisfiable arrangement of variables, and will output 0 otherwise.  This is our P1 program.

Our P2 program is a program that always outputs 0.  P1 and P2 will be different if and only if the formula is satisfiable.

Difficulty: 5. The reduction itself is pretty easy- “write a program that sees if the inputs are satisfiable”.  The hard part is realizing that you don’t really use the loop structure as a loop, and that you aren’t searching for an input to make it satisfiable, you’re just using whatever input the SAT instance gives you.

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:

Protected: Partially Ordered Knapsack

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