module Functions.Recursive where

Import list

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.

_+_: Addition

Consider 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  _+_

Exercises

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

Mutual definitions

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

Exercises

Define the following functions mutually:

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

Binary representation of ℕ

Import the binary representation of natural numbers:

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

Exercise

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):

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

Exercises

Define ℤ and some operations on it (such as _+_, _-_, _*_).

Binary trees

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

Exercise

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

mirror : BinTree → BinTree