Given some recursive function, can we effectively associate it a polynomial as in the DPRM theorem?

Question

I'm interested in the following assertion about the Davis-Putnam-Robinson-Matijasevich theorem

Given a recursive function $f:\mathbb{N}\rightarrow\mathbb{N}$, i.e. its index, we can effectively get a polynomial $p\in\mathbb{Z}[x,y,z_1,\dots,z_n]$ that satisfies $$f(x)=y\iff\exists z_1\dots z_n \in \mathbb{N} \\ p(x,y,z_1\dots z_n )=0.$$

In other words

After indexing recursive functions and integer polynomials, there is a recursive function whose input is the index of a recursive function $f:\mathbb{N}\rightarrow\mathbb{N}$ and whose output is the index of a polynomial $p\in\mathbb{Z}[x,y,z_1,\dots,z_n]$ that satisfies

$$f(x)=y\iff\exists z_1\dots z_n \in \mathbb{N} \\ p(x,y,z_1\dots z_n )=0.$$

I believe it's true, and that it's implicit in the proof of the DPRM theorem (both in Matijasevic proof and Martin Davis proof). If this is stated somewhere and you know it, please let me know :). On the other hand, it may be too obvious that this is implicit in the proofs, but in that case I would like to hear that from someone else.

Why I believe this is true: both proofs are constructive, i.e., they indicate how to get the desired polynomial from an arbitrary recursive functions. I develop a bit more:

• Matijasevic proof

As I understand the proof, given a register machine, i.e. its instructions, it specifies how to coded each possible instruction as a polynomial. If we index each possible register machine by its instructions, the polynomial is effectively obtained from the index of the function, and we could put this procedure in a recursive function.

• Martin Davis proof

As I understand the proof (theorem 6.1), it proves that diophantine functions are closed under composition, primitive recursion, and minimalization (i.e. the $\mu$ operator). In each case, it gives an explicit and concrete diophantine formula (well, formulas with abbreviations, but all of those can be expanded). This proves that recursively enumerable functions are diophantine. Now, if we index each possible recursively enumerable function by its "factorization" using composition, primitive recursion, and minimalization (this is possible and effective), then the polynomial we get is effectively obtained from the index of the function.

Thanks for reading :)

Answer 1

Davis (also available on the MAA site) begins section 7 by saying "an explicit enumeration of all the Diophantine sets of positive integers will now be described".

He then gives theorem 7.1, from which one can get a polynomial form for a universal Diophantine set.

In the proof of theorem 7.3, he says "write $$x\in D_n \iff (\exists z_1,\cdots, z_n) [P(n,x,z_1,\cdots, z_n)=0]$$ where P is some definite (though complicated) polynomial."

I find all that plenty explicit about the explicitness.