# Import List

```
module Sets.Recursive where

open import Data.Bool using (Bool; true; false)```

The effect of this `open import` declaration is the same as if we copied the definition of the `Bool` type here. Note that we enumerated the constructors of `Bool` too.

More about import declarations will come later.

# Peano representation

We are looking for a representation for the natural numbers. The simplest choice is the Peano representation which corresponds to the unary numeral system:

term interpretation in decimal form
`zero` 0
`suc zero` 1
`suc (suc zero)` 2
`suc (suc (suc zero))` 3
... ...

# Definition of `ℕ`

In Agda, the definition of natural numbers is as follows.

```
data ℕ : Set where
zero :     ℕ
suc  : ℕ → ℕ```

Note that this definition yields the infinite set of judgements.

``````ℕ : Set
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ
suc (suc (suc zero)) : ℕ
...``````

# Type checking of expressions

With the Emacs command C-`c` C-`d`, one can get Agda to type check a given expression (`d` stands for 'deduce').

Example: Hit C-`c` C-`d` and enter `suc (suc zero)`.

## Exercises

Deduce the type of the following expressions with Agda:

• `suc zero`
• `suc (zero)`
• `(suc) zero`
• `zero suc`
• `(suc suc) zero`
• `suc`

# Binary representation of `ℕ`

Consider the following definition of positive natural numbers, labelled as ℕ⁺:

```
data ℕ⁺ : Set where
one      :      ℕ⁺
double   : ℕ⁺ → ℕ⁺
double+1 : ℕ⁺ → ℕ⁺```

Note that this definition above yields the following judgements (without ordering):

``````ℕ⁺ : Set
one : ℕ⁺
double one : ℕ⁺
double+1 one : ℕ⁺
double (double one) : ℕ⁺
double+1 (double one) : ℕ⁺
double (double+1 one) : ℕ⁺
double+1 (double+1 one) : ℕ⁺
double (double (double one)) : ℕ⁺
...``````

And

```
data ℕ₂ : Set where
zero :      ℕ₂
id   : ℕ⁺ → ℕ₂```

yields

``````ℕ₂ : Set
zero : ℕ₂
id one : ℕ₂
id (double one) : ℕ₂
id (double+1 one) : ℕ₂
id (double (double one)) : ℕ₂
id (double+1 (double one)) : ℕ₂
...``````

Soon we will prove in Agda that `ℕ` and `ℕ₂` are isomorphic with the following relation:

ℕ₂
`zero` `zero`
`suc zero` `id one`
`suc (suc zero)` `id (double one)`
`suc (suc (suc zero))` `id (double+1 one)`
... ...

## Exercises

1. How 9 is represented in `ℕ₂`? Type check that expression.

2. Why did not we simply use one `data` definition with 4 constructors, such as `zero`, `one`, `double`, and `double+1`?

# Rationale behind different representations

Each representation has its merit.

## Exercise

Determine which representation (`ℕ` or `ℕ₂`) is better for the following tasks.

• Compute `n * 2`.
• Compute `⌊n / 2⌋`.
• Decide whether the number is odd.
• Compute `n + m`.
• Compute `n * m`.
• Prove that `n + m` = `m + n` for all `m` and `n`.
• Store a number.

A good strategy is to choose the right representation for each task and convert values between different representations.

## Exercise

Define `ℤ`.

(Several solutions are possible.)

# Binary trees

```
data BinTree : Set where
leaf : BinTree
node : BinTree → BinTree → BinTree```

yields

``````BinTree : Set
leaf : BinTree
node leaf leaf : BinTree
node (node leaf leaf) leaf : BinTree
node leaf (node leaf leaf) : BinTree
node (node leaf leaf) (node leaf leaf) : BinTree
...``````

`BinTree` elements are good for representing binary trees (just the shapes without data).

## Exercise

Define binary trees according to the following shapes. Binary tree shapes

## Exercises

1. Define binary trees
• with natural number data attached to the leafs
• with natural number data attached to the nodes
• with Booleans in the nodes and natural numbers in the leafs
2. Define the lists (finite sequences) of natural numbers.

3. Define the non-empty lists of natural numbers.