Bailout Recursion

Posted on 2014-05-21 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

\(\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}\) \(\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}\) \(\newcommand{\a}{a}\) \(\newcommand{\b}{b}\) \(\newcommand{\c}{c}\) \(\newcommand{\p}{p}\) \(\newcommand{\q}{q}\) \(\newcommand{\r}{r}\) \(\newcommand{\s}{s}\) \(\newcommand{\x}{x}\) \(\newcommand{\y}{y}\) \(\newcommand{\z}{z}\) \(\newcommand{\bool}{\mathbb{B}}\) \(\newcommand{\btrue}{\mathsf{true}}\) \(\newcommand{\bfalse}{\mathsf{false}}\) \(\newcommand{\bnot}{\mathsf{not}}\) \(\newcommand{\band}{\mathbin{\mathsf{and}}}\) \(\newcommand{\bor}{\mathbin{\mathsf{or}}}\) \(\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}\) \(\newcommand{\beq}{\mathsf{eq}}\) \(\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}\) \(\newcommand{\id}{\mathsf{id}}\) \(\newcommand{\compose}{\mathsf{compose}}\) \(\newcommand{\const}{\mathsf{const}}\) \(\newcommand{\apply}{\mathsf{apply}}\) \(\newcommand{\flip}{\mathsf{flip}}\) \(\newcommand{\flipB}{\mathsf{flip2}}\) \(\newcommand{\flipC}{\mathsf{flip3}}\) \(\newcommand{\flipD}{\mathsf{flip4}}\) \(\newcommand{\flipE}{\mathsf{flip5}}\) \(\newcommand{\clone}{\mathsf{clone}}\) \(\newcommand{\cloneC}{\mathsf{clone3}}\) \(\newcommand{\composeAonB}{\mathsf{compose1on2}}\) \(\newcommand{\composeAonC}{\mathsf{compose1on3}}\) \(\newcommand{\composeAonD}{\mathsf{compose1on4}}\) \(\newcommand{\composeBonA}{\mathsf{compose2on1}}\) \(\newcommand{\composeBonB}{\mathsf{compose2on2}}\) \(\newcommand{\composeConA}{\mathsf{compose3on1}}\) \(\newcommand{\ptrue}{\mathsf{ptrue}}\) \(\newcommand{\pfalse}{\mathsf{pfalse}}\) \(\newcommand{\pnot}{\mathsf{pnot}}\) \(\newcommand{\pand}{\mathbin{\mathsf{pand}}}\) \(\newcommand{\por}{\mathbin{\mathsf{por}}}\) \(\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}\) \(\newcommand{\fst}{\mathsf{first}}\) \(\newcommand{\snd}{\mathsf{second}}\) \(\newcommand{\dup}{\mathsf{dup}}\) \(\newcommand{\tup}{\mathsf{tup}}\) \(\newcommand{\tSwap}{\mathsf{swap}_{\times}}\) \(\newcommand{\tPair}{\mathsf{pair}_{\times}}\) \(\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}\) \(\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}\) \(\newcommand{\tupL}{\mathsf{tupL}}\) \(\newcommand{\tupR}{\mathsf{tupR}}\) \(\newcommand{\uncurry}{\mathsf{uncurry}}\) \(\newcommand{\curry}{\mathsf{curry}}\) \(\newcommand{\lft}{\mathsf{left}}\) \(\newcommand{\rgt}{\mathsf{right}}\) \(\newcommand{\either}{\mathsf{either}}\) \(\newcommand{\uSwap}{\mathsf{swap}_{+}}\) \(\newcommand{\uPair}{\mathsf{pair}_{+}}\) \(\newcommand{\uAssocL}{\mathsf{assocL}_{+}}\) \(\newcommand{\uAssocR}{\mathsf{assocR}_{+}}\) \(\newcommand{\isLft}{\mathsf{isLeft}}\) \(\newcommand{\isRgt}{\mathsf{isRight}}\) \(\newcommand{\nats}{\mathbb{N}}\) \(\newcommand{\zero}{\mathsf{0}}\) \(\newcommand{\next}{\mathsf{next}}\) \(\newcommand{\unnext}{\mathsf{unnext}}\) \(\newcommand{\iszero}{\mathsf{isZero}}\) \(\newcommand{\prev}{\mathsf{prev}}\) \(\newcommand{\natrec}{\mathsf{natrec}}\) \(\newcommand{\simprec}{\mathsf{simprec}}\) \(\newcommand{\bailrec}{\mathsf{bailrec}}\) \(\newcommand{\mutrec}{\mathsf{mutrec}}\) \(\newcommand{\dnatrec}{\mathsf{dnatrec}}\) \(\newcommand{\normrec}{\mathsf{normrec}}\) \(\newcommand{\findsmallest}{\mathsf{findsmallest}}\) \(\newcommand{\mnormrec}{\mathsf{mnormrec}}\) \(\newcommand{\nequal}{\mathsf{eq}}\) \(\newcommand{\nplus}{\mathsf{plus}}\) \(\newcommand{\ntimes}{\mathsf{times}}\) \(\newcommand{\nleq}{\mathsf{leq}}\) \(\newcommand{\ngeq}{\mathsf{geq}}\) \(\newcommand{\nminus}{\mathsf{minus}}\) \(\newcommand{\nmax}{\mathsf{max}}\) \(\newcommand{\nmin}{\mathsf{min}}\) \(\newcommand{\ndivalg}{\mathsf{divalg}}\) \(\newcommand{\nquo}{\mathsf{quo}}\) \(\newcommand{\nrem}{\mathsf{rem}}\) \(\newcommand{\ndiv}{\mathsf{div}}\) \(\newcommand{\ngcd}{\mathsf{gcd}}\) \(\newcommand{\ncoprime}{\mathsf{coprime}}\) \(\newcommand{\nlcm}{\mathsf{lcm}}\) \(\newcommand{\nmindiv}{\mathsf{mindiv}}\) \(\newcommand{\nisprime}{\mathsf{isPrime}}\) \(\newcommand{\npower}{\mathsf{power}}\) \(\newcommand{\nchoose}{\mathsf{choose}}\) \(\newcommand{\dom}{\mathsf{dom}}\) \(\newcommand{\cod}{\mathsf{cod}}\) \(\newcommand{\lists}[1]{\mathsf{List}(#1)}\) \(\newcommand{\nil}{\mathsf{nil}}\) \(\newcommand{\cons}{\mathsf{cons}}\) \(\newcommand{\uncons}{\mathsf{uncons}}\) \(\newcommand{\isnil}{\mathsf{isNil}}\) \(\newcommand{\tail}{\mathsf{tail}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\foldr}{\mathsf{foldr}}\) \(\newcommand{\foldl}{\mathsf{foldl}}\) \(\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}\) \(\newcommand{\unfoldN}{\mathsf{unfoldN}}\) \(\newcommand{\dfoldr}{\mathsf{dfoldr}}\) \(\newcommand{\cfoldr}{\mathsf{cfoldr}}\) \(\newcommand{\bfoldr}{\mathsf{bfoldr}}\) \(\newcommand{\dbfoldr}{\mathsf{dbfoldr}}\) \(\newcommand{\lfoldr}{\mathsf{lfoldr}}\) \(\newcommand{\snoc}{\mathsf{snoc}}\) \(\newcommand{\revcat}{\mathsf{revcat}}\) \(\newcommand{\rev}{\mathsf{rev}}\) \(\newcommand{\last}{\mathsf{last}}\) \(\newcommand{\cat}{\mathsf{cat}}\) \(\newcommand{\addlength}{\mathsf{addlength}}\) \(\newcommand{\length}{\mathsf{length}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\at}{\mathsf{at}}\) \(\newcommand{\map}{\mathsf{map}}\) \(\newcommand{\range}{\mathsf{range}}\) \(\newcommand{\zip}{\mathsf{zip}}\) \(\newcommand{\zipPad}{\mathsf{zipPad}}\) \(\newcommand{\unzip}{\mathsf{unzip}}\) \(\newcommand{\prefix}{\mathsf{prefix}}\) \(\newcommand{\suffix}{\mathsf{suffix}}\) \(\newcommand{\lcp}{\mathsf{lcp}}\) \(\newcommand{\lcs}{\mathsf{lcs}}\) \(\newcommand{\all}{\mathsf{all}}\) \(\newcommand{\any}{\mathsf{any}}\) \(\newcommand{\tails}{\mathsf{tails}}\) \(\newcommand{\inits}{\mathsf{inits}}\) \(\newcommand{\filter}{\mathsf{filter}}\) \(\newcommand{\elt}{\mathsf{elt}}\) \(\newcommand{\addcount}{\mathsf{addcount}}\) \(\newcommand{\count}{\mathsf{count}}\) \(\newcommand{\repeat}{\mathsf{repeat}}\) \(\newcommand{\sublist}{\mathsf{sublist}}\) \(\newcommand{\infix}{\mathsf{infix}}\) \(\newcommand{\select}{\mathsf{select}}\) \(\newcommand{\unique}{\mathsf{unique}}\) \(\newcommand{\delete}{\mathsf{delete}}\) \(\newcommand{\dedupeL}{\mathsf{dedupeL}}\) \(\newcommand{\dedupeR}{\mathsf{dedupeR}}\) \(\newcommand{\common}{\mathsf{common}}\) \(\newcommand{\disjoint}{\mathsf{disjoint}}\) \(\newcommand{\sublists}{\mathsf{sublists}}\) \(\newcommand{\take}{\mathsf{take}}\) \(\newcommand{\drop}{\mathsf{drop}}\) \(\newcommand{\takeBut}{\mathsf{takeBut}}\) \(\newcommand{\dropBut}{\mathsf{dropBut}}\) \(\newcommand{\takeWhile}{\mathsf{takeWhile}}\) \(\newcommand{\dropWhile}{\mathsf{dropWhile}}\)

This page is part of a series on Arithmetic Made Difficult.

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