Question

As this thread title gives away I need to prove $x^y$ to be a primitive recursive function.

So mathematically speaking, I think the following are the recursion equations, well aware that I am assigning to $0^0$ the value $1$, which shouldn't be, since it is an "indeterminate" form.

\begin{cases} x^0=1 \\ x^{n+1} = x^n\cdot x \end{cases}

More formally I would write: \begin{cases} h(0) = 1 \\ h(x,y+1) = g(y,h(x,x),x) \end{cases}

as $g(x_1, x_2, x_3) = h\left(u^3_2(x_1, x_2, x_3),u^3_3(x_1, x_2, x_3)\right)$ and provided $h(x,y) = x \cdot y$ is primitive recursive.

Is my proof acceptable? Am I correct, am I missing something or am I doing anything wrong?

Was it helpful?

Solution

Supposing that $\times~(mult)$ is primitive recursive function. Then you could write:

$exp(x,y)={ x }^{ y }$

1) $exp(x,0)=x^0=1$

2) $exp(x,y+1)=x^{y+1}=(x^y)\times x=mult(exp(x,y),x)$

for $mult$ you could show that:

$mult(x,y)=x\times y$

1)$mult(x,0)=x \times 0=0$

2)$\operatorname{mult} \left({x, y + 1}\right) = x \times \left({y + 1}\right) = \left({x \times y}\right) + x = \operatorname{add} \left({\operatorname{mult} \left({x, y}\right), x}\right)$

and for addition $add$ the proof is straightforward.

Hope these are useful!

OTHER TIPS

As I wrote in the comments, you haven't actually proved anything. If you want to prove that $x^y$ is p.r., you need to write it in the scheme form, and then you need to prove that indeed $x^y = f(y,x)$ for your defined $f$ for all $x$ and $y$ (by double induction).

Consider the following definition of $f(y,x) = x^y$:

$f(0,x) = s(z(x))$ (i.e., the successor of the constant zero function).

$f(y+1, x) = u^3_1(u^3_1(x^y, x, y) \cdot x, x, y)$.

I assume now that multiplication, $x \cdot y$ and wrote it infix, and obviously $x^y = f(y,x)$. The function $u^a_b$ is the $a$-ary projection of $b$.

(Ps. if this doesn't work for you, please post your scheme you want to use, otherwise we cannot do else then guess.)

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top