# 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>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.

• Is $f.x$ your strange way of writing $f(x)$? Hmm, why do you write $(a+c).(d+c)$ then? What do the dots mean? – Andrej Bauer Jan 17 at 13:45
• What was the actual question? Which function are you trying to write in tail-recursive form? – Daniel McLaury Jan 17 at 13:56
• The question was to write $f$ tailrecursively, updated the question accordingly. Also the $.$ is function application, so yes, $f.x=f(x)$ and $\psi .a.b.c.d.n = \psi (a,b,c,d,n)$ – Maarten Jan 17 at 14:07
• For the moment, the specification looks like black magic to me. – Apass.Jack Jan 17 at 14:57
• As pointed out by Leo163, please correct $a*((n+1)^2+h.n)+b*(4*g.n-7*h.n)+c*((n+1)^2+2*n+3+d$ to $a*((n+1)^2-h.n)+b*(4*g.n-7*h.n)+c*((n+1)^2+2*n+3+d)$. Also note the closing parenthesis was missing. – Apass.Jack Jan 17 at 15:40

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$$.