5
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ Modify your attempted definition of $f(x)$ to start with $(\mu z\leq 2x)$. $\endgroup$ – Andreas Blass May 12 '18 at 11:54
  • $\begingroup$ Thanks but now I am just back at the original question. Where do I go with this? $\endgroup$ – E.K. May 12 '18 at 13:26
  • $\begingroup$ 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 \} \}$". $\endgroup$ – Ian May 12 '18 at 15:49
  • $\begingroup$ 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$. $\endgroup$ – Ian May 12 '18 at 15:56
  • $\begingroup$ Theoretical proof if at all possible. $\endgroup$ – E.K. May 12 '18 at 15:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.