Later we’ll go into a more detail about what a function is set-theoretically, but to get started that brutalist interpretation of functions you learned sometime after Kindergarten will do. So let’s have the idea of one thing succeeding another housed in a successor function \(S(n)\;\). And yet we won’t say something like

\begin{align*} S(n) = n + 1 \end{align*}

because that would be too, well, brutalist.

For example, if we start at \(0\), the successor to \(0\) is \(1\;\), or \(S(0) = 1\;\). But if we’re going to be highly abstract and pure about this, we don’t want or need to connect this to any actual numerical symbols of base\(_{10}\) like \(1\;\). So we’ll just use the usual numerical symbols as reminders. Let’s So in order to Instead, we’ll just keep reapplying the successor function \(S\;\) similar to nesting Russian dolls Russian or matryoshka dolls:

\begin{align*} 0 &= 0 \\ 1 &= S(0) \\ 2 &= S(S(0)) \\ 3 &= S(S(S(0))) \\ 4 &= S(S(S(S(0)))) \\ \ldots \end{align*}

Awkward? YMMV Your mileage may vary. . But we have to admit we’ve defined something akin to the natural numbers using just the constant \(0\) and a successor function applied to it. Now, let’s define addition on this system. To do this we’ll use these two identities

\begin{align} x + 0 &= x \\ x + s(y) &= s(x + y) \end{align}

This should cover all possible cases of addition. Testing, let’s add \(1\) and \(2\;\) or \(s(0) + s(s(0))\;\)

\begin{align} s(0) + s(s(0)) &= \\ s(s(0) + s(0)) &= \\ s(s(s(0)) + 0) &= s(s(s(0))) \end{align}

• We apply (2) to (3) to get (4); in effect abstracting \(1+2\;\), the left side of (2), to the successor of \(1+1\;\), the right side of (2).
• But now the inner part of (4), namely \(s(0) + s(0)\;\), resembles (2) allowing us to match the first \(s(0)\) to \(x\) and the second to \(s(y)\), which in turn allows us to rewrite it as \(s(s(0) + 0)\;\).
• But according to (1) \(s(0) + 0 = s(0)\;\;\), leaving \(s(s(0))\;\)
• Including back in the outermost \(s\) we now have \(s(s(s(0)))\;\) our answer.

What have we accomplished with this convoluted method? For one, we’ve reduced the entire idea of the natural numbers, along with adding two of these reimagined natural numbers, to just a small set of symbols, namely

• a constant symbol \(0\)
• variable symbols \(x\) and \(y\)
• and a function symbol \(s\)

And with these four symbols we create statements made of terms built from our symbols as in (1) and (2), e.g., \(x + 0\;\) is term, and \(s(x + y)\;\) is another term. This allows us to state our problem as terms, then rewrite these terms step-by-step as we did above to get to a final term rewrite that is our answer. And so we have a term rewriting system that provides addition of our natural numbers Rewriting is basically what you do when you, e.g., take steps to simplify or reduce a fraction. More on normal or canonical forms later. . As Madhavan Mukund says Mukund lecture notes.

So what’s the alternative? Your modern digital computer creates a human-friendly world of numbers and addition with the help of base\(_{2}\) binary numbers, computer circuit board logic gates, and lots and lots of Assembler code to manage it all. Then come the higher languages which present math as we normally see it, e.g., \(1 + 1 = 2\;\). When seen in this light, we might begin to appreciate a very basic, fundamental fact about modern computing, namely, we can create strategies to accomplish logical calculations by manipulating (rewriting) terms built of symbols. Again, this adds a whole new dimension to our age-old math world mix of scrolls, paper, books, pencils, blackboards and chalk, and those mysterious mental representations of math inside our human brains.

Example of induction: if one domino falls, so will the next.

Simplistic as our natural number system in the previous section may seem, there’s actually quite a bit of math theory to unpack to really understand what just happened. When we build a number up from repeated or nested application of the successor function \(s\) we were using the ideas of induction and recursion You may or may not have encountered induction. Typically, a math course will introduce it as a proof strategy. .

