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?