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.
Domain-Theoretic Liftings
The domain-theoretic approach to non-termination is to model computations as maps between sets with an additional element. Thus we define a lifting operation which takes a set and adds an element to it
\[M A = A + 1\]which is the set of computations that either return an element of type \(A\) or do not terminate.
Of course, 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.
To avoid this problem, in domain theory, a set \(A\) are endowed with a complete partial order (\(\sqsubseteq\)) where non-termination is modelled as the least element (\(\bot\)). The operation \(A \mapsto A_\bot\) which adds a least element to a CPO is called the lifting of a CPO.
Moreover, functions have to respect a continuity condition, that is the function must preserve least upper bounds of arbitrary \(\omega\)-chains:
Essentially what this means is that the function \(f\) when applied to the best approximation of a subset, can be computed locally for each element of this subset. One consequence of this fact is that \(f\) is monotonic: it preserves the order of the CPO. One feature of this category is that every continuous map \(A_\bot \xrightarrow{\text{cont}} A_\bot\) has a fixed-point operator via the Fixed-Point Theorem:
\[\text{fix}(f) = \bigsqcup_{i \in \omega} f^n(\bot)\]which is given by the least upper bound of an \(\omega\)-chain
\[\bot \sqsubseteq f(\bot) \sqsubseteq f^2(\bot) \sqsubseteq \dots \sqsubseteq f^n(\bot) \sqsubseteq \dots\]To go back to our original problem. Since \(\bot \sqsubseteq a\) for all \(a \in A\), we cannot define a continuous map \(A_\bot \to 2_\bot\) such the one above because in the codomain of this function the elements \(\textbf{True}\) and \(\textbf{False}\) are not related.
Remark. When doing mathematics into a proof assistant the expert distinguishes two ways:
- implementing all the theory inside the prover’s logic, or
- creating a new synthetic language whose structure is interpreted inside the mathematical theory we want to work with
The second approach is the one, for example, used in HoTT, where types are certain topological spaces and functions are continuous.
The problem of formalising domain theory is that it becomes more complicated when the proof assistant is based on type theory. In particular, the problem is that a type is not really a set.
On the other hand, doing things synthetically would mean that recursion is somewhat spread across the whole language. What I mean by this is that since every continuous function has a fixed-point then non-termination can happen at every type making the internal language of this category effectively an inconsistent language when viewed as a logic. Hence the need for treating recursion as an effect.
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))\]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 similarly to the construction in domain theory.
Considerations. Now that recursion is being isolated into an effect we have solved one problem. However, programming in practice with this monad is far from being easy as one has to
- prove that each program on \(DA\) they define is a continuous function
- working with a coinductive bisimilarity relation rather than equality
- ensure productivity of definitions
Metric Lifting Monad (Martin Escardó)
Escardó’s metric lifting models partiality using metric spaces rather than coinduction, but the idea is not that different from Capretta’s. 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})\]Considerations. This approach does not seem to suffer from the use of coinduction, but it still needs the programmer to prove functions are non-expansiveness.
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 Synthetic Approach. What I personally found truly amazing about the guarded lifting is that this monad is truly synthetic. There is no need for additional structure as in Capretta’s lifting, no need for checking continuity or non-expansiveness of maps. Furthermore, using the model of guarded type theory one can show that (in a certain sense) it corresponds to Martin’s metric lifting on one side and to Capretta’s monad on the other. I will probably need another post to explain this point.
Intensionality. To be honest, the only problem arising from the use of guarded recursion unfortunately is the fact that computations are modelled intensionally, that is two computations that return the same output given the same input are not necessarily equal if they take a different amount of steps to terminate. This is an issue that has to be solved once again by quotienting the monad which is another problem entirely.
Nevertheless, these problems also arise in coinductive and metric approaches. At present, the only extensional model of general recursion I am aware of is based on domain theory.
Consistency. Naturally, one might wonder why do we need guarded recursion, if domain theory already lets us model all of this extensionally? The answer to that is that, while domain theory is extremely powerful for modelling recursion extensionally, it does not yield a logically consistent model suitable for type theory. As noted in the introduction, this inconsistency makes domain-theoretic models ill-suited as foundations for type-theoretic languages, where logical soundness is essential.