# Show that $f(x) = \lfloor \sqrt{2} \cdot x\rfloor$ is primitive recursive function.

Trying to wrap my head around primitive recursive functions. Especially bounded minimalisation and how to prove something is indeed primitive recursive.

Found the following problem for the subject

Show that $f(x) = \lfloor \sqrt{2} \cdot x\rfloor$ is primitive recursive function.

With some testing I found out that

$f(x) = (\mu z \leq 2x)(2x^{2} <(z+1)^{2})$

should work with any given number. Now I just don't know where to go with this information.

edit.

I just realized that $x \leq z$ always on the above function. So it must be wrong?

edit2.

So I tried to come up with something that would prove $f(x)$ is indeed primitive recursive. Here is my attempt

$f(0) = \lfloor \sqrt{2} \cdot 0 \rfloor = 0$

$f(n+1) = (\mu z \leq 2x)(2x^{2} < (z +1)^{2})$

Now define relation S as follows

$R = \{(z,x,y) \in \mathbb{N}^{3} | (2x^{2} < (z +1)^{2} \}$

Now R is primitive recursive since

$f_{S}(z,x,y) = f_{<} (mult(2,c(2,x)),c(2,succ(z)))$

where $c(a,b) = b^{a}$, $mult(a,b) = a \cdot b$, $succ(a) = a + 1$ and $f_{<}$ is characteristic function of relation $\{ (x,y) | x < y\}$.

Let $h: \mathbb{N}^{2} \rightarrow \mathbb{N}$ be function

$g(y,x) = (\mu z \leq y)((z,x,y) \in R)$

Now $g$ is primitive recursive as it is gained by bounded minimalisation from primitive recursive relation $S$.

Let $h:\mathbb{N}^{2} \rightarrow \mathbb{N}$, $h(y,x) = g(2y,y)$. Now $h$ can be written as follows

$h(y,x) = g(mult(2,y),y)$

so $h$ is primitive recursive.

Now we can write $f(n+1) = h(n,f(n))$ and thus $f$ is primitive recursive.

Is this at all correct?

• Modify your attempted definition of $f(x)$ to start with $(\mu z\leq 2x)$. – Andreas Blass May 12 '18 at 11:54
• Thanks but now I am just back at the original question. Where do I go with this? – E.K. May 12 '18 at 13:26
• Do you want a theoretical proof like this one, or a more pragmatic proof where you write a realistic implementation using only primitive recursive operations? For example, one way to do the latter would be to explicitly calculate the number of bisection operations needed to get $\lfloor l_n x \rfloor = \lfloor u_n x \rfloor$ where $[l_n,u_n]$ are the bisection brackets of $\sqrt{2}$ starting from, say, $[1,2]$. This amounts to asking for an estimate for $\min \{ |k/\sqrt{2}-n| : k \in \mathbb{N},n \in \{ 1,\dots,x \} \}$". – Ian May 12 '18 at 15:49
• Once you know that this number is say $\epsilon$ then $\sqrt{2} x$ is guaranteed to be at least $\epsilon$ away from an integer, and so it suffices to run bisection until the length of your bracket is less than $\epsilon/x$. – Ian May 12 '18 at 15:56
• Theoretical proof if at all possible. – E.K. May 12 '18 at 15:56