SRL is a total programming language for reversible computing. In SRL, every program that mentions n registers denes a bijection Zn ! Zn. Since SRL contains only a very essential set of commands it is 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 program P that remains unaltered after the execution of P. First, we show that the existence of xed points in SRL is undecidable and complete in 10. 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.
Loop languages are an important sub-class of while programming languages (see
for instance [
Each register contains a value in Z; each program mentioning n registers denes a bijection Zn ! Zn. Consider the following SRL programs: P0 : for x(inc r) P1 : for x(dec r)
P2 : for y(for x(inc 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 modication 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 plus the square x2. 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
negative, 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 [
Among the languages whose programs represent exactly reversible functions,
SRL and ESRL [
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 modied by the execution of P?. We prove that the xpoint problem is undecidable and complete in 10. 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 [
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 [
The sets of positive integers, non-negative integers, integers, and rational numbers 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 program P of SRL denes a bijection Zn ! Zn, where n 2 N+ is the number of registers that occur in the denition of P. Such n registers are said to be mentioned or used in P. The program P 1 is the inverse of P and computes the inverse bijection (below we explain how to generate P 1 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 on P 1. 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, nor dec r, nor for r(P0) 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 [
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 dened for every k 2 Z. (the extension of the denition 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)).
Denition 1 (Fixpoint of a program). Let P be a SRL program that mentions n registers x = hx1; : : : ; xni. 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 [
Denition 2 ( FIXPOINT-decision problem). Let P be a SRL-program then the FIXPOINT-decision problem is
FIXPOINT(P)
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
[
Polynomials Let p(x1; : : : ; xn) be an integer polynomial, i.e. a polynomial with integer coecients and unknowns x1; : : : ; xn. A polynomial is in normal form if: (i) it is a sum of monomials; (ii) each monomial has form cxe11 xe22 : : : xek where c 6= 0 k 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.
For instance, 3x2y+y2 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 example, the normal form of 3xy(z + y2) + 2z 3y3x is 3xyz + 2z. We shall often omit exponents equal to 1 as well as monomial coecients c equal to 1. The null polynomial is denoted by 0.
Denition 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) = xy3z + 2xyz3 z4. 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 the exponents of 2xyz3. 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:
such that p(x1; : : : ; xn) = 0? HTP(D) can be straightforwardly generalized to questions on a set of integer polynomials fp1(x1; : : : ; xn); : : : ; pm(x1; : : : ; xn)g as follows:
HTP(D)(p1; : : : ; pm)
such that pi(x1; : : : ; xn) = 0; for every 1 i m ?
The diculty of solving HTP(D) depends on D [16, (1.3.1)],[
Denition 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
The rst part of this section focuses on proving the next theorem. Theorem 1. The problem FIXPOINT as in Denition 2 (page 3), is undecidable and complete in 10.
The strategy is to reduce Equ(Z), i.e. HTP(Z) that deals with a single Diophantine equation, to FIXPOINT. We show how by means of a signicant 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:
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))))); for x(for y(for y(dec s))); inc s; inc s. (1) (A) (B) (C) (2) (3) (4) Line (A) updates the content of s in accordance with the assignment: The factor x3 follows from the three nested iterations driven by x. Analogously, the two nested iterations driven by y yield the factor y2. Factor 2 comes from inc s; inc s. Under the same idea, lines (B) and (C) produce: s
s + 2x3y2. s s s s + 2, xy2 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 + 2x3y2 xy2 + 2 for s. We can formalize the overall eect as follows:
P(p)(x; y; s) = (x; y; s + 2x3y2 xy2 + 2).
Being (x; y; s) a xpoint of P(p), we must have s = s + 2x3y2 xy2 + 2 which is possible only if 2x3y2 xy2 +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 + 2x3y2
xy2 + 2) = (x; y; s + p(x; y))
= (x; y; s + 0) = (x; y; s),
which means that (x; y; s) is a xpoint of P(p). Since Equ(Z) is 10-complete [
We now proceed to the strengthening of Theorem 1. In [27, Part 1: Corollary 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 POINT contain programs that mention 12 registers. 10 already when FIX4
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.
Denition 5 (Linear SRL programs). Let n 2 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 (Denition 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) ).
We dene 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 summarized by Corollary 2. Once again, let: 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 for x(inc a1); for x1(dec a1); for x(inc a2); for x2(dec a2); for y(inc b1); for y1(dec b1); for x(for y(for y1(dec s))); inc s; inc s for x(for x1(for x2(for y(for y1(inc s; inc s))))); Comment a1 a2 b1 s s s a1 + x a2 + x b1 + y x1 x2 y1 s + 2xx1x2yy1 s s + 2: xyy1
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) = (x; x; x; a1; a2; y; y; b1; s + 2x3y2
xy2 + 2) = (x; x; x; a1; a2; y; y; b1; s) 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 = 2x3y2 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
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:
Distributing them inside (11) yields the constraint that: s = s + 2x3y2 xy2 + 2
which we can satisfy only if 0 = 2x3y2 xy2 + 2 = p(x; y), i.e. p(x; y) has a
solution. Since Equ(Z) is 10-complete [
x unknown of q d(x) 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. Equivalently, 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 to obtain y2. 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 ingredient that let the reduction work. Specically, 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 many registers as the number of copies of the unknowns of q. So P(q) needs hP i 1 further registers.
Summarizing, given an instance q(x1; : : : ; xm) = 0 of Equ(Z), the linear program 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) 2 l-SRL( 2u(p)d(p) ).
Equation u
d
Theorem 3. The problem l -FIXPOINT is undecidable and complete in
linear programs in l-SRL( 3712 ).
The proof of Theorem 3 relies on two results of [
The second result we need from [
Standard techniques [
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, 9x : P(x) = x?, is undecidable. Given the simplicity of the problem and the limitations of the language SRL, this is a signicant 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 [
We also established bounds on the number of registers which imply the undecidability: 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. Several 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?