[Math] Prove that [x/y] is a primitive recursive function

computabilityfunctions

Prove that [x/y] is a primitive recursive function using this theorem:
If $g(x_1,…,x_n)$ is primitive recursive, then $f(x_1,…,x_n)=\sum^{x_n}_{i=0}g(x_1,…,x_{n-1},i)$ is also a primitive recursive function.
I've tried, but I couldn't come up with an idea.

Best Answer

Assuming $\left[ \frac{x}{y} \right]$ is the integer part of the division of $x$ and $y$, and that $x, y \in \mathbb{N} \cup\{0\}$ then let us define $\left[ \frac{x}{0} \right] = x$.

Remark: In discrete math and computer science, it seems quite usual to include $0$ in the natural numbers. Also, note that this function is similar to the floor function.

To prove the assertion that $\left[ \frac{x}{y} \right]$ is primitive recursive, consider the following equivalences:

$$ \left[ \frac{x}{y} \right]=z \iff \left(y=0 \land x=z \right) \lor \left( y \neq 0 \land z \leq \frac{x}{y} \lt z+1 \right)$$

$$\iff \left(y=0 \land x=z \right) \lor \left( y \neq 0 \land zy \leq {x} \lt (z+1)y \space \right) $$ $$\iff \left(y=0 \land x=z \right) \lor \left( y \neq 0 \land z \space\text{is the smallest natural number such that} \space {x} \lt (z+1)y \space \right) $$

Additionally, note that $\left[ \frac{x}{y} \right] \leq x$.Thus, we can define the function using the bounded minimisation operator :

$$\left[ \frac{x}{y} \right] = \mu z \leq x\left[ (y=0 \land x=z) \lor (y \neq 0 \land x<(z+1)y) \space \right]$$

Therefore the function $\left[ \frac{x}{y} \right]$ has been constructed by the bounded minimisation operator of primitive recursive functions and relations. It follows from the definition of a primitive recursive function that $\left[ \frac{x}{y} \right]$ is primitive recursive.

Related Question