module Functions.Recursive where

open import Data.Bool using (Bool; true; false) open import Data.Nat using (ℕ; suc; zero)

Functions can be recursive as well, which is essential for working on sets that were defined recursively. In this case, a common approach is to define an alternative for each of the constructors and when the constructor is recursive then the function itself shall also be probably recursive.

`_+_`

: AdditionConsider the previous definition of the `ℕ`

type, where we had the following constructors with the following types:

`zero : ℕ`

`suc : ℕ → ℕ`

Note that this was done along the lines of the mathematical definition of the Peano arithmetic. Consider also the definion of how to calculate the sum of two natural numbers with this representation:

$\begin{array}{ccc}\hfill 0+n& \hfill =\hfill & n\hfill \\ \hfill (1+m)+n& \hfill =\hfill & 1+(m+n)\hfill \end{array}$

Now consider the same definition in Agda:

_+_ : ℕ → ℕ → ℕ zero + n = n suc m + n = suc (m + n) infixl 6 _+_

Define the following functions:

```
pred : ℕ → ℕ -- predecessor (pred 0 = 0)
infixl 6 _∸_
_∸_ : ℕ → ℕ → ℕ -- subtraction (0 ∸ n = n)
infixl 7 _*_
_*_ : ℕ → ℕ → ℕ -- multiplication
infixl 6 _⊔_
_⊔_ : ℕ → ℕ → ℕ -- maximum
infixl 7 _⊓_
_⊓_ : ℕ → ℕ → ℕ -- minimum
⌊_/2⌋ : ℕ → ℕ -- half (⌊ 1 /2⌋ = 0)
odd : ℕ → Bool -- is odd
even : ℕ → Bool -- is even
```

It is possible to define functions mutually, like we did for sets. As an example, consider the mutual definition of the `even`

and `odd`

functions:

```
odd : ℕ → Bool
even : ℕ → Bool
even zero = true
even (suc n) = odd n
odd zero = false
odd (suc n) = even n
```

Define the following functions mutually:

_≡?_ : ℕ → ℕ → Bool -- is equal _≤?_ : ℕ → ℕ → Bool -- is less than or equal

`ℕ`

Import the binary representation of natural numbers:

open import Sets.Recursive using (ℕ⁺; one; double; double+1; ℕ₂; zero; id)

Define a conversion function of the following type:

from : ℕ₂ → ℕ -- hint: use _*_

Note that the `from`

function shall define a reverse function of the following isomorphism between `ℕ`

and `ℕ₂`

(later we will prove that `from`

is an isomorphism):

ℕ |
ℕ₂ |
---|---|

`zero` |
`zero` |

`suc zero` |
`id one` |

`suc (suc zero)` |
`id (double one)` |

`suc (suc (suc zero))` |
`id (double+1 one)` |

... | ... |

Later we will see how to define the same conversion in the other direction.

Define `ℤ`

and some operations on it (such as `_+_`

, `_-_`

, `_*_`

).

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

Define (recursive) mirroring of binary trees, that is a function with the following type:

`mirror : BinTree → BinTree`