\def\code#1{\mathtt{#1}} \def\closure#1{\mathcal C_{#1}} \def\par#1{\left( {#1} \right)} \def\set#1{\left\{ {#1} \right\}} \def\union{\cup}

Closure analysis

fact n return: isZero n base recurse
    base: return 1
    recurse: sub n 1 step1
        step1 m: fact m step2
        step2 f: mul n f return

main return1: fact 5 m0
    m0 f: print f m1
    m1: return1

Take the exemplar line

\code{step1}\ \code{m}\ \code{return}\ \code{:}\ \code{isZero}\ \code{n}\ \code{base}\ \code{recurse}

Turn this into a equation where we take all indentifiers in the call. For each identifier that is a name, we add a the closure. For each identifier that is a parameter, we just add it plain. Then subtract the parameters of the declaration itself.

This creates a set of equations:

\begin{align} \closure{\code{fact}} &= \set{\code{n}} \union \closure{\code{base}} \union \closure{\code{recurse}} \setminus \set{\code{n}, \code{return}} \\ \closure{\code{base}} &= \set{\code{return}} \\ \closure{\code{recurse}} &= \set{\code{n}} \union \closure{\code{step1}} \\ \closure{\code{step1}} &= \set{\code{m}} \union \closure{\code{fact}} \union \closure{\code{step2}} \setminus \set{\code{m}} \\ \closure{\code{step2}} &= \set{\code{n}, \code{f}, \code{return}} \setminus \set{\code{f}} \\ \closure{\code{main}} &= \closure{\code{fact}} \union \closure{\code{m0}} \setminus \set{\code{return1}} \\ \closure{\code{m0}} &= \set{\code{f}} \union \closure{\code{m1}} \setminus \set{\code{f}} \\ \closure{\code{m1}} &= \set{\code{return1}} \end{align}

Let's try to solve these equations:

\begin{align} \closure{\code{fact}} &= \closure{\code{recurse}} \setminus \set{\code{n}, \code{return}} \\ \closure{\code{base}} &= \set{\code{return}} \\ \closure{\code{recurse}} &= \set{\code{n}} \union \closure{\code{step1}} \\ \closure{\code{step1}} &= \set{\code{n}, \code{return}} \union \closure{\code{fact}} \setminus \set{\code{m}} \\ \closure{\code{step2}} &= \set{\code{n}, \code{return}} \\ \closure{\code{main}} &= \closure{\code{fact}} \setminus \set{\code{return1}} \\ \closure{\code{m0}} &= \set{\code{return1}} \\ \closure{\code{m1}} &= \set{\code{return1}} \end{align}

The problem now is that we have a cycle around \closure{\code{fact}}.

\begin{align} \closure{\code{fact}} &= \closure{\code{recurse}} \setminus \set{\code{n}, \code{return}} \\ \closure{\code{recurse}} &= \set{\code{n}} \union \closure{\code{step1}} \\ \closure{\code{step1}} &= \set{\code{n}, \code{return}} \union \closure{\code{fact}} \setminus \set{\code{m}} \end{align}

Let's inline all expressions until we recurse:

\begin{align} \closure{\code{fact}} &= \set{\code{n}} \union \par{ \set{\code{n}, \code{return}} \union \closure{\code{fact}} \setminus \set{\code{m}} } \setminus \set{\code{n}, \code{return}} \end{align}

Alternatively, we could pick any of the others to inline. The results should be the same:

\begin{align} \closure{\code{recurse}} &= \set{\code{n}} \union \par{ \set{\code{n}, \code{return}} \union \par{ \closure{\code{recurse}} \setminus \set{\code{n}, \code{return}} } \setminus \set{\code{m}} } \end{align}

Solving for fact

\begin{align} \closure{\code{fact}} &= \set{\code{n}} \union \par{ \set{\code{n}, \code{return}} \union \closure{\code{fact}} \setminus \set{\code{m}} } \setminus \set{\code{n}, \code{return}} \\ \closure{\code{fact}} &= \par{ \set{\code{n}} \setminus \set{\code{n}, \code{return}} } \union \par{ \par{ \set{\code{n}, \code{return}} \union \closure{\code{fact}} \setminus \set{\code{m}} } \setminus \set{\code{n}, \code{return}} } \\ \closure{\code{fact}} &= \par{ \set{\code{n}} \setminus \set{\code{n}, \code{return}} } \union \par{ \par{ \set{\code{n}, \code{return}} \union \closure{\code{fact}} } \setminus \set{\code{m}, \code{n}, \code{return}} } \\ \closure{\code{fact}} &= \par{ \set{\code{n}, \code{return}} \setminus \set{\code{m}, \code{n}, \code{return}} } \union \par{ \closure{\code{fact}} \setminus \set{\code{m}, \code{n}, \code{return}} } \\ \closure{\code{fact}} &= \closure{\code{fact}} \setminus \set{\code{m}, \code{n}, \code{return}} \\ \closure{\code{fact}} &\in \mathcal{P} \par{ \set{\code{m}, \code{n}, \code{return}} ^\mathrm{C} } \end{align}

The smallest solution is \closure{\code{fact}} = \emptyset.

We can substitute this back to solve all equations. But let's instead look at a different recursive equation and see if we can solve it too:

Solving for recurse

\begin{align} \closure{\code{recurse}} &= \set{\code{n}} \union \par{ \set{\code{n}, \code{return}} \union \par{ \closure{\code{recurse}} \setminus \set{\code{n}, \code{return}} } \setminus \set{\code{m}} } \\ \closure{\code{recurse}} &= \set{\code{n}} \union \par{ \set{\code{n}, \code{return}} \setminus \set{\code{m}} } \union \par{ \closure{\code{recurse}} \setminus \set{\code{m}, \code{n}, \code{return}} } \\ \closure{\code{recurse}} &= \set{\code{n}, \code{return}} \union \par{ \closure{\code{recurse}} \setminus \set{\code{m}, \code{n}, \code{return}} } \end{align}

The smallest solution is \closure{\code{recurse}} = \set{\code{n}, \code{return}}.