Range

Posted on 2017-05-05 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 Range
  ( range, _test_range, main_range
  ) where

import Testing
import Tuples
import DisjointUnions
import NaturalNumbers
import Plus
import Lists
import Snoc
import Cat
import Length
import Map
import UnfoldN

For our first application of \(\unfoldN(\ast)\) we’ll define a function, \(\range\), that constructs lists of natural numbers. There are a few ways to do this. We could take an argument \(n\) and construct the list of natural numbers from \(\zero\) to \(n\), but this is too specialized. We could instead take two arguments \(a\) and \(b\) and construct the list of natural numbers from \(a\) to \(b\), but we’ll have to check whether or not the arguments are in order. A third option – and the one we’ll take – is to take two arguments \(a\) and \(b\), and construct the list of the first \(b\) natural numbers starting from \(a\).

Define \(f : \nats \rightarrow \ast + \nats \times \nats\) by \[f(k) = (\next(k),k).\] We then define \(\range : \nats \times \nats \rightarrow \lists{\nats}\) by \[\range(a,b) = \unfoldN(f,b,a).\]

In Haskell:

range :: (List t, Natural n, Equal n) => n -> n -> t n
range a b = unfoldN f b a
  where f k = rgt (tup (next k) k)

Since \(\range\) is an \(\unfoldN(\ast)\), it is the unique solution to a system of functional equations.