Again, this may seem very simplistic, but the idea of induction is inherent to the natural numbers. So if \(\mathbb{N}\;\) is also referred to as the counting numbers, then we count or enumerate things with them—going up as high as we need to

Table 1: Enumeration of the first ten primes

1	2	3	4	5	6	7	8	9	10
2	3	5	7	11	13	17	19	23	29

Let’s make a quick look-up table in Haskell for Table 1

primeEnum n | (n < 11) && (n > 0) = case (n) of
                          1  -> 2
                          2  -> 3
                          3  -> 5
                          4  -> 7
                          5  -> 11
                          6  -> 13
                          7  -> 17
                          8  -> 19
                          9  -> 23
                          10 -> 29
            | otherwise = error "We only know the first ten primes."
            

primeEnum 9

23

Mathematicians abstracted “the next one” by saying for any \(n \in \mathbb{N}\;\), there will be a \(n+1 \in \mathbb{N}\;\;\) “next one after \(n\;\)”. Myriad phenomena in life and math lend themselves to this “if you’ve got this one, you can get next one” idea.

𝖟𝕭 zB: German abbreviation for zum Beispiel, or for example. : A classic proof using mathematical induction is the proposition Propositions are statements or assertions that can be proven to be either true or false. Make sure you went down this rabbit hole.

\begin{align*} P(n) = 0 + 1 + 2 + 3 + \ldots + n = \frac{n(n+1)}{2} \end{align*}

To be clear, we’re not deriving this formula The story behind this formula is interesting. See this for the backstory. Note the formula is
\begin{align*} \frac{\text{(number of pairs)} ⋅ \text{(sum of each pair)}}{2} \end{align*}
, we’re attempting to prove it. So for example if we add the first three numbers, according to the formula we should get \(6\;\)

\begin{align*} \frac{(3)(3+1)}{2} = \frac{(12)}{2} = 6 \end{align*}

An induction proof is a two-step process: a base case and an induction step

Base case: \(P(0)\)

\(P(0)\;\) is trivial. Just plug in \(0\)

\begin{align*} \frac{(0)(0+1)}{2} = \frac{(0\cdot1)}{2} = 0 \end{align*}

Inductive step: Now we have to consider \(n \gt 0\;\) cases. The whole idea is to show that for any number \(k \ge 0\;\), if \(P(k)\;\) works, so will \(P(k+1)\;\)

We start by assuming what is called the induction hypothesis, i.e., that our statement \(P\) will hold for \(P(n)\;\). Here we’re saying for the unique case when \(n = k\;\) that \(P(k)\;\) is true

\begin{align} 0 + 1 + 2 + \ldots + k = \frac{k(k+1)}{2} \end{align}

Good. Now we want to consider \(P(k+1)\;\). We’ll just add it on both sides since it is the next step after \(k\;\)

\begin{align*} (0 + 1 + 2 + \ldots + k) + (k + 1) = \frac{k(k+1)}{2} + (k+1) \end{align*}

Now, we consider just the right side of this equation and do some algebraic manipulation

\begin{align*} \frac{k(k+1)}{2} + (k+1) &= \frac{k(k+1)}{2} + \frac{2(k+1)}{2} \\ &= \frac{k(k+1)+2(k+1)}{2} &= \frac{(k+1)(k+2)}{2} &= \frac{(k+1)((k+1)+1)}{2} \end{align*}

Going back to our original left-hand side

\begin{align} (0 + 1 + 2 + \ldots + k) + (k + 1) = \frac{(k+1)((k+1)+1)}{2} \end{align}

Now, compare (6) with (7). On the left-hand side of (7) we have the next step \((k+1)\;\) and on the right-hand side of (7) we have in the numerator the “number of pairs” increased from \(k\;\) to \(k+1\;\) and the “sum of each pair” likewise increased by \(1\;\) from \(k+1\) to \(k + 1 + 1\;\). Through algebraic manipulation we have proved that “the next one” will indeed increase as we might want it to. For example, if we total the first ten numbers

