summaryrefslogtreecommitdiffstats
path: root/content/zettel/1b2.md
blob: c0b9e0723e7b3769b3a91d9e356be638f621aa1a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
+++
title = "Tail calls"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["1d1", "1b1"]
forwardlinks = ["3a", "1b3"]
zettelid = "1b2"
+++

Tail calls are an optimisation that can be applied in software, which
detects that a recursive call only happens at the tail of the function.
If that is the case, then the recursive call can happen without having
to preserve the stack at every call, as it can effectively be translated
to an equivalent version that only uses loops. This optimisation is
important to improve the efficiency of recursive functions if the stack
is not needed, and is especially important in functional languages where
recursion might be more widely used.

As tail calls can be efficiently translated to loops, this also means
that they can be efficiently encoded in hardware when the code is passed
through high-level synthesis. This is straightforward if the tail calls
are detected and automatically translated to loops, however, what
happens if that is not the case and we only have a tail call construct
in the intermediate language.

The CompCert ([\#3a]) \[1\] register transfer language (RTL)
intermediate language, for example, has an explicit tail call construct
(`Itailcall`), which is used if it can detect that a function contains a
tail call. Apart from that, it only has a jump command, which can be
used for loops. Therefore, supporting the tail call construct allows us
to support a subset of possible recursive functions. Even though these
are as powerful as loops, it may be more natural to write their
definitions as a recursive function instead of a loop.

<div id="refs" class="references csl-bib-body" markdown="1">

<div id="ref-leroy06_formal_certif_compil_back_end" class="csl-entry"
markdown="1">

<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">X. Leroy, “Formal certification of
a compiler back-end or: Programming a compiler with a proof assistant,”
in *Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on
principles of programming languages*, in POPL ’06. Charleston, South
Carolina, USA: Association for Computing Machinery, 2006, pp. 4254.
doi: [10.1145/1111037.1111042].</span>

</div>

</div>

  [\#3a]: /zettel/3a
  [10.1145/1111037.1111042]: https://doi.org/10.1145/1111037.1111042