\(\range\) is the unique \(f : \nats \times \nats \rightarrow \lists{\nats}\) satisfying the following system of equations for all \(a,b \in \nats\). \[\left\{\begin{array}{l} f(a,\zero) = \nil \\ f(a,\next(b)) = \cons(a,f(\next(a),b)) \end{array}\right.\]

_test_range_zero :: (List t, Natural n, Equal (t n), Equal n)
  => t n -> Test (n -> Bool)
_test_range_zero t =
  testName "range(a,zero) == nil" $
  \a -> eq (range a zero) (nil `withTypeOf` t)


_test_range_next :: (List t, Natural n, Equal (t n), Equal n)
  => t n -> Test (n -> n -> Bool)
_test_range_next t =
  testName "range(a,next(b)) == cons(a,range(next(a),b))" $
  \a b -> eq
    ((range a (next b)) `withTypeOf` t)
    (cons a (range (next a) b))

A special case.

For all \(a \in \nats\) we have \(\range(a,\next(\zero)) = \cons(a,\nil)\).

Note that \[\begin{eqnarray*} & & \range(a,\next(\zero)) \\ & = & \cons(a,\range(\next(a),\zero)) \\ & = & \cons(a,\nil) \end{eqnarray*}\] as claimed.

_test_range_one :: (List t, Natural n, Equal (t n), Equal n)
  => t n -> Test (n -> Bool)
_test_range_one t =
  testName "range(a,next(zero)) == cons(a,nil)" $
  \a -> eq (range a (next zero)) ((cons a nil) `withTypeOf` t)

The \(\length\) of a \(\range\) is predictable.

For all \(a,b \in \nats\), we have \(\length(\range(a,b)) = b\).

We proceed by induction on \(b\). For the base case \(b = \zero\), we have \[\begin{eqnarray*} & & \length(\range(a,b)) \\ & = & \length(\range(a,\zero)) \\ & = & \length(\nil) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \zero \\ & = & b \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(b\). Now \[\begin{eqnarray*} & & \length(\range(a,\next(b))) \\ & = & \length(\cons(a,\range(\next(a),b))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \next(\length(\range(\next(a),b))) \\ & = & \next(b) \end{eqnarray*}\] as claimed.

_test_range_length :: (List t, Natural n, Equal (t n), Equal n)
  => t n -> Test (n -> n -> Bool)
_test_range_length t =
  testName "length(range(a,b)) == b" $
  \a b -> eq (length ((range a b) `withTypeOf` t)) b

\(\range\) interacts with \(\snoc\).

For all \(a,b \in \nats\) we have \[\range(a,\next(b)) = \snoc(\nplus(a,b),\range(a,b)).\]

We proceed by induction on \(b\). For the base case \(b = \zero\), we have \[\begin{eqnarray*} & & \range(a,\next(b)) \\ & = & \range(a,\next(\zero)) \\ & = & \cons(a,\nil) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \snoc(a,\nil) \\ & = & \snoc(\nplus(a,\zero),\range(a,\zero)) \\ & = & \snoc(\nplus(a,b),\range(a,b)) \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(b\). Then we have \[\begin{eqnarray*} & & \range(a,\next(\next(b))) \\ & = & \cons(a,\range(\next(a),\next(b))) \\ & = & \cons(a,\snoc(\nplus(\next(a),b),\range(\next(a),b))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \snoc(\nplus(\next(a),b),\cons(a,\range(\next(a),b))) \\ & = & \snoc(\nplus(a,\next(b)),\range(a,\next(b))) \end{eqnarray*}\] as needed.

_test_range_snoc :: (List t, Natural n, Equal (t n), Equal n)
  => t n -> Test (n -> n -> Bool)
_test_range_snoc t =
  testName "range(a,next(b)) == snoc(plus(a,b),range(a,b))" $
  \a b -> eq
    ((range a (next b)) `withTypeOf` t)
    (snoc (plus a b) (range a b))

\(\range\) interacts with \(\nplus\) in its second argument.

If \(a,b,c \in \nats\), we have \[\range(a,\nplus(b,c)) = \cat(\range(a,b),\range(\nplus(a,b),c)).\]

We proceed by induction on \(c\). For the base case \(c = \zero\), we have \[\begin{eqnarray*} & & \range(a,\nplus(b,c)) \\ & = & \range(a,\nplus(b,\zero)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-zero-right} = & \range(a,b) \\ & = & \cat(\range(a,b),\nil) \\ & = & \cat(\range(a,b),\range(\nplus(a,b),\zero)) \\ & = & \cat(\range(a,b),\range(\nplus(a,b),c)) \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(c\). Using the inductive hypothesis we have \[\begin{eqnarray*} & & \range(a,\nplus(b,\next(c))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \range(a,\next(\nplus(b,c))) \\ & = & \snoc(\nplus(a,\nplus(b,c)),\range(a,\nplus(b,c))) \\ & = & \snoc(\nplus(a,\nplus(b,c)),\cat(\range(a,b),\range(\nplus(a,b),c))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \snoc(\nplus(\nplus(a,b),c),\cat(\range(a,b),\range(\nplus(a,b),c))) \\ & = & \cat(\range(a,b),\snoc(\nplus(\nplus(a,b),c),\range(\nplus(a,b),c))) \\ & = & \cat(\range(a,b),\range(\nplus(a,b),\next(c))) \end{eqnarray*}\] as needed.

_test_range_plus_right :: (List t, Natural n, Equal (t n), Equal n)
  => t n -> Test (n -> n -> n -> Bool)
_test_range_plus_right t =
  testName "range(a,plus(b,c)) == cat(range(a,b),range(plus(a,b),c))" $
  \a b c -> eq
    ((range a (plus b c)) `withTypeOf` t)
    (cat (range a b) (range (plus a b) c))

\(\range\) interacts with \(\next\) in its first argument.

For all \(a,b \in \nats\) we have \[\range(\next(a),b) = \map(\next)(\range(a,b)).\]

We proceed by induction on \(b\). For the base case \(b = \zero\), we have \[\begin{eqnarray*} & & \range(\next(a),b) \\ & = & \range(\next(a),\zero) \\ & = & \nil \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \map(\next)(\nil) \\ & = & \map(\next)(\range(a,\zero)) \\ & = & \map(\next)(\range(a,b)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(b\). Now \[\begin{eqnarray*} & & \range(\next(a),\next(b)) \\ & = & \cons(\next(a),\range(\next(\next(a)),b)) \\ & = & \cons(\next(a),\map(\next)(\range(\next(a),b))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \map(\next)(\cons(a,\range(\next(a),b))) \\ & = & \map(\next)(\range(a,\next(b))) \end{eqnarray*}\] as needed.

_test_range_next_left :: (List t, Natural n, Equal (t n), Equal n)
  => t n -> Test (n -> n -> Bool)
_test_range_next_left t =
  testName "range(next(a),b) == map(next,range(a,b))" $
  \a b -> eq
    ((range (next a) b) `withTypeOf` t)
    (map next (range a b))

And \(\range\) interacts with \(\nplus\) in its first argument. In this theorem we use a bit of new notation. When a function argument is replaced by a dash, we implicitly mean lambda-abstraction. That is, if \(f\) is a function, then \(f(-)\) is short for \(\lambda x. f(x)\).

If \(a,b,c \in \nats\), we have \[\range(\nplus(a,b),c) = \map(\nplus(a,-))(\range(b,c)).\]

We proceed by induction on \(a\). For the base case \(a = \zero\) note that \(\nplus(a,-) = \id\), since for all \(b \in \nats\) we have \[\nplus(\zero,-)(b) = \nplus(\zero,b) = b.\] Thus \[\begin{eqnarray*} & & \range(\nplus(a,b),c) \\ & = & \range(\nplus(\zero,b),c) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-zero} = & \range(b,c) \\ & = & \map(\id)(\range(b,c)) \\ & = & \map(\nplus(\zero,-))(\range(b,c)) \\ & = & \map(\nplus(a,-))(\range(b,c)) \end{eqnarray*}\] as needed. For the inductive step, suppose the result holds for some \(a\). Now \[\begin{eqnarray*} & & \range(\nplus(\next(a),b),c) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next} = & \range(\next(\nplus(a,b)),c) \\ & = & \map(\next)(\range(\nplus(a,b),c)) \\ & = & \map(\next)(\map(\nplus(a,-))(\range(b,c))) \\ & = & (\map(\next) \circ \map(\nplus(a,-)))(\range(b,c)) \\ & = & \map(\next(\nplus(a,-)))(\range(b,c)) \\ & = & \map(\nplus(\next(a),-))(\range(b,c)) \end{eqnarray*}\] as needed.

_test_range_plus_left :: (List t, Natural n, Equal (t n), Equal n)
  => t n -> Test (n -> n -> n -> Bool)
_test_range_plus_left t =
  testName "range(plus(a,b),c) == map(plus(a,-),range(b,c))" $
  \a b c -> eq
    ((range (plus a b) c) `withTypeOf` t)
    (map (plus a) (range b c))

Testing

Suite:

_test_range ::
  ( TypeName n, Natural n, Equal n, Show n, Arbitrary n
  , TypeName (t n), List t, Equal (t n), Show (t n), Arbitrary (t n)
  ) => Int -> Int -> t n -> IO ()
_test_range size cases t = do
  testLabel1 "range" t

  let args = testArgs size cases

  runTest args (_test_range_zero t)
  runTest args (_test_range_next t)
  runTest args (_test_range_one t)
  runTest args (_test_range_length t)
  runTest args (_test_range_snoc t)
  runTest args (_test_range_plus_right t)
  runTest args (_test_range_next_left t)
  runTest args (_test_range_plus_left t)

Main:

main_range :: IO ()
main_range = do
  _test_range 20 100 (nil :: ConsList Unary)