\begin{align*} \text{Total sum} = \frac{10 \cdot 11}{2} \end{align*}

and totalling the next number \(11\) will just be

\begin{align*} \text{Total sum} = \frac{11 \cdot 12}{2} \end{align*}

which is covered in our proof for any \(k+1\;\).

We’ll do a Haskell example where Gauss’ summing formula will be of use.

⇲ In a sequence on natural numbers \(1 \ldots n\;\) one of the numbers \(k\;\) is missing, e.g., \(1, \ldots, k-1, k+1, \ldots, n\;\). Find which number it is.

If we have a relatively short list we can no doubt spot it, e.g., \(1,2,4,5\;\); obviously \(3\;\) is missing. But what if our sequence is thousands of numbers long. For example, with Haskell’s list completion we can create a list representing a very big sequence

[1..100]

[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100]

Still doable, but for a sequence going from \(1\) to \(1,000\) it would be hard to spot the missing number. One solution would be to recurse through the list testing each number that it was the next after the previous

:{
missingNumberGen n m | 
:}

:{
missingTest1 xs
:}

For example, what if we add up the first three consecutive odd numbers

Peano postulated axioms, givens, starting points. Using set theory methods, he attempted to

According to a modern treatment, there are five basic Peano axioms Peano actually had nine axioms; however, four of these deal with the equality of his natural numbers, which we’ll deal with later when we explore relations, a more general concept above functions. . The first axiom states

1. \(0\) is a natural number, i.e., \(0 \in \mathbb{N}\)

This is our starting point. Peano then gives four axioms to establish equality

2. For every natural number \(n\), \(S(n)\;\) is a natural number. That is, the natural numbers are closed under \(S\;\). Or \(x \in \mathbb{N} \rightarrow Sx \in \mathbb{N}\;\;\).

1. For all natural numbers x and y, if x = y, then y = x. That is, equality is symmetric.

Turning math into code means we must first decide which data structure to use. For our string of \(1\)’s we will use the Haskell list data structure. This may seem ironic to a budding mathematician who went down the set theory rabbit holes above. Yes, so much of math can be seen as set theory-based. And no, a list is not a set. And yes, Haskell has a library for sets. But as beginners we will simulate sets with lists We could also represent our \(1\)’s as a string, i.e., like text between double-quotes, but any string in Haskell is just a list of the text’s individual characters, e.g., "1111" is really just ['1','1','1','1']. . This means our set of \(1\)’s will be represented as a list with the integer \(1\) repeated as its elements, e.g., [1,1,1,1,1] is \(11111\).

First we’ll try a really primitive way to do UNS subtraction

• Put \(1\)’s into lists,
• Apply the built-in list element counter function, length, on each to count the number of \(1\)’s in each,
• Subtract one from the other.

Not very enlightening, but it works

(length [1,1,1,1]) - (length [1,1])

2

We can write our own function uns1 for this taking two values as input

uns1 list1 list2 = (length list1) - (length list2)

uns1 [1,1,1,1] [1,1]

2

Now, let’s create a better function utilizing Haskell’s type and recursion features

unsSub2 :: [a] -> [a] -> [a]
unsSub2 l1x l2x | null l1x = l2x
                | null l2x = l1x
unsSub2 (l1:l1x) (l2:l2x) = unsSub2 l1x l2x

We’re relying on Haskell’s pattern matching and guards to accomplish loop-like behavior … a lot at once.

It seems to work when the subtrahend is smaller than the minuend

unsSub2 [1,1,1,1,1,1] [1,1,1,1,1]

[1]

unsSub2 [1,1] [1,1]

[]

But the following test exposes a problem, i.e., unsSub2 gets things backwards when the subtrahend is larger than the minuend. This is a logic error, i.e., the code evaluates and runs, but produces bad output

unsSub2 [1,1] [1,1,1,1]

[1,1]

