Double Bailout Fold

Posted on 2018-01-10 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 #-}
module DoubleBailoutFold (
  dbfoldr, _test_dbfoldr, main_dbfoldr
) where

import Testing
import Booleans
import Tuples
import DisjointUnions
import NaturalNumbers
import Lists
import HeadAndTail

In this post we’ll construct a hybrid of double fold and bailout fold.

Let \(A\) and \(B\) be sets. Suppose we have maps \[\delta : B \rightarrow C,\] \[\beta : A \times \lists{A} \times B \rightarrow \bool,\] \[\mu : B \rightarrow B,\] \[\psi : A \times \lists{A} \times B \rightarrow C,\] and \[\chi : A \times B \times C \times C \rightarrow C.\] Then there is a unique map \(\Theta : \lists{A} \times B \rightarrow C\) such that \[\Theta(\nil,b) = \delta(b)\] and \[\Theta(\cons(a,x),b) = \left\{\begin{array}{ll} \psi(a,x,b) & \mathrm{if}\ \beta(a,x,b) \\ \chi(a,x,b,\Theta(x,b),\Theta(x,\mu(b))) & \mathrm{otherwise}. \end{array}\right.\] We denote this \(\Theta\) by \(\dbfoldr(\delta)(\beta)(\mu)(\psi)(\chi)\).

Define \(\varepsilon : B \times \lists{A} \rightarrow C\) by \[\varepsilon(b,x) = \delta(b)\] and \(\varphi : A \times C^{B \times \lists{A}} \rightarrow C^{B \times \lists{A}}\) casewise by \[\varphi(a,g)(b,x) = \left\{\begin{array}{ll} \psi(a,\tail(x),b) & \mathrm{if}\ \beta(a,\tail(x),b) \\ \chi(a,\tail(x),b,g(b,\tail(x)),g(\mu(b),\tail(x))) & \mathrm{otherwise}, \end{array}\right.\] and let \(\Theta(x,b) = \foldr(\varepsilon)(\varphi)(x)(b,x)\). To see that \(\Theta\) solves the given equations, note that \[\begin{eqnarray*} & & \Theta(\nil,b) \\ & = & \foldr(\varepsilon)(\varphi)(\nil)(b,\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \varepsilon(b,\nil) \\ & = & \delta(b), \end{eqnarray*}\] that \[\begin{eqnarray*} & & \Theta(\cons(a,x),b) \\ & = & \foldr(\delta)(\varphi)(\cons(a,x))(b,\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(a,\foldr(\delta)(\varphi)(x))(b,\cons(a,x)) \\ & = & \bif{\beta(a,\tail(\cons(a,x)),b)}{\psi(a,\tail(\cons(a,x)),b)}{\chi(a,\tail(\cons(a,x)),b,\foldr(\varepsilon)(\varphi)(x)(b,\tail(\cons(a,x))),\foldr(\varepsilon)(\varphi)(x)(\mu(b),\tail(\cons(a,x))))} \\ & = & \bif{\beta(a,x,b)}{\psi(a,x,b)}{\chi(a,x,b,\foldr(\varepsilon)(\varphi)(x)(b,x),\foldr(\varepsilon)(\varphi)(x)(\mu(b),x))} \\ & = & \bif{\beta(a,x,b)}{\psi(a,x,b)}{\chi(a,x,b,\Theta(x,b),\Theta(x,\mu(b)))} \end{eqnarray*}\] as needed. Now suppose \(\Psi : \lists{A} \times B \rightarrow C\) also satisfies the equations; we show that \(\Psi = \Theta\) by list induction. For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \Psi(\nil,b) \\ & = & \delta(b) \\ & = & \Theta(\nil,b) \end{eqnarray*}\] as needed. For the inductive step, suppose the equations hold for all \(b\) for some \(x\), and let \(a \in A\). Then we have \[\begin{eqnarray*} & & \Psi(\cons(a,x),b) \\ & = & \bif{\beta(a,x,b)}{\psi(a,x,b)}{\chi(a,x,b,\Psi(x,b),\Psi(x,\mu(b)))} \\ & = & \bif{\beta(a,x,b)}{\psi(a,x,b)}{\chi(a,x,b,\Theta(x,b),\Theta(x,\mu(b)))} \\ & = & \Theta(\cons(a,x),b) \end{eqnarray*}\] as needed.

Implementation

We can implement \(\dbfoldr\) using the definition or the universal property.

dbfoldr, dbfoldr'
  :: (List t)
  => (b -> c)
  -> (a -> t a -> b -> Bool)
  -> (b -> b)
  -> (a -> t a -> b -> c)
  -> (a -> t a -> b -> c -> c -> c)
  -> t a -> b -> c


dbfoldr' delta beta mu psi chi x b = foldr epsilon phi x (b,x)
  where
    epsilon (a,_) = delta a

    phi a g (c,w) = if beta a (tail w) c
      then psi a (tail w) c
      else chi a (tail w) c (g (c, tail w)) (g (mu c, tail w))


-- terrible notation, or the worst notation?
dbfoldr δ β μ ψ χ = ξ
  where
    ξ z b = case uncons z of
      Left () -> δ b
      Right (Pair a x) -> if β a x b
        then ψ a x b
        else χ a x b (ξ x b) (ξ x (μ b))

We should check that these two agree.

_test_dbfoldr_equiv :: (List t, Equal (t a), Equal c)
  => t a -> b -> c
  -> Test ((b -> c) -> (a -> t a -> b -> Bool) -> (b -> b) -> (a -> t a -> b -> c) -> (a -> t a -> b -> c -> c -> c) -> t a -> b -> Bool)
_test_dbfoldr_equiv _ _ _ =
  testName "dbfoldr(delta,beta,mu,psi,chi)(x,b) == dbfoldr'(delta,beta,mu,psi,chi)(x,b)" $
  \delta beta mu psi chi x b -> eq
    (dbfoldr delta beta mu psi chi x b)
    (dbfoldr' delta beta mu psi chi x b)

Testing

Suite:

_test_dbfoldr ::
  ( TypeName a, Show a, Equal a, Arbitrary a, CoArbitrary a
  , TypeName (t a), List t, Equal (t a), Arbitrary (t a), Show (t a), CoArbitrary (t a)
  , CoArbitrary b, Arbitrary b, Show b, CoArbitrary c, Arbitrary c
  , TypeName b, TypeName c, Equal b, Equal c
  ) => Int -> Int -> t a -> b -> c -> IO ()
_test_dbfoldr size cases t b c = do
  testLabel3 "dbfoldr" t b c

  let args = testArgs size cases

  runTest args (_test_dbfoldr_equiv t b c)

Main:

main_dbfoldr :: IO ()
main_dbfoldr = do
  _test_dbfoldr 50 500 (nil :: ConsList Bool)  (zero :: Unary) (zero :: Unary)
  _test_dbfoldr 50 500 (nil :: ConsList Unary) (zero :: Unary) (zero :: Unary)
  _test_dbfoldr 50 500 (nil :: ConsList Bool)  (zero :: Unary) (true :: Bool)
  _test_dbfoldr 50 500 (nil :: ConsList Unary) (zero :: Unary) (true :: Bool)