[BN] Some mathematical preliminaries: sets, relations and functions presents an inductive definition of the natural numbers. Implement this definition as a data type in some functional programming language (for instance Agda or Haskell).
[BN] Some mathematical preliminaries: sets, relations and functions also contains a function rec. Implement this function (for the definition of natural numbers from the previous exercise), and use it to give a non-recursive definition of addition, add : ℕ → ℕ → ℕ.
[BN] Define a function that appends two lists using the function listrec from Some mathematical preliminaries: sets, relations and functions.
[BN] There is an incorrect definition of the integers, ℤ, in Some mathematical preliminaries: sets, relations and functions. Explain why this definition is incorrect.
[BN] Implement addition in PRF.
[BN] Implement multiplication in PRF.
[BN] The injective function f : ℕ × ℕ → ℕ defined by f (m, n) = 2ᵐ3ⁿ was used to show that ℕ × ℕ is countable. Prove that this is a primitive recursive function.
[BN] Prove that the cartesian product of two countable sets is countable.
(Exercises marked with [BN] are based on exercises from a previous version of this course, given by Bengt Nordström.)