We can correct this by changing the second line 3

1: :{
2: unsSub21 :: [a] -> [a] -> [a]
3: unsSub21 l1x l2x | null l1x = []
4:                 | null l2x = l1x
5: unsSub21 (l1:l1x) (l2:l2x) = unsSub21 l1x l2x
6: :}

Now it works

unsSub21 [1,1,1,1,1] [1,1,1,1,1,1,1]

[]

Another attempt would have us turn any extra \(1\)’s in the minuend turned into \(-1\)’s. No, it’s not exactly UNS, but we’re just practicing here. unsSub3 below should do it, but the first evaluation gives an error Eventually you’ll be a pro with Haskell error messages, but for now we’ll just have to puzzle them out. : There is something wrong with the type declaration.

unsSub3 :: [a] -> [a] -> [a]
unsSub3 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub3 (l1:l1x) (l2:l2x) = unsSub3 l1x l2x

No instance for (Num a) arising from a use of ‘negate’
  ...

One trick is to simply comment out your type declaration and try again

-- unsSub3 :: [a] -> [a] -> [a]
unsSub3 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub3 (l1:l1x) (l2:l2x) = unsSub3 l1x l2x

When we allow Haskell to infer the type, we have success.

:t unsSub3

unsSub3 :: Num a => [a] -> [a] -> [a]

Because we’re using negate our list type [a] cannot be just anything, rather, the a’s, the list elements, must be instances of the class Num. Retrying with Haskell’s type declaration

:{
unsSub3 :: Num a => [a] -> [a] -> [a]
unsSub3 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub3 (l1:l1x) (l2:l2x) = unsSub3 l1x l2x
:}

this evaluates. Now

unsSub3 [1,1] [1,1,1,1,1]

[-1,-1,-1]

One improvement would be to make sure our input lists are made up of just ones. For this we have a choice of Haskell built-ins like filter, all, map, any, and elem

list1 = [1,1,1,1]
list2 = [-1,1,1,1,1]

One version using any to test for not equal to 1

any (/=1) list2

True

Another version of testing for not equal to 1 using a (lambda) anonymous function

any (\x -> x /= 1) list2  -- checks if any in the list conform to test

True

We can test two lists by using Boolean or (||)

(any (\x -> x /= 1) list1) || (any (\x -> x /= 1) list2)

True

filter returns a list with elements conforming to the test

filter (/=1) [1,1,1,1]

[]

all checks if all elements conform to test and returns Boolean

all (==1)  [1,1,1,2]

False

map, (see Maps and filters) which we’ll use extensively, applies the test to a list and outputs a new list with the outcomes of each test on each input list element. Here the test is an anonymous function testing again for not equal to 1

map (\x -> (x > 1) || (x < 1)) [-1,1,2,3,4]

[True,False,True,True,True]

elem with type Eq a => a -> [a] -> Bool is not quite as handy since it doesn’t allow for a Boolean predicate test. So yes, we could test if 1 is an element of a list, but not if all are

elem 1 [1,1,1,1] || elem 1 [1,2,3]

True

We can “trick” elem into helping us. First, we produce a list created from map as above testing each element for 1

map (\x -> x /= 1) [1,1,-1,1]

[False,False,True,False]

Then elem will tell us if any elements were not equal to 1

elem True $ map (\x -> x /= 1) [1,1,-1,1]

True

We’ll build in a test using any, but like before, this code doesn’t evaluate properly

unsSub4 :: Num a => [a] -> [a] -> [a]
unsSub4 l1x l2x | (any (\x -> x /= 1) l1x) || (any (\y -> y /= 1) l2x) = []
unsSub4 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub4 (l1:l1x) (l2:l2x) = unsSub4 l1x l2x

The error once again complains of something to do with the elements a of the input arrays

Could not deduce (Eq a) arising from a use of ‘/=’
...
Possible fix:
        add (Eq a) to the context of
          the type signature for:
            unsSub4 :: forall a. Num a => [a] -> [a] -> [a]

