=Paper=
{{Paper
|id=Vol-2243/paper12
|storemode=property
|title=The Fixed Point Problem for General and for Linear SRL Programs is Undecidable
|pdfUrl=https://ceur-ws.org/Vol-2243/paper12.pdf
|volume=Vol-2243
|authors=Armando B. Matos,Luca Paolini,Luca Roversi
|dblpUrl=https://dblp.org/rec/conf/ictcs/MatosPR18
}}
==The Fixed Point Problem for General and for Linear SRL Programs is Undecidable==
https://ceur-ws.org/Vol-2243/paper12.pdf
The xed point problem for general and for linear
SRL programs is undecidable
1 2 2
Armando B. Matos , Luca Paolini , and Luca Roversi
1
University of Porto, Portugal
2
University of Turin, Italy
armandobcm@yahoo.com, luca.paolini@unito.it, luca.roversi@unito.it
Abstract. SRL is a total programming language for reversible comput-
SRL, every program that mentions n registers de nes a bijection
ing. In
Z → Z . Since SRL contains only a very essential set of commands it is
n n
a language suitable for studying strengths and weaknesses of reversible
computations.
We deal with xed points in SRL, i.e. we are interested in the problem
of deciding if there is a tuple of initial register values of a given pro-
gram P that remains unaltered after the execution of P. First, we show
that the existence of xed points in SRL
is undecidable and complete
0
in Σ1 . Second, we show that such problem remains undecidable even
when the number of registers mentioned by the program P is limited
to 12. Moreover, if we restrict to linear programs of SRL, i.e. to those
programs where dierent registers control nested loops, then the problem
is undecidable already when programs mentions 3712 registers.
1 Introduction
Loop languages are an important sub-class of while programming languages (see
for instance [3,6,15]) which characterize the class of primitive recursive functions
[18,19]. The language of [18,19] is the starting point to design the reversible
languages SRL and ESRL de ned in [17] (see also [24]).
Each register contains a value in Z; each program mentioning n registers
n
de nes a bijection Z → Zn . Consider the following SRL programs:
P0 : for x(inc r) P2 : for y(for x(inc r))
P1 : for x(dec r) P3 : for x(for x(dec r))
The program P0 mentions the two registers x and r . If the initial value of x is
strictly positive, P0 eventually increments the initial value of r by (the initial
value of ) x. If the initial value of x is negative, P0 eventually decrements the
initial value of r by x. So, in any case, P0 is the inverse of P1. I.e., running P1
after P0, written as P0; P1, we compute the identity on the tuple (x, r). It is
worth to note that SRL ensures the reversibility by forbidding the modi cation
of a register driving a loop (as x in P0) in the loop-body. P2 iterates P1. The
nal value of r is its initial value plus the product xy . P2 is linear because no
register driving a loop is mentioned in its body. Clearly, P3 is non -linear exactly
for the opposite reason. So, the nal value of r that P3 yields is its initial value
2
plus the square x . The language ESRL extends SRL with the instruction that
exchanges the contents of two registers.
The examples underline the three main aspects that dierentiate both SRL
and ESRL from non-reversible (classic) Loop languages and which ensure they
only compute bijections: (i) a program register may contain any, possibly nega-
tive, integer; (ii) every elementary operation is reversible and (iii) a projection,
like ignoring registers (at output) or eliminating its content, is not allowed. This
is similar, but not completely identical to what happens in Quantum Mechanics.
General forms of cloning copying the content of a register to another and
erasing are not possible. Only some limited versions of them exist. For example,
the fan-out in [28] and the cloning of orthogonal states in [21, page 530] are
limited cloning.
Among the languages whose programs represent exactly reversible functions,
SRL and ESRL [17,23,22] are probably the simplest ones, but they are far from
being trivial. For SRL and similar languages, nding undecidable decision prob-
lems and proving their undecidability is harder than for Loop languages exactly
because SRL is extremely simple.
In this paper, we focus on the xed point problem (shortened to xpoint
problem) for SRL: given a program P, is there an input tuple which is not
modi ed by the execution of P?. We prove that the xpoint problem is unde-
0
cidable and complete in Σ1 . In particular, the undecidability shows up when the
programs mention 12 registers and, in the case of linear programs, when they
mention 3712 registers.
We present a reduction from Hilbert's Tenth Problem (shortened in HTP)
to the xpoint problem. Thus, an eventual algorithm that solves the xpoint
problem would give us an algorithm which, for any given Diophantine equation,
decides whether the equation has a solution with all unknowns taking integer
values (see [16] for more details). But such algorithm does not exist.
We focus on problems related to HTP which look promising for dealing with
the problem we may ask on a programming language: Given P and Q in SRL,
are they equivalent? This question is showed to be undecidable for straight-line
programs by means of a proof that relies on HTP [8,10,9]. Since straight-line
programs can be viewed as a sort of trace-semantics for programs in SRL, we
conjecture that some results on such programs can also hold for SRL.
Contents. Section 2, page 2 contains the background necessary to understand
this work. The main results of this paper are Theorem 1 (page 7, Section 3) and
Theorem 3 (page 10, Section 4). Finally, in Section 5 (page 11) we present some
conclusions and open problems.
2 Preliminaries
The sets of positive integers, non-negative integers, integers, and rational num-
+
bers are denoted by N , N, Z and Q, respectively.
2.1 The language SRL
SRL is a language whose programs work on registers that store values of Z. Each
n
program P of SRL de nes a bijection Z → Zn , where n ∈ N+ is the number
of registers that occur in the de nition of P. Such n registers are said to be
−1
mentioned or used in P. The program P is the inverse of P and computes the
−1
inverse bijection (below we explain how to generate P in an eective manner).
The syntax of SRL-programs relies on four possible constructions: (i) inc x
increments the content of the register x by 1; (ii) dec x decrements the content
of the register x by 1; (iii) P0 ; P1 is the sequential composition of 2 programs;
and, (iv) for r(P) iterates P as many times as the initial contents of r if that
value is positive; otherwise, if r contains a negative value, then the iteration is
−1
on P . Moreover, the constraint that (iv) must satisfy is that neither inc r nor
dec r occur in P, leaving the content of r unchanged.
An SRL-program is linear if in every instruction of the form for r(P), the
program P does not mention the register r . That is, P can contain neither inc r ,
0
nor dec r , nor for r(P ) instructions.
The inverse of an SRL-program is generated by transforming inc x, dec x,
P0 ; P1 and for r(P) in dec x, inc x, P1 −1 ; P0 −1 and for r(P−1 ), respectively. For
more information on SRL and its extensions, as well as results related with that
language, consult for instance [17] and [22].
Example 1. Let P be the program for r(for b(inc a); for a(inc b)). Let a = 0, b = 1,
and r = n be the initial values of the corresponding registers. The nal value
of a is F2n , i.e. the Fibonacci number with index 2n where we take Fk de ned
for every k ∈ Z. (the extension of the de nition of Fk to negative values of k is
straightforward). We remark that F2n is exponential in n. Moreover, the inverse
of P is for r(for a(dec b); for b(dec a)).
De nition 1 (Fixpoint of a program). Let P be a SRL program that men-
tions n registers x = hx1 , . . . , xn i. Let x, a tuple of n integers, denote the initial
values of x. Let P(x) be the tuple of the corresponding nal contents after P is
executed with the initial values x. If P(x) = x, then the tuple x is a xpoint of P.
2.2 Decision problems and reductions
Let A be a predicate, i.e. a function from a set to truth values. A decision problem
related to A is an eective procedure able to say when the answer to A(x)? is
yes, for every x. Let B be also a decision problem. A (many-one) reduction of A
to B , written A ≤ B , is an eective function f which maps every instance x of A
to an instance f (x) of B such that the answer to A(x)? is yes i the answer to
B(f (x))? is yes. The relation ≤ is transitive. If A ≤ B and A is undecidable,
then B is also undecidable [25,5,14,4,1,2,7,26].
De nition 2 (FIXPOINT-decision problem). Let P be a SRL-program then
the FIXPOINT-decision problem is
FIXPOINT(P) ≡ Does P have a xpoint? .
More explicitly, FIXPOINT(P) is equivalent to: Given a SRL program P, is there
a tuple x such that P(x) = x ?.
Moreover, we write l -FIXPOINT(P) whenever P is linear. We mean to ask: Given
a linear SRL program P, is there a tuple x such that P(x) = x?.
Roughly speaking, this paper is about reducing Hilbert's Tenth Problem
[16,12,27,20], also known as the Diophantine decision problem, to FIXPOINT(P)
and to l -FIXPOINT(P). We shall nd a constant c such that, if the number
of registers mentioned by P does not exceed c, the problem FIXPOINT(P) is
undecidable. We also prove analogous results for the problem l -FIXPOINT(P),
that is, when P is linear.
2.3 Polynomials
Let p(x1 , . . . , xn ) be an integer polynomial, i.e. a polynomial with integer co-
e cients and unknowns x1 , . . . , xn . A polynomial is in normal form if: (i) it is
a sum of monomials; (ii) each monomial has form cx1 x2 . . . xekk where c 6= 0
e1 e2
is a constant, the unknowns x1 ,. . . , xk are pairwise distinct, and ei ≥ 1, for
every 1 ≤ i ≤ k ; (iii) no two monomials have the same unknowns with the same
exponents.
2 2
For instance, 3x y+y −yx2 +5 is not in normal form. The unique normal form
of a given p(x1 , . . . , xn ) can be obtained by sorting in lexicographic order: (i) the
unknowns within each monomial, and (ii) the monomials of the polynomial. For
2
example, the normal form of 3xy(z + y ) + 2z − 3y 3 x is 3xyz + 2z . We shall often
omit exponents equal to 1 as well as monomial coe cients c equal to 1. The null
polynomial is denoted by 0.
De nition 3. For any polynomial p(x1 , . . . , xn ) in normal form, we identify:
u(p) the number of unknowns
deg(xi ) the maximum degree of the unknown xi
deg(p) the maximum among deg(x1 ) . . . deg(xn )
d(p) the maximum degree of a monomial of p,
or the degree of the polynomial p.
Example 2. Let p(x, y, z) = xy 3 z + 2xyz 3 − z 4 . The polynomial p has three
unknowns x, y and z , so u(p) = 3. The unknowns occur with various degrees in
distinct monomials, but the maximal exponents are deg(x) = 1, deg(y) = 3 and
deg(z) = 4. So 4 = deg(p) = deg(z). Finally, d(p) = 5, given by summing up all
3
the exponents of 2xyz .
2.4 Hilbert's Tenth Problem and the Diophantine equation
problem.
+
Let D be one among N , N, Z or Q. As said, we shorten Hilbert's Tenth Problem
by HTP. Its question about a given polynomial p(x1 , . . . , xn ) is:
HTP(D)(p) ≡ Does a tuple x1 , . . . , xn of values in D exist
such that p(x1 , . . . , xn ) = 0?
HTP(D) can be straightforwardly generalized to questions on a set of integer
polynomials {p1 (x1 , . . . , xn ), . . . , pm (x1 , . . . , xn )} as follows:
HTP(D)(p1 , . . . , pm ) ≡ Does a tuple x1 , . . . , xn of values in D exist
such that pi (x1 , . . . , xn ) = 0, for every 1 ≤ i ≤ m ?
The di culty of solving HTP(D) depends on D [16, (1.3.1)],[13,12,20]. If
a given HTP(D) problem is undecidable, we can look for the least number of
unknowns and the least degrees which su ce to keep HTP(D) undecidable. To
our knowledge [27] contains the latest (very recent) improvements concerning
the bounds on that number of unknowns. I.e., for a single equation, HTP(Z) is
undecidable for polynomials with at least 11 unknowns.
De nition 4. If the system of equations consists of a single equation, then
Equ(D) is our favourite notations for HTP(D). Instead, the notation Sys(D)
underlines that the given instance of HTP(D) has more than one Diophantine
equation.
3 Properties of the xpoint problem for SRL
The rst part of this section focuses on proving the next theorem.
Theorem 1. The problem FIXPOINT as in De nition 2 (page 3), is undecidable
0
and complete in Σ1 .
Proving Theorem 1
The strategy is to reduce Equ(Z), i.e. HTP(Z) that deals with a single Diophan-
tine equation, to FIXPOINT. We show how by means of a signi cant running
example. The example illustrates how to map a polynomial to a program of
SRL. The general case will follow easily. Let p(x, y) be the polynomial:
p(x, y) = 2x3 y 2 − xy 2 + 2. (1)
We map p(x, y) to the program P(p), namely the sequential composition of the
following three lines of code:
for x(for x(for x(for y(for y(inc s; inc s))))); (A)
for x(for y(for y(dec s))); (B)
inc s; inc s. (C)
Line (A) updates the content of s in accordance with the assignment:
s ← s + 2x3 y 2 . (2)
3
The factor x follows from the three nested iterations driven by x. Analogously,
2
the two nested iterations driven by y yield the factor y . Factor 2 comes from
inc s; inc s. Under the same idea, lines (B) and (C) produce:
s ← s − xy 2 (3)
s ← s + 2, (4)
respectively. The overall eect of P(p) is thus to update the initial value of s
with the value of (1), for every xed value of x and y .
Concerning the general case, for any polynomial p, the corresponding P(p)
uses as many registers as the number of unknowns of p, plus one register s which
is incremented by the value of p(x, y).
Every monomial of p is transformed in blocks of iterations nested as many
times as required to obtain the corresponding exponents. The nested blocks
eventually operate on a program that only contains sequences of inc s, or dec s,
which determine the constant multiplicative factor of the monomial.
We are now ready to comment on how P(p) has a xpoint, if, and only if,
p(x, y) = 0 has a solution, following our running example.
If P(p) has a xpoint, then p(x, y) = 0 has a solution.
Let us assume that the tuple (x, y, s) used as input for the registers (x, y, s) is
a xpoint of P(p). The execution of P(p) from (x, y, s) let us denote it as
P(p)(x, y, s) necessarily replaces the value s + 2x3 y2 − xy2 + 2 for s. We can
formalize the overall eect as follows:
P(p)(x, y, s) = (x, y, s + 2x3 y2 − xy2 + 2).
3 2
Being (x, y, s) a xpoint of P(p), we must have s = s + 2x y − xy2 + 2 which is
3 2 2
possible only if 2x y −xy +2 = 0 = p(x, y). Thus (x, y) is a solution of p(x, y)=0.
If p(x, y) = 0 has a solution, then P(p) has a xpoint.
Let us assume that the tuple (x, y) is a solution of p(x, y) = 0. Execute P(p)(x, y, s),
i.e. the program P(p) whose variables (x, y, s) assume the initial values x, y and
s, respectively, with some arbitrarily xed value s. Then:
P(p)(x, y, s) = (x, y, s + 2x3 y2 − xy2 + 2) = (x, y, s + p(x, y))
= (x, y, s + 0) = (x, y, s),
0
which means that (x, y, s) is a xpoint of P(p). Since Equ(Z) is Σ1 -complete [25],
also FIXPOINT is, and this concludes the justi cation to Theorem 1.
We now proceed to the strengthening of Theorem 1. In [27, Part 1: Corol-
lary 1.1 (p. 5)] it is stated that the problem Equ(Z) keeps being undecidable even
if the number of unknowns of the polynomials of Equ(Z) does not exceed 11.
Since we know how to reduce Equ(Z) to FIXPOINT in the general case, and in
this reduction the number of program registers equals the number of unknowns
plus 1 (2 + 1 = 3 in our running example), we can improve our result.
Corollary 1. FIXPOINT is undecidable and complete in Σ10 already when FIX-
POINT contain programs that mention 12 registers.
4 Properties of the linear xpoint problem for SRL
Let us recall from Section 2 that a program P of SRL is linear, if nested iterations
driven by the same register are forbidden.
De nition 5 (Linear SRL programs). Let n ∈ N. Then l-SRL(n) denotes the
subset of linear SRL programs that use no more than n registers.
The rst part of this section focuses on the next theorem.
Theorem 2. The problem l -FIXPOINT is undecidable and complete in Σ10 .
It corresponds to Theorem 1 (page 5). The proof strategy reduces Equ(Z)
to l -FIXPOINT. The proof is somewhat more complex than that of Theorem 1
because the number of registers in a linear program of SRL that represents the
polynomial p of a Diophantine equation depends on the number of unknowns
of p and on its monomial degree (De nition 3, page 3).
Corollary 2. Let p be a polynomial which is an instance of Equ(Z). Let u(p)
and d(p) be respectively the number of unknowns and the monomial degree of p. It
is possible to reduce the problem p = 0 to the xpoint problem of a program P (p)
that belongs to l-SRL( 2u(p)d(p) ).
Proving Theorem 2
We de ne a reduction from Equ(Z) single equation Diophantine problem
over Z to l -FIXPOINT, the xpoint problem on linear SRL.
Like in the proof of Theorem 1 we illustrate how the proof works by means
of an example. The general case will follow intuitively and, in fact, will be sum-
marized by Corollary 2. Once again, let:
p(x, y) = 2x3 y 2 − xy 2 + 2. (5)
be the polynomial already used to illustrate how the proof of Theorem 1 works.
The program P(p) which p(x, y) maps to, is the sequential composition of
the following lines of code:
Program Comment
for x(inc a1 ); for x1 (dec a1 ); a1 ← a1 + x − x1 (a)
for x(inc a2 ); for x2 (dec a2 ); a2 ← a2 + x − x2 (b)
for y(inc b1 ); for y1 (dec b1 ); b1 ← b1 + y − y 1 (c)
for x(for x1 (for x2 (for y(for y1 (inc s; inc s))))); s ← s + 2xx1 x2 yy1 (d)
for x(for y(for y1 (dec s))); s ← s − xyy1 (e)
inc s; inc s s ← s + 2. (f )
The whole sequential composition belongs to l-SRL(9). The registers used
are x, x1 , x2 , a1 , a2 , y , y1 , b1 , and s. By x, x1 , x2 , y, and y1 we denote the initial
values of the homonyms registers. We remark that the code at lines (d) and (e)
linearize in some sense, the code (A) and (B) of the non linear case at page 5.
We now comment on why p(x, y) = 0 has a solution if, and only if, the linear
program P(p) has a xpoint holds, by following our running example.
If p(x, y) = 0 has a solution, then P(p) has a xpoint.
Let us assume that the tuple (x, y) of instances of (x, y) is a solution of p(x, y) = 0.
Execute P(p)(x, x, x, a1 , a2 , y, y, b1 , s), i.e. the program P(p) whose variables x,
x1 , x2 , a1 , a2 , y , y1 , b1 and s assume their initial values x, x, x, a1 , a2 , y, y, b1 ,
and s, respectively, for some arbitrarily xed a1 , a2 , b1 , and s. Then:
P(p)(x, x, x, a1 , a2 , y, y, b1 , s) =
= (x, x, x, a1 + x − x, a2 + x − x, y, y, b1 + y − y, s + 2xxxyy − xyy + 2) (6)
3 2 2
= (x, x, x, a1 , a2 , y, y, b1 , s + 2x y − xy + 2)
= (x, x, x, a1 , a2 , y, y, b1 , s) (7)
where (6) holds because x, x1 , x2 , y and y1 never change while a1 , a2 , b1 and s
get updated in accordance with the behavior of P(p). Instead, (7) is true because
0 = 2x3 y2 − xy2 + 2 by assumption. I.e. the linear program P(p) of SRL has a
xpoint.
If P has a xpoint, then p(x, y) = 0 has a solution.
Let (x, x1 , x2 , a1 , a2 , y, y1 , b1 , s), inputs for the registers (x, x1 , x2 , a1 , a2 , y, y1 , b1 , s),
be a xpoint of P(p). Let P(p)(x, x1 , x2 , a1 , a2 , y, y1 , b1 , s) denote the execution of
P(p) from (x, x1 , x2 , a1 , a2 , y, y1 , b1 , s). By following what happens to the values
of x, x1 , x2 , a1 , a2 , y, y1 , b1 and s from (a) through (f) in the program above, we
obtain:
P(p)(x, x1 , x2 , a1 , a2 , y, y1 , b1 , s) =
(x, x1 , x2 , a1 + x − x1 , a2 + x − x2 , y, y1 , b1 + y − y1 , s + 2xx1 x2 yy1 − xyy1 + 2)
where x, x1 , x2 , y, and y1 remain constant because they only drive iterations.
Being (x, x1 , x2 , a1 , a2 , y, y1 , b1 , s) a xpoint of P(p), we must satisfy the following
series of constraints:
a1 = a1 + x − x1 (8)
a2 = a2 + x − x2 (9)
b1 = b1 + y − y1 (10)
s = s + 2xx1 x2 yy1 − xyy1 + 2. (11)
As the left and right-hand side of (8), (9) and (10) must be equal, forcefully:
x1 = x x2 = x y1 = y.
3 2
Distributing them inside (11) yields the constraint that: s = s + 2x y − xy2 + 2
3 2 2
which we can satisfy only if 0 = 2x y − xy + 2 = p(x, y), i.e. p(x, y) has a
0
solution. Since Equ(Z) is Σ1 -complete [25] l -FIXPOINT is and this concludes the
justi cation of Theorem 2.
4.1 Proving Corollary 2
We want to exploit our running example to estimate a reasonably tight bound
on the amount of registers that P(p) uses, where P(p) is the program de ned
in the above reduction. Looking at P(p) as the sequential composition of (a)
through (f) we can state the following.
P(p) must have one register per every unknown of p(x, y) plus one register
which stores the value of p(x, y). So we have the three registers x, y and s.
For a generic polynomial q , this means that P(q) needs u(q) + 1 registers.
P(p) also uses a pair x1 , x2 of registers. All together, x, x1 and x2 compute x3
for any value x that we assign to the unknown x of the polynomial p. Equiv-
alently, x1 and x2 stand for the linearization of x inside P(p) and they are as
many as the degree d(x) of x minus 1 because x counts for one occurrence of
itself, of course. The meaning of y1 is analogous. Together with y it counts
for the two occurrences of y in P(p) that we use for the unknown y of p
2
to obtain y . For a generic polynomial q , this means that P(q) also needs
hP i
x unknown of q d(x) − 1 registers.
Finally, P(p) also uses a pair of registers a1 , a2 . They are the key ingre-
dient that let the reduction work. Speci cally, every ai assures that the
corresponding xi is in fact a copy of x. The meaning of b1 (there is an
unique bi in our running example) is analogous. It ensures that y1 contains
the same value as y . For a generic polynomial q , this boils down to have as
registers as the number of copies of the unknowns of q . So P(q) needs
hmany
P i
x unknown of q d(x) − 1 further registers.
Summarizing, given an instance q(x1 , . . . , xm ) = 0 of Equ(Z), the linear pro-
gram P(q) of SRL uses as many as u(p) + 1 + 2u(p)(d(p) − 1) registers, which is a
number bounded by u(p) + 1 + 2u(p)(d(p) − 1) = u(p)(2d(p) − 1) + 1 ≤ 2u(p)d(p).
So, P(q) ∈ l-SRL( 2u(p)d(p) ).
Equation Program
u d 16ud
58 4 3 712 ←
38 8 4 864
32 12 6 144
29 16 7 424
28 20 8 960
26 24 9 984
25 28 11 200
24 36 13 824
... ... ...
Fig. 1. The rst two columns are from [12, page 861]. For each row they state that the
Equ(N+ ) sub-problem that asks for the existence of zeros of a Diophantine equations
over N (with coe cients in Z) with no more than u unknowns and monomial degree not
+
exceeding d, is undecidable. The third column expresses that l -FIXPOINT is undecidable
even considering programs with no more than 16ud registers only. Thus, from the data
in [12], the best upper bound on the number of registers su cient for undecidability
is 3 712.
4.2 Strengthening Theorem 2
Theorem 2 can be strengthened like Theorem 1.
Theorem 3. The problem l -FIXPOINT is undecidable and complete in Σ10 for
linear programs in l-SRL( 3712 ).
The proof of Theorem 3 relies on two results of [12]. The rst result presents
an universal system of Diophantine equations which includes the parameters x,
z , u and y and 28 unknowns that take values in N+ [12, Theorem 3]. Fixing
values for x, y, u and z yields a set Sx,y,u,z of Diophantine equations, i.e. an
+
instance of Sys(N ). Then, Sx,y,u,z has a solution if and only if x ∈ Whz,u,yi
(notation of [12]), where Whz,u,yi is a system of equations which we can think of
as much expressive as a universal Turing machine. The system Sx,y,u,z can be
+
transformed into a single Diophantine equation sx,y,u,z over N whose polyno-
mial has monomial degree 4 and 58 unknowns, besides the above x, y, u and z .
+
Therefore, sx,y,u,z belongs to Equ(N ).
The second result we need from [12] is Theorem 4. It lists a sequence of pairs
(u, d) of natural numbers as in Figure 1. The decision problem p = 0 of Equ(N+ )
is undecidable if p belongs to the class of polynomials with no more than u
unknowns and monomial degree not exceeding d. So, Theorem 4 of [12] directly
0
implies that sx,y,u,z is undecidable and Σ1 -complete whenever the u and the d
of the polynomial it involves occur in Figure 1.
Standard techniques [16] imply that we can reduce the instance sx,y,u,z
of Equ(N
+
) to s0x,y,u,z of Equ(Z) so that the polynomial p of s0x,y,u,z has 4 × 58 =
232 unknowns and monomial degree equal to 2 × 4 = 8. Corollary 2 at page 7 ap-
0
plies to sx,y,u,z , so that that the number of registers that the linear program P(p)
0
uses is 2 × 232 × 8 = 3712. Being sx,y,u,z undecidable implies that l -FIXPOINT
is undecidable for P(p) ∈ l-SRL(3712).
5 Final remarks
Among the non trivial total reversible programming languages, SRL is perhaps
the simplest one. In this work we prove that a natural decision problem, namely
does a given SRL program P have a xpoint x?, that is, ∃x : P(x) = x?,
is undecidable. Given the simplicity of the problem and the limitations of the
language SRL, this is a signi cant result because simple decision problems about
very simple programming languages tend to be decidable.
It is interesting to remark that, while the undecidability of the Diophantine
decision and similar problems can be proved by reducing the Turing machine (or
universal register language) halting problem to the existence of a solution of a
polynomial equation (see for instance [29, Section 5.5] and [11]), we proved the
undecidability of the xpoint problem for a very limited total reversible register
language by reducing Equ(Z) to it.
We also established bounds on the number of registers which imply the un-
decidability: 12 registers are enough in the general case and 3 712 in the linear
one.
We think that there are better upper bounds for that number of registers,
perhaps for the general and, almost certainly, for the linear SRL programs. Sev-
eral other open problems are suggested by this research. For instance, given
a positive integer k , are there SRL programs having exactly k xpoints? And
also: is there a reduction Equ(Z) ≤ FIXPOINT such that the number of roots
of the polynomial is equal to the number of xpoints of the corresponding SRL
program?
References
1. Boolos, .G., Burgess, P.J., Jerey, C.R.: Computability and Logic. CUP (2007)
2. Cooper, S.B.: Computability Theory. CRC Press Company (2004)
3. Crolard, T., Lacas, S., Valarcher, P.: On the expressive power of the Loop language.
Nordic Journal of Computing 13(1-2), 4657 (2006)
4. Cutland, N.: Computability: An Introduction to Recursive Function Theory. Cam-
bridge University Press (1980)
5. Davis, M.: Computability and Unsolvability. Dover (1985)
6. Enderton, B.H.: Computability Theory: an Introduction to Recursion Theory. Aca-
demic Press, 1 edn. (2010)
7. Hermes, H.: Enumerability, Decidability, Computability. Springer-Verlag (1969)
8. Ibarra, O.H., Leininger, B.S.: Straight-line programs with one input variable. SIAM
Journal on Computing 11(1), 114 (1982)
9. Ibarra, O.H., Leininger, B.S.: On the simpli cation and equivalence problems for
straight-line programs. J. ACM 30(3), 641656 (1983)
10. Ibarra, O.H., Leininger, B.S.: On the zero-inequivalence problem for loop programs.
J. Comput. Syst. Sci. 26(1), 4764 (1983)
11. Jones, J.P., Matiyasevich, Y.: Register machine proof of the theorem on exponential
diophantine representation of enumerable sets. Journal Symbolic Logic 49, 818829
(1984)
12. Jones, J.P.: Undecidable diophantine equations. Bull. Amer. Math. Soc. (N.S.)
3(2), 859862 (1980)
13. Jones, N.D.: Computability and Complexity: From a Programming Perspective.
Foundations of Computing Series, MIT Press (1997)
14. Kleene, S.C.: Introduction to Metamathematics. North-Holland (1952), reprinted
by Ishi press on 2009
15. Kristiansen, L., Niggl, K.H.: On the computational complexity of imperative pro-
gramming languages. Theoretical Computer Science 318(1-2), 139161 (Jun 2004)
16. Matiyasevich, Y.: Hilbert's Tenth Problem. MIT Press (1993)
17. Matos, A.B.: Analysis of a simple reversible language. Theoretical Computer Sci-
ence 290(3), 20632074 (2003)
18. Meyer, A.R., Ritchie, D.M.: The complexity of loop programs. In: Proceedings of
22nd National Conference of the ACM. pp. 465469. Association for Computing
Machinery (1967)
19. Meyer, A.R., Ritchie, D.M.: Computational complexity and program structure. In:
IBM Research Report RC 1817. IBM (1967)
20. Nathanson, M.B.: Additive Number Theory The Classical Bases. Springer Science
& Business Media (1996)
21. Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information:
10th Anniversary Edition. Cambridge University Press, New York, NY, USA, 10th
edn. (2011)
22. Paolini, L., Piccolo, M., Roversi, L.: A class of recursive permutations which is
primitive recursive complete (2016), Submitted
23. Paolini, L., Piccolo, M., Roversi, L.: A class of reversible primitive recursive func-
tions. Electronic Notes in Theoretical Computer Science 322(18605), 227242
(2016)
24. Perumalla, K.: Introduction to Reversible Computing. CRC Press (2014)
25. Rogers, H.: Theory of Recursive Functions and Eective Computability. MIT Press
Cambridge, MA (1967)
26. Soare, R.I.: Turing Computability: Theory and Applications. Springer (2016), de-
partment of Mathematics, the University of Chicago
27. Sun, Z.W.: Further results on Hilbert's Tenth Problem (2017), https://arxiv.
org/abs/1704.03504, Cornell University Library
28. Tooli, T.: Reversible computing. In: de Bakker, J., van Leeuwen, J. (eds.) Au-
tomata, Languages and Programming. pp. 632644. Springer Berlin Heidelberg,
Berlin, Heidelberg (1980)
29. Yuri, M.: Hilbert's tenth problem: what was done and what is to be done. In:
Denef, J., Lipshitz, L., Pheidas, T., Geel, J.V. (eds.) Hilbert's Tenth Problem:
Relations with Arithmetic and Algebraic Geometry (Contemporary Mathematics,
270). Amer. Math. Soc. (2000)