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$


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


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

  • $\begingroup$ 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? $\endgroup$ Jan 17, 2019 at 13:45
  • $\begingroup$ What was the actual question? Which function are you trying to write in tail-recursive form? $\endgroup$ Jan 17, 2019 at 13:56
  • $\begingroup$ 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)$ $\endgroup$
    – Maarten
    Jan 17, 2019 at 14:07
  • $\begingroup$ For the moment, the specification looks like black magic to me. $\endgroup$
    – John L.
    Jan 17, 2019 at 14:57
  • $\begingroup$ 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. $\endgroup$
    – John L.
    Jan 17, 2019 at 15:40

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.