Again, we’ll leave out a type declaration and see what Haskell thinks it is

:{
-- unsSub4 :: Num a => [a] -> [a] -> [a]
unsSub4 l1x l2x | (any (\x -> x /= 1) l1x) || (any (\y -> y /= 1) l2x) = []
unsSub4 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub4 (l1:l1x) (l2:l2x) = unsSub4 l1x l2x
:}

:t unsSub4

unsSub4 :: (Eq a, Num a) => [a] -> [a] -> [a]

Trying this

:{
unsSub4 :: (Eq a, Num a) => [a] -> [a] -> [a]
unsSub4 l1x l2x | (any (\x -> x /= 1) l1x) || (any (\y -> y /= 1) l2x) = []
unsSub4 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub4 (l1:l1x) (l2:l2x) = unsSub4 l1x l2x
:}

and it evaluates. What’s happening? As before, the input element a’s type must also be an instance of the Eq class, which means there has to be a way to equate any pair of a’s

:i Eq

type Eq :: * -> Constraint
class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool
  {-# MINIMAL (==) | (/=) #-}
  	-- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
instance (Eq a, Eq b) => Eq (Either a b)
  -- Defined in ‘Data.Either’
instance Eq a => Eq [a] -- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
instance Eq Word -- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
instance Eq Ordering -- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
instance Eq Int -- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
...

What :i or :info is saying about the typeclass Eq is that in order to be an instance of it, input a must have defined what happens when two of its members are subjected to an equality tests (==) and (/=).

Now unsSub4 :: (Eq a, Num a) => [a] -> [a] -> [a] restricts a to being a value that has instances for Eq and Num registered. Why is this important? Because without specifying, anticipating the ability to perform equality (Eq) comparisons on only numerical values (Num), other non-numerical values for a might give false output. When we declare the function unsSub4’s input and output types with unsSub4 :: (Eq a, Num a) => [a] -> [a] -> [a], we are guaranteeing sane behavior.

unsSub4 [1,2] [1,1,1,1,1,1]

[]

What will happen if we use lists of strings of 1?

unsSub4 ["1","1"] ["1","1","1","1"]

<interactive>:2516:1-35: error:
    • No instance for (Num [Char]) arising from a use of ‘unsSub4’
    • In the expression: unsSub4 ["1", "1"] ["1", "1", "1", "1"]
      In an equation for ‘it’:
          it = unsSub4 ["1", "1"] ["1", "1", "1", ....]

Again, Haskell is playing it safe. We haven’t made Haskell aware of any way to handle strings as list elements. We use (/=), which will work

'1' /= '2'

True

but we haven’t accounted for negate which wants to negate an actual number. Looking into negate’s type

:t negate

negate :: Num a => a -> a

we see it cannot handle anything but numbers registered with the typeclass Num. So yes, we can use string versions of 1, but that’s because there is a registered instance for Char which defines behind the scenes how to equate numbers

:i Eq

type Eq :: * -> Constraint
class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool
  {-# MINIMAL (==) | (/=) #-}
  	-- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
...
instance Eq Char -- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
...

As you saw in LYAHFGG, recursion is the Haskell way of looping. UNS addition, as represented by lists, will be a simple matter of combining two lists of 1’s into one total list. Borrowing from above, we can start out very simple by concatenating the lists

[1,1,1,1] ++ [1,1]

[1,1,1,1,1,1]

uns2 list1 list2 = list1 ++ list2

:{
unsAdd1 :: (Eq a, Num a) => [a] -> [a] -> [a]
unsAdd1 l1x l2x | (any (\x -> x /= 1) l1x) || (any (\y -> y /= 1) l2x) = []
unsAdd1 l1x l2x | null l1x = l2x
                | null l2x = l1x
unsAdd1 (l1:l1x) (l2:l2x) = l1 : l2 : unsAdd1 l1x l2x
:}

unsAdd1 [1,1] [1]

[1,1,1]

unsAdd1 gives a nice example of recursion. But what if any of the list elements are negative 1’s? Let’s say if the lists contain -1’s we’ll take away a positive 1. One approach would be to just concatenate both lists, then go through removing positive and negative pairs

:{
unsAdd2 :: (Eq a, Num a) => [a] -> [a] -> [a]
unsAdd2 l1x l2x | ((any (/=1) l1x) && (any (/=(-1)) l1x))
                  || ((any (/=1) l2x) && (any (/=(-1)) l2x)) = []
unsAdd2 l1x l2x | null l1x = l2x
                | null l2x = l1x
unsAdd2 (l1:l1x) (l2:l2x) = l1 : l2 : unsAdd2 l1x l2x
:}

unsAdd2 [1,1] [-1,-1,-1]

[1,-1,1,-1,-1]

Here’s a variant where the test for 1 and -1 is somewhat shorter building on this idea

all (`elem` [1,-1]) [1,1,1,-1,1,-1,-1]

True

:{
unsAdd3 l1x l2x | not (all (`elem` [1,-1]) l1x) && not (all (`elem` [1,-1]) l2x) = []
unsAdd3 l1x l2x | null l1x = l2x
                | null l2x = l1x
unsAdd3 (l1:l1x) (l2:l2x) = l1 : l2 : unsAdd3 l1x l2x
:}

unsAdd3 [1,1] [-1,-1,-1]

[1,-1,1,-1,-1]

One simple idea would be to use a fold, e.g.

foldr (\x acc -> x + acc) 0 [1,-1,1,1,1,-1,1]

3

foldr (\x acc -> x + acc) 0 [1,-1,1,-1,-1,-1,1]

-1

:{
unsAdd4 l1x l2x = let ux = l1x ++ l2x
                  in collps ux
                     where collps = foldr (\x acc -> x + acc) 0
:}

unsAdd4 [1,1,1,-1] [1,-1]

2

:{
unsAdd5 ux = let pux = filter (==1) ux
                 mux = filter (==(-1)) ux
             in pux ++ mux
:}

unsAdd5 [1,-1,1,1,-1,-1,1,-1,1,1,1,1]

[1,1,1,1,1,1,1,1,-1,-1,-1,-1]

The UNS is considered a bijective base-1 numeral system. How is bijective meant here? The answer is to imagine the set of all whole numerals \(1,2,\ldots,\infin\;\), and then the set of all UNS 1-strings, e.g., 1, 11, 111. These two sets are mapped bijectively, as with bijective functions. The term unary can be interpreted mainly as a number system having only one digit. However, when we explore Peano numbers, we will revisit the idea of unary functions and unary operators.

The built-in Haskell gcd was used to reduce the rational number, e.g., fraction, to its lowest terms.

𝖟𝕭. Find the lowest terms of \(42/56\)

gcd 42 56

14

i.e., \(14\) is the greatest common divisor of both \(42\) and \(56\)

\[ \frac{42}{56} \]

Euclid’s algorithm, is an efficient method for computing the greatest common divisor (GCD) of two integers (numbers), the largest number that divides them both without a remainder.

:{
eGCD :: Integral i => i -> i -> i
eGCD 0 b = b
eGCD a b = eGCD (b `mod` a) a
:}

eGCD 60 25

5

This code give the first four perfect numbers In number theory, a perfect number is a positive integer that is equal to the sum of its positive divisors, excluding the number itself. For instance, \(6\) has divisors \(1\), \(2\) and \(3\) (excluding itself), and \(1 + 2 + 3 = 6\;\), so \(6\) is a perfect number.

:{
main = do
  let n = 4
  mapM_ print $
    take n [candidate | candidate <- [2 .. 2 ^ 19], getSum candidate == 1 ]
    where
      getSum candidate =
        1 % candidate + sum [1 % factor + 1 % (candidate `div` factor)
                            | factor <- [2 .. floor (sqrt (fromIntegral candidate))]
                            , candidate `mod` factor == 0 ]
:}

main

6
28
496
8128