[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.
The disjoint union A ⊎ B of two sets A and B can be defined inductively in the following way: If x ∈ A, then inl x ∈ A ⊎ B, and if y ∈ B, then inr y ∈ A ⊎ B.
Give a higher-order function corresponding to the primitive recursion scheme for disjoint unions, and state the structural induction principle.
[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.
(Exercises marked with [BN] are based on exercises from a previous version of this course, given by Bengt Nordström.)