module Functions.Functions_vs_Sets where

open import Sets.Enumerated using (Bool; true; false)

Now, that we have seen sets and functions, it may make sense to compare them and discuss the observed differences.

Negation as a relation

Recall how the logical negation can be represented as a relation between values of the Bool and Bool sets:

data Not : Bool → Bool → Set where
  n₁ : Not true false
  n₂ : Not false true

Note that this will create four new sets of which two are non-empty.

Not a b is non-empty iff b is the negated value of a.

Negation as a function

Now consider the representation of the negation as a function:

not : Bool → Bool
not true  = false
not false = true

Relations vs. functions

Benefits of using relations:

• Less restrictions:

  • not all the cases should be covered (partial specification)
  • redundancy is allowed
  • general recursion is allowed
  • inconsistency is allowed (that is, an empty relation)

• Shorter definitions (the difference increases with complexity)

Benefits of using functions:

• More and better guarantees:

  • coverage check ensures that all cases are covered
  • reachability check excludes redundant cases
  • termination check ensures termination for recursion
  • inconsistency is excluded by construction

• Functions have computational content:

  • code generation is possible
  • shorter proofs (see later)

• Ease of use, cf. not (not a) and Not a b ∧ Not b c

Specification vs. implementation

• Relations are useful for describing the problem/question (that is, a specification).

• Functions are useful for describing the solution/answer (that is, an implementation).

Remarks:

• Implementations are connected to specifications by the type system (see later).

• Functions are also used in specifications due to their ease of use and because they can conveniently represent negation and universal quantification.

  • Just like in mathematics where definitions may rely on previously known theorems.

Functions with a Boolean value (predicates)

An A → B → C function corresponds to the specification A → B → C → Set according the previous remarks. That is, _≤?_ : ℕ → ℕ → Bool would correspond to ℕ → ℕ → Bool → Set, but actually it is easier to define Boolean-valued functions, so we have _≤_ : ℕ → ℕ → Set as specification.