# Bailout Recursion

Posted on 2014-05-21 by nbloomf

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude, BangPatterns #-}
module BailoutRecursion
( bailoutRec, _test_bailoutrec, main_bailoutrec
) where

import Testing
import Booleans
import Tuples
import DisjointUnions
import NaturalNumbers

So far we have defined two special recursion operators, $$\natrec(\ast)(\ast)$$ and $$\simprec$$. These act like program skeletons: fill in the slots with functions of the right signatures and get a computable function out. In this post we’ll define another operator, which we will call bailout recursion.

Suppose we have sets $$A$$ and $$B$$ and functions with the following signatures: $\begin{eqnarray*} \varphi & : & A \rightarrow B \\ \beta & : & \nats \times A \rightarrow \bool \\ \psi & : & \nats \times A \rightarrow B \\ \omega & : & \nats \times A \rightarrow A. \end{eqnarray*}$

Then there is a unique function $$\Theta : \nats \rightarrow A \rightarrow B$$ such that, for all $$n \in \nats$$ and $$a \in A$$, $\Theta(\zero,a) = \varphi(a)$ and $\Theta(\next(m),a) = \left\{ \begin{array}{ll} \psi(m,a) & \mathrm{if}\ \beta(m,a) \\ \Theta(m, \omega(m,a)) & \mathrm{otherwise}. \end{array}\right.$

This function $$\Theta$$ will be denoted $$\bailrec(\varphi)(\beta)(\psi)(\omega)$$.

We define $$ε : \nats \times A \rightarrow A + (\nats \times A)$$ by $$ε(\tup(n)(a)) = \lft(a)$$ and $$\chi : (A + (\nats \times A))^{\nats \times A} \rightarrow (A + (\nats \times A))^{\nats \times A}$$ by $\chi(h)(\tup(n)(a)) = \bif{\beta(\prev(n),a)}{\rgt(\tup(\prev(n))(a))}{h(\prev(n),\omega(\prev(n),a))}.$ Now thinking of $$((A+(\nats \times A))^{\nats \times A},ε,\chi)$$ as an inductive set, we define $$Θ : \nats \times A \rightarrow B$$ by $Θ(n,a) = \either(\varphi,\psi)(\natrec(ε)(\chi)(n)(\tup(n)(a))).$

To see that $$Θ$$ has the claimed properties, note that $\begin{eqnarray*} & & Θ(\zero,a) \\ & \let{Θ(n,a) = \either(\varphi,\psi)(\natrec(ε)(\chi)(n)(\tup(n)(a)))} = & \either(\varphi,\psi)(\natrec(ε)(\chi)(\zero)(\tup(\zero)(a))) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-zero} = & \either(\varphi,\psi)(ε(\tup(\zero)(a))) \\ & \hyp{ε(\tup(n)(a)) = \lft(a)} = & \either(\varphi,\psi)(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \varphi(a) \end{eqnarray*}$ and $\begin{eqnarray*} & & Θ(\next(n),a) \\ & \let{Θ(n,a) = \either(\varphi,\psi)(\natrec(ε)(\chi)(n)(\tup(n)(a)))} = & \either(\varphi,\psi)(\natrec(ε)(\chi)(\next(n))(\tup(\next(n))(a))) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-next} = & \either(\varphi,\psi)(\chi(\natrec(ε)(\chi)(n))(\tup(\next(n))(a))) \\ & \hyp{\chi(h)(\tup(n)(a)) = \bif{\beta(\prev(n),a)}{\rgt(\tup(\prev(n))(a))}{h(\tup(\prev(n))(a))}} = & \either(\varphi,\psi)(\bif{\beta(\prev(\next(n)),a)}{\rgt(\tup(\prev(\next(n)))(a))}{\natrec(ε)(\chi)(n)(\tup(\prev(\next(n)))(a))}) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-prev-next} = & \either(\varphi,\psi)(\bif{\beta(n,a)}{\rgt(\tup(\prev(\next(n)))(a))}{\natrec(ε)(\chi)(n)(\tup(\prev(\next(n)))(a))}) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-prev-next} = & \either(\varphi,\psi)(\bif{\beta(n,a)}{\rgt(\tup(n)(a))}{\natrec(ε)(\chi)(n)(\tup(\prev(\next(n)))(a))}) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-prev-next} = & \either(\varphi,\psi)(\bif{\beta(n,a)}{\rgt(\tup(n)(a))}{\natrec(ε)(\chi)(n)(\tup(n)(a))}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \bif{\beta(n,a)}{\either(\varphi,\psi)(\rgt(\tup(n)(a)))}{\either(\varphi,\psi)(\natrec(ε)(\chi)(n)(\tup(n)(a)))} \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \bif{\beta(n,a)}{\psi(\tup(n)(a))}{\either(\varphi,\psi)(\natrec(ε)(\chi)(n)(\tup(n)(a)))} \\ & \let{Θ(n,a) = \either(\varphi,\psi)(\natrec(ε)(\chi)(n)(\tup(n)(a)))} = & \bif{\beta(n,a)}{\psi(\tup(n)(a))}{Θ(n,a)} \end{eqnarray*}$

Next suppose $$\Psi : \nats \times A \rightarrow B$$ is another mapping which satisfies the properties of $$\Theta$$; we show that $$\Psi = \Theta$$ by induction on $$n$$. For the base case $$n = \zero$$, we have $\begin{eqnarray*} & & \Psi(\zero,a) \\ & \hyp{\Psi(\zero,a) = \varphi(a)} = & \varphi(a) \\ & \hyp{\Theta(\zero,a) = \varphi(a)} = & \Theta(\zero,a) \end{eqnarray*}$ for all $$a \in A$$. For the inductive step, suppose the equality holds for some $$n$$, and let $$a \in A$$. Then we have $\begin{eqnarray*} & & \Psi(\next(n),a) \\ & \hyp{\Psi(\next(n),a) = \bif{\beta(n,a)}{\psi(n,a)}{\Psi(n,\omega(n,a))}} = & \bif{\beta(n,a)}{\psi(n,a)}{\Psi(n,\omega(n,a))} \\ & \hyp{\Psi(n,a) = \Theta(n,a)} = & \bif{\beta(n,a)}{\psi(n,a)}{\Theta(n,\omega(n,a))} \\ & \hyp{\Theta(\next(n),a) = \bif{\beta(n,a)}{\psi(n,a)}{\Theta(n,\omega(n,a))}} = & \Theta(\next(n),a) \end{eqnarray*}$ as needed.

You might notice that in this proof, we didn’t really use $$\beta$$ or $$\psi$$. When this happens in a proof it usually means we’ve got some unnecessary details. But in this case, we will be using $$\beta$$ and $$\psi$$ later, and the piecewiseness of $$\Theta$$ will be crucial in constructing an efficient tail-recursive evaluation strategy.

## Implementation

As we did with $$\natrec$$ and $$\simprec$$, we’d like to implement $$\bailrec$$ in software. There are a couple of ways to go about this. First, the signature.

bailoutRec, bailoutRec' :: (Natural n)
=> (a -> b)
-> (n -> a -> Bool)
-> (n -> a -> b)
-> (n -> a -> a)
-> n
-> a
-> b

There’s the naive way:

bailoutRec phi beta psi omega =
let
theta n a = case unnext n of
Left () -> phi a
Right m ->
if beta m a
then psi m a
else theta m (omega m a)

in theta

And there’s the definition from the proof:

bailoutRec' phi beta psi omega n a =
either phi (uncurry psi) (naturalRec epsilon chi n (tup n a))
where
epsilon (Pair _ b) = lft b
chi h (Pair m b) = if beta (prev m) b
then rgt (tup (prev m) b)
else h (tup (prev m) (omega (prev m) b))

Unlike simple recursion, the naive implementation of bailout recursion is already tail recursive.

We should test that these are equivalent:

_test_bailoutrec_equiv :: (Natural n, Equal b)
=> n -> a -> b -> Test ((a -> b) -> (n -> a -> Bool) -> (n -> a -> b) -> (n -> a -> a) -> n -> a -> Bool)
_test_bailoutrec_equiv _ _ _ =
testName "bailoutRec(phi,beta,psi,omega)(n,a) == bailoutRec'(phi,beta,psi,omega)(n,a)" \$
\phi beta psi omega n a -> eq
(bailoutRec phi beta psi omega n a)
(bailoutRec' phi beta psi omega n a)

## What it does

Bailout recursion does some cool things that simple recursion does not. The $$\omega$$ map lets us “mutate” the initial parameter $$a$$ at each step in the recursion, and the boolean-valued function $$\beta$$ lets us short-circuit the recursion.

Also note that simple recursion and bailout recursion were carefully chosen to have tail recursive evaluation strategies. Roughly speaking, a recursive function is called tail recursive if there is “nothing left to do” after the recursive call. For example, $f(n+1) = 1 + f(n)$ is not tail recursive, because on the right hand side there is something waiting for the result of the recursive evaluation – in this case, the $$1+$$.

Arbitrary recursion is dangerous because in general, every time one function uses another we have to keep track of what remains to be done afterward – if we aren’t careful, it is very easy to write recursive functions which eat up lots of memory. Even simple recursion can blow up exponentially; the classic example is the Fibonacci numbers (which we’ll see later).

In contrast, a tail recursive function by definition doesn’t have to keep track of what remains to be done after the recursion. Our recursion operators, $$\natrec(\ast)(\ast)$$, $$\simprec$$, and $$\bailrec$$, are carefully chosen so that they have tail recursive implementations.

By the way, I think it’s helpful to compare the difference between arbitrary recursion and recursion operators to the difference between arbitrary GOTOs and structured loops. In both cases we have a simple but dangerous primitive operation that is hidden behind a safer and more meaningful interface. A for loop means “repeat this some number of times”; while the meaning of simple recursion is given by its universal property.

As with natural and simple recursion, the “uniqueness” part of bailout recursion is also handy. To be a little more explicit, it says the following.

Let $$A$$ and $$B$$ be sets, with mappings $\begin{eqnarray*} \varphi & : & A \rightarrow B \\ \beta & : & \nats \times A \rightarrow \bool \\ \psi & : & \nats \times A \rightarrow B \\ \omega & : & \nats \times A \rightarrow A. \end{eqnarray*}$ Then $$\bailrec(\varphi)(\beta)(\psi)(\omega)$$ is the unique solution $$f : \nats \times A \rightarrow B$$ to the following system of functional equations for all $$k \in \nats$$, $$a \in A$$: $\left\{\begin{array}{l} f(\zero,a) = \varphi(a) \\ f(\next(k),a) = \bif{\beta(k,a)}{\psi(m,a)}{f(k,\omega(k,a))} \end{array}\right.$

## Testing

Suite:

_test_bailoutrec ::
( Equal a, Show a, Arbitrary a, CoArbitrary a, TypeName a
, Equal b, Show b, Arbitrary b, CoArbitrary b, TypeName b
, Equal n, Show n, Arbitrary n, CoArbitrary n, TypeName n, Natural n
) => Int -> Int -> n -> a -> b -> IO ()
_test_bailoutrec size cases n a b = do
testLabel3 "bailoutRec" n a b
let args = testArgs size cases

runTest args (_test_bailoutrec_equiv n a b)

Main:

main_bailoutrec :: IO ()
main_bailoutrec = do
let
b = true :: Bool
n = zero :: Unary
x = lft true :: Union Bool Unary
y = tup zero zero :: Pair Unary Unary

_test_bailoutrec 100 100 n b b
_test_bailoutrec 100 100 n n b
_test_bailoutrec 100 100 n b n
_test_bailoutrec 100 100 n n n
_test_bailoutrec 100 100 n x x
_test_bailoutrec 100 100 n y y