# [Solutions to Exercises] “Creating the Natural Numbers from First Principles”

In the article “Creating the Natural Numbers from First Principles” I provided some exercises at the end. If these exercises were easy for you, skip down to the solution of the bonus where I outline an interesting construction and provide more exercises for even deeper exploration.

1.) We need to implement exponentiation for `Nat`

. Switching on `a`

and `b`

we have:

```
func exp(_ a: Nat, _ b: Nat) -> Nat {
switch (a, b) {
case (.Succ, .Zero):
???
case (.Zero, .Succ):
???
case (.Succ, .Succ):
???
case (.Zero, .Zero):
???
}
}
```

The first case is asking for the value of `a^0`

. A positive integer raised to the zeroth power is just `1`

. The next case is asking for `0^b`

, which clearly is `0`

. We can fill in those cases now:

```
func exp(_ a: Nat, _ b: Nat) -> Nat {
switch (a, b) {
case (.Succ, .Zero):
return .Succ(.Zero)
case (.Zero, .Succ):
return .Zero
case (.Succ, .Succ):
???
case (.Zero, .Zero):
???
}
}
```

Next we need `a^b`

where we know `a`

and `b`

are positive natual numbers. We can reduce this to our base cases by observing that `a^b = a^(b-1) * a`

:

```
func exp(_ a: Nat, _ b: Nat) -> Nat {
switch (a, b) {
case (.Succ, .Zero):
return .Succ(.Zero)
case (.Zero, .Succ):
return .Zero
case let (.Succ, .Succ(pred_b)):
return exp(a, pred_b * a
case (.Zero, .Zero):
???
}
}
```

Now, this last case: `0^0`

. In math this is left as an undefined value, so technically we should probably throw a `fatalError`

or something. But, the standard library math function evaluates `pow(0.0, 0.0)`

to be `1.0`

, so we’ll adopt that. The final function is:

```
func exp(_ a: Nat, _ b: Nat) -> Nat {
switch (a, b) {
case (_, .Zero):
return .Succ(.Zero)
case (.Zero, .Succ):
return .Zero
case let (.Succ, .Succ(pred_b)):
return exp(a, pred_b * a
}
}
```

2.) Next we make `Nat`

implement the `Comparable`

protocol:

```
extension Nat : Comparable {}
func < (a: Nat, b: Nat) -> Bool {
switch (a, b) {
case (.Zero, .Zero):
???
case (.Succ, .Zero):
???
case (.Zero, .Succ):
???
case (.Succ, .Succ):
???
}
}
```

The first three of these cases are obvious: `Zero`

is less than every natural number except for itself.

```
extension Nat : Comparable {}
func < (a: Nat, b: Nat) -> Bool {
switch (a, b) {
case (.Zero, .Succ):
return true
case (_, .Zero):
return false
case (.Succ, .Succ):
???
}
}
```

The last case is done recursively using the predecessors of `a`

and `b`

and the fact that `a < b`

if and only if `a-1 < b-1`

:

```
extension Nat : Comparable {}
func < (a: Nat, b: Nat) -> Bool {
switch (a, b) {
case (.Zero, .Succ):
return true
case (_, .Zero):
return false
case let (.Succ(pred_a), .Succ(pred_b)):
return pred_a < pred_b
}
}
```

3.) This question was to define `min`

and `max`

for `Nat`

, but really we get that for free by adopting the `Comparable`

protocol. I didn’t really think this one through :/

4.) Now we want to implement the distance function:

```
func distance(_ a: Nat, _ b: Nat) -> Nat {
???
}
```

This should return the absolute value of the difference between `a`

and `b`

. Our base cases are derived from the fact that `distance(n, .Zero) == distance(.Zero, n) == n`

:

```
func distance(_ a: Nat, _ b: Nat) -> Nat {
switch (a, b) {
case (.Zero, _):
return b
case (_, .Zero):
return a
case (.Succ, .Succ)
???
}
}
```

Now the last case can reduce `a`

and `b`

so that we get closer to the base case:

```
func distance(_ a: Nat, _ b: Nat) -> Nat {
switch (a, b) {
case (.Zero, .Zero):
return .Zero
case (.Zero, .Succ):
return b
case (.Succ, .Zero):
return a
case let (.Succ(pred_a), .Succ(pred_b)):
return distance(pred_a, pred_b
}
}
```

I explicity put every case instead of wildcards because the Swift compiler didn’t think I was being exhaustive in my case statements for some reason.

5.) Using the `distance`

function from above we can write this quite easily:

```
func modulus(_ a: Nat, _ m: Nat) -> Nat {
if a < m {
return a
}
return modulus(distance(a, m), m)
}
modulus(five, two) == one
modulus(.Succ(five), two) == .Zero
```

Notice that `distance`

is simulating subtraction in `Nat`

.

6.) This function is quite simple to implement:

```
func pred(_ n: Nat) -> Nat? {
switch n {
case .Zero:
return nil
case let .Succ(pred):
return pred
}
}
pred(two) == one
pred(.Zero) == nil
```

7.) Implementing the `IntegerLiteralConvertible`

involves filling in this function:

```
extension Nat : IntegerLiteralConvertible {
init(integerLiteral value: IntegerLiteralType) {
self = ???
}
}
```

Now, every function we wrote involving `Nat`

was recursive, and that’s due to the inductive nature of `Nat`

. Unfortunately we cannot inmplement `init`

using recursion. So, we will need to define a helper function:

```
extension Nat : IntegerLiteralConvertible {
init(integerLiteral value: IntegerLiteralType) {
self = Nat.fromInt(value)
}
static func fromInt (n: Int, accum: Nat = .Zero) -> Nat {
if n == 0 {
return accum
}
return Nat.fromInt(n-1, accum: .Succ(accum))
}
}
let six: Nat = 6 // true
six == .Succ(five) // true
let seven = Nat.Succ(6) // true
seven == six + 1 // true
```

8.) This will be a topic of a future post where we will discuss a very general construction for turning any commutative monoid into an abelian group. In a very precise sense, this is the most universal and “correct” way of constructing the integers from the natural numbers.

However, only using what we know from the previous article we can construct the integers in a less general manner. An integer is either a natural number, or the negative of a natural number. This perfectly translates into an enum in Swift:

```
enum Z {
case Neg(Nat)
case Pos(Nat)
}
```

I’m using `Z`

for this type because that is what is used in mathematics (for the German word *Zahlen*, and the symbol used is \(\mathbb Z\)).

To make this type resemble the integers we should define addition, multiplication, equality, et cetera. Some of that would look like this:

```
func + (a: Z, b: Z) -> Z {
switch (a, b) {
case let (.Neg(a), .Neg(b)):
return .Neg(a + b)
case let (.Pos(a), .Pos(b)):
return .Pos(a + b)
case let (.Pos(a), .Neg(b)):
return a > b ? .Pos(distance(a, b)) : .Neg(distance(a, b))
case let (.Neg(a), .Pos(b)):
return a < b ? .Pos(distance(a, b)) : .Neg(distance(a, b))
}
}
func * (a: Z, b: Z) -> Z {
switch (a, b) {
case let (.Neg(a), .Neg(b)):
return .Pos(a * b)
case let (.Pos(a), .Pos(b)):
return .Pos(a * b)
case let (.Pos(a), .Neg(b)):
return .Neg(a * b)
case let (.Neg(a), .Pos(b)):
return .Neg(a * b)
}
}
extension Z : Equatable {}
func == (a: Z, b: Z) -> Bool {
switch (a, b) {
case let (.Neg(a), .Neg(b)):
return a == b
case let (.Pos(a), .Pos(b)):
return a == b
case let (.Pos(a), .Neg(b)):
return a == .Zero && b == .Zero
case let (.Neg(a), .Pos(b)):
return a == .Zero && b == .Zero
}
}
```

We can now construct some integers and perform some arithmetic on them:

```
let pos_two = Z.Pos(two)
let neg_two = Z.Neg(two)
let pos_four = Z.Pos(four)
let neg_four = Z.Neg(four)
neg_two * neg_two == pos_two + pos_two
pos_two * neg_two == neg_four
```

Now, we have indeed constructed the integers from the natural numbers `Nat`

, but there is something not quite right about this solution. In the definition of `+`

we had to use the fact that `Nat`

is comparable. Otherwise, the definition of `Z`

depended on only the abstract properties of `Nat`

.

Turns out, there is a very general construction that can be used to make `Z`

out of `Nat`

, but it also works in many other situations. Even better, in a very precise since, it is the most universal way of constructing `Z`

out of `Nat`

. This will be the topic of a future post after the necessary concepts have been developed. This object is known as the “Grothendieck group”, and it constructs an abelian group from a commutative monoid.

I leave it as an exercise to develop the rest of the integer theory, in particular:

- Make
`Z`

implement`Comparable`

. - Define the predecessor function
`pred (Z) -> Z`

(no longer need the optional return type). - Define the absolute value function:
`abs (Z) -> Nat`

. - Define subtraction
`- (Z, Z) -> Z`

. - Define exponentiation
`exp (Z, Nat) -> Z`

. Note that the power is`Nat`

because if one uses negative exponents one needs fractions. **Bonus**: Can you construct the rational numbers (fractions`a/b`

) from`Z`

?