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.
-
How did you define primitive recursive functions? – Asaf Karagila Dec 09 '13 at 22:57
-
$f(x_1,...,x_n)$ is a primitive recursive function if $f(x_1,...,x_{n-1},0)=g(x_1,...,x_{n-1})$ and $f(x_1,...,x_{n-1},y+1)=h(x_1,...,y,f(x_1,...,x_{n-1},y))$. g and h are primitive recursive functions – user1242967 Dec 09 '13 at 23:04
-
Yeah, sorry about that. I thought that you had an issue with proving the theorem, not that $[x/y]$ is primitive recursive. – Asaf Karagila Dec 09 '13 at 23:32
-
Do you use [x/y] to denote substitution or is it some other concept? – Trismegistos Dec 10 '13 at 09:37
2 Answers
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.
- 936
I am assuming that you are referring to integer division.
You can define $\lceil x/y \rceil$ by primitive recursion, like this:
$h(x,y,0) = 0$ , $h(x,y,t+1) = \begin{cases} h(x,y,t) + 1 & \mbox{$x - t\cdot y \geq 0$}\\ h(x,y,t)& \mbox{ow.} \end{cases} $
And so, $\lceil x/y \rceil = h(x,y,x)$
I used that $+,\cdot,-,\geq$ are all primitive recursive (with $-$ restricted to natural numbers in the canonical way) and that $\lceil x/0 \rceil = 0$.