Tailrecursive definition for a function

Question

In an exam I took we were asked to provide a tailrecursive definition of a recursive function. I failed miserably and the provided solution makes absolutely no sense to me. If anyone could explain that would be very helpful for my resit. The provided solution is the following:

---

Given are the functions $f, g, h \in \mathbb{N} \rightarrow \mathbb{Z}$ with $f.0 = 20, g.0 = 37, h.0 = 13$ and for $n>0$:

$$ f.n = 3*g.n-7*h.n \\ g.n = n^2-h.(n-1) \\ h.n = f.(n-1)+g.(n-1) $$

---

For the tailrecursive version of $f$ specify

$$ \psi \in \mathbb{Z} \rightarrow \mathbb{Z} \rightarrow \mathbb{Z} \rightarrow \mathbb{Z} \rightarrow \mathbb{N} \rightarrow \mathbb{Z} \\ \psi .a.b.c.d.n = a * g.n + b * h.n + c * (n + 1)^2 + d $$

Such that $f.n = \psi .3.(-7).0.0.n$

Then

$$ \psi .a.b.c.d.0 = 37 * a + 13*b+c+d $$

and

$$ \psi .a.b.c.d.(n+1)\\ = \text{\{ spec \}}\\ a*((n+1)^2+h.n)+b*(4*g.n-7*h.n)+c*((n+1)^2+2*n+3+d)\\ = \text{\{ arithmetic \}}\\ 4*b*g.n+(a-7*b)*h.n+(a+c)*(n+1)^2+d+c*(2*n+3)\\ = \text{\{ Construction Hypothesis \}}\\ \psi .(4*b).(a-7*b).(a+c).(d+c*(2*n+3)).n $$

---

The main problem I am having is how they arrived at the specification, since the actual calculation I can follow. If anyone has any insights as to how the specification was obtained I think I would be able to grasp the answer better.

Thank you in advance.

Answer 1

I cannot find a way to make the specification coincide with what your solutions say, but I can get very close to that (personally, I think that your solutions contain a small mistake).

The first part should be $a*((n+1)^2-h.n)$ (and not $a*((n+1)^2+h.n)$), as per the definition of $g$ in terms of $h$.

The second part, $b*(4*g.n-7*h.n)$, comes from the definitions of $h$ and $f$: $b*h.(n+1)=b*(f.n+g.n)=b*((3*g.n-7*h.n)+g.n)=b*(4*g.n-7*h.n)$.

Finally, $c*((n+1)^2+2*n+3$ is just a (uselessly convoluted) way of writing $c*(n+2)^2$.