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