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](https://www.jstor.org/stable/2324421) and Martin Davis [proof](http://www.jstor.org/stable/2318447?origin=JSTOR-pdf)). 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](https://www.jstor.org/stable/2324421)


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](http://www.jstor.org/stable/2318447?origin=JSTOR-pdf)


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 :)



Given some recursive function, can we effectively associate it a polynomial as in the DPRM theorem?
Davis (also available on the MAA [site](https://www.maa.org/sites/default/files/pdf/upload_library/22/Ford/MartinDavis.pdf)) 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.


