Recursion as an Effect
Published:
In one of my previous post I showed that any theory featuring general recursion is inconsistent when viewed as a logical system which inevitably leads to the idea that all definable functions in such a theory should be total (or productive). However, losing Turing-completeness could be somewhat problematic for some, but it can be addressed in several ways. One of these, an possibly the most popular, is to isolate recursion into a monad, effectively regarding recursion as an effect. We discuss several lifting monads which are fit for purpose.
A Naive Solution
In domain theory non-termination is modelled as an operation \(A \mapsto A_\bot\) which takes a CPO and endows it with a bottom element, which is called the lifting of a CPO.
Thus one could naively think that it is fine to just model non-termination by defining the set
\[M A = A + 1\]which is the set of computations that either return an element of type \(A\) or do not terminate.
Unfortunately, without proper restrictions on the functions that we can apply to it, this monad allows one to “decide non-termination”: one can write a function \(f : M A \to \{\textbf{True}, \textbf{False}\}\) which returns \(\textbf{True}\) if the program does not terminate and \(\textbf{False}\) otherwise. This clearly is not what we are trying to model. In domain theory this is not a problem, because \(\bot \sqsubseteq a\) for all \(a \in A\) and in the set \(\bot \sqsubseteq \textbf{True}, \bot \sqsubseteq \textbf{False}\}\) the elements \(\textbf{True}\) and \(\textbf{False}\) are not related, thus we cannot give a continuous mapping \(a \mapsto \textbf{False}\) and \(\bot \mapsto \textbf{True}\).
The Coinductive Lifting (Capretta)
One solution proposed by Capretta is to take the coinductive solution to the following domain equation
\[D A \cong A + D A\]In other words, \(DA\) is the set coinductively generated by the constructors \(\text{now} : A \to D A\) and \(\text{delay} : DA \to DA\). Intuitively, \(\text{now}(x)\) is a terminating computation which returns an element \(x \in A\) in \(0\) steps, while \(\text{delay}(c)\) takes a computation \(c \in DA\) and delays it by adding one computational step to it. For example, \(\text{delay}(\text{delay}(\text{delay}(10)))\) is a computation which returns the number \(10\) in three steps.
Remark. \(D\) can be given the structure of an \(\omega\)-CPO with \(\bot\).
First, the non-terminating computation \(\bot\) can be defined coinductively as
\[\bot = \text{delay}(\bot)\]which is clearly a productive definition. Intuitively, \(\bot\) corresponds to the never-ending stream of delays:
\[\bot = \text{delay}(\text{delay}(\text{delay}\dots))\]so clearly, we cannot produce a function which discriminate between a terminating computation and non-terminating one. Capretta proves that \(D\) is a domain (up-to bisimilarity), that is, he defines a partial order \(\sqsubseteq_D\) on \(D\) which leads to a notion of least upper bounds for \(\omega\)-chains, written \(\bigsqcup_{n\in \omega} d_n\) for
\[d_0 \sqsubseteq_D d_0 \sqsubseteq_D d_1 \dots \sqsubseteq_D d_n \dots\]then it can be proven that every continuous function on \(D\) has a fixed-point.
However, the constructive delay monad doesn’t seem to have a nice presentation as a theory. This means that contrarily to \(M\) it is not entirely clear how to give an algebraic presentation.
Metric Lifting Monad (Martin Escardó)
Escardó’s metric lifting models partiality using metric spaces rather than coinduction. The metric lifting of a set \(A\), written \(LA\), is defined as
\[LA = (A \times \mathbb{N}) \cup \{\infty\}\]together with a distance function \(d : LA \times LA \to [0, \infty]\) where equal computations have distance \(0\), terminating computations \((a,k)\) and non-terminating ones have distance \((1/2)^k\), and terminating computations \((a,k)\) and \((b,l)\) have distance \(1/2^{\text{min}(k,l)}\). Intuitively, \((a,k)\) is a computation which returns \(a\) in \(k\) steps and \(\infty\) is the divergent computation.
Remark. \(LA\) is a complete bounded metric ultrametric space.
The unit of the monad \(LA\) is defined by \(\eta_A(a) = (a,0)\) and the delay operation is defined by
\[\delta_A(a,n) = (a, n + 1) \qquad \delta_A(\infty) = \infty\]In metric spaces terminology, a function is non-expansive if it does not expand the space relative to a distance function \(d\), but possibly contracts it:
\[d(f(x), f(y)) \le d(x,y)\]On the other hand, a contractive map is a map which contracts the space:
\[d(f(x), f(y)) \le c \dot (d(x,y))\]for a certain \(c < 1\). At this point it is possible to define a fixed-point operator for all contractive maps
\[\text{fix} : (LA \to LA) \to LA\]which sends every non-expansive map \(f\) to the fixed-point of \(\delta_A \circ f\), which is contractive because \(\delta_A\) is contractive. At this point the non-divergent computation is now defined as
\[\bot_A = \text{fix}(id_{LA})\]Guarded Lifting (Atkey & McBride)
The coinductive lifting monad suffers from productivity and equality issues, while both the coinductive and metric liftings need additional structure on the maps defined on them to work properly with fixed-points.
In guarded type theory however, maps are always non-expansive and contractiveness is enforced at the type level. In particular, a contractive map is a function of type \(\triangleright X \to X\) for which there is always a fixed-point at all types \(X\):
\[\text{fix}_g : (\triangleright X \to X) \to X\]sending a map \(f : (\triangleright X \to X)\) to the unique fixed-point of \(f \circ \text{next}\). The guarded lifting is defined as the unique solution to the domain equation
\[L_g A = A + \triangleright L_g A\]There is an obvious unit of the monad \(\eta_A : A \to L_g A\) and delay map which has type
\[\delta_A : \triangleright L_g A \to L_g A\]Conceptually, this monad can be seen as Capretta’s lifting monad with an explicit notion of time or delay built into the type theory. At this point the divergent computation \(\bot_A : L_{g} A\) is defined as the guarded fixed-point of \(\delta\):
\[\bot_A = \text{fix}_g (\delta_A)\]Now we can check from the fixed-point property that \(\bot = \delta_A (\text{next}(\bot_A))\). Here, the term \(\delta_A \circ \text{next}\) corresponds to the delay operation which adds one step to the computation.
Conclusion
The three monads presented here have many similarities, perhaps too many for it not to have a proper reconciliating story, but perhaps there is.