3
$\begingroup$

This is a question about the decidability of program equivalence.

Primitive recursive functions correspond exactly to the functions that can be implemented on a specific register machine usually named LOOP, see for instance [1].

It is known that the equivalence of LOOP programs is undecidable. The problem is: are two given LOOP programs P and Q equivalent? (i.e. do they implement the same function?)

The interest in reversible (and total) transformations lead to the development of another LOOP-like register language, named SRL (simple register language) whose programs are bijections Z^k --> Z^k, see [2].

One SRL program (with k=2) is

(a) for x {inc y} inc x

This program implements the bijection

x' = x+1
y' = x+y

where x' and y' are the final values of x and y respectively.

(Most LOOP programs are not bijections because of two reasons: - Projection (all registers except one are ignored), say f(x,y)=x - dec x (if x'=0 (after), we can not go backwards; before the execution it could be x=0 or x=1.

Now, the definition of SRL, it is very simple.

Domain: Z={...,-1,0,1,2,...}.

The input and the output are all the (initial and final respectively) values of the registers used by the program.

  instruction         effect

  inc x               increment x by one

  dec x               decrement x by one

  for x {P}           execute x times the SRL program P
                      P can not have "inc x" or "dec x" instructions
                      The value of x is not changed.
                      P is executed x times ("controlled composition")
  P;Q                 Concatenation of two instructions (composition)

(The inverse of "inc x" is "dec x", the inverse of "for x{P}" is "for x {P^{-1}}", the inverse of "P;Q" is "Q^{-1};P^{-1}")

Another SRL program (n,a,b)-> (n',a',b') is

(b) for n{for a{inc b}; for b{inc a}}

The outputs a and b are exponentional (on the input values), they are related to the Fibonacci sequence.

My question is

Is the SRL-EQUIVALENCE decision problem decidable? I've been thinking about that for some time, but I don't know the answer.

Problem: are two given SRL programs P and Q equivalent? (i.e. do they implement the same function?)

References

[1] Meyer and Ritchie, The complexity of loop programs, IBM Watson Research Center, Yorktown Heights

[2] Armando Matos, "Analysis of a simple reversible language", Theoretical Computer Science

$\endgroup$

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.