Tailrecursive definition for a function 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&gt;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.
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$.