Contents Previous Next

• Relations
  • Types of relations
  • Nullary relations
  • Unary relations
  • Binary relations
    • Properties of binary relations

Relations

module Types.relations where

open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
open import Lang.dataStructures using (
  Bool; true; false;
  ⟂; ⊤; ℕ; List;
  one; two; three; four; five; six; seven; eight; nine; ten; zero; succ; _+_;
  _::_; [])
open import Types.functions using (_on_; flip)

Relations can be defined as properties that assign truth values to finite tuples of elements. In other words, a relation is a function that accepts a finite set of arguments to produce a truth value. A binary relation would output a truth value given two objects, similarly a unary relation would apply on a single object to output a truth value. This can be generalized to k-ary relations.

In type theory, since relations are also types and “truth values” of a proposition is replaced by existence or belonging to the universe of all types, one can think of relations as functions that take n-tuples as input and return some object of type Set1 - the set of all Sets.

Types of relations

Nullary relations

Nullary relations are functions that can take any object and return an empty set ∅:

infix 3 ¬_

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ P = P → ⟂

Unary relations

In logic, a predicate can essentially be defined as a function that returns a binary value - whether the proposition that the predicate represents is true or false. In type theory, however, we define predicate in a different way. A predicate for us is a function that exists (and hence, is true):

Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
Pred A ℓ = A → Set ℓ

Here, a predicate P : Pred A ℓ can be seen as a subset of A containing all the elements of A that satisfy property P.

Membership of objects of A in P can be defined as:

infix 4 _∈_ _∉_

_∈_ : ∀ {a ℓ} {A : Set a} → A → Pred A ℓ → Set _
x ∈ P = P x

_∉_ : ∀ {a ℓ} {A : Set a} → A → Pred A ℓ → Set _
x ∉ P = ¬ (x ∈ P)

The empty (or false) predicate becomes:

∅ : ∀ {a} {A : Set a} → Pred A lzero
∅ = λ _ → ⟂

The singleton predicate (constructor):

is_sameAs : ∀ {a} {A : Set a}
        → A
        → Pred A a
is x sameAs = x ≡_

equal? : is six sameAs (succ five)
equal? = refl

Binary relations

A heterogeneous binary relation is defined as:

REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ lsuc ℓ)
REL A B ℓ = A → B → Set ℓ

and a homogenous one as:

Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
Rel A ℓ = REL A A ℓ

Properties of binary relations

In type theory, an implication $ A ⟹ B $ is just a function type $ f: A → B $, and if f exists, the implication does too. We define implication between two relations in agda as:

_⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
        → REL A B ℓ₁
        → REL A B ℓ₂
        → Set _
P ⇒ Q = ∀ {i j} → P i j → Q i j

A function f : A → B is invariant to two homogenous relations Rel A ℓ₁ and Rel B ℓ₂ if $ ∀ x, y ∈ A _and f(x), f(y) ∈ B, f(Rel x y) ⟹ (Rel f(x) f(y)) $:

_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
          → Rel A ℓ₁
          → (A → B)
          → Rel B ℓ₂
          → Set _
P =[ f ]⇒ Q = P ⇒ (Q on f)

A function f preserves an underlying relation while operating on a datatype if:

_Preserves_⟶_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
        → (A → B)
        → Rel A ℓ₁
        → Rel B ℓ₂
        → Set _
f Preserves P ⟶ Q = P =[ f ]⇒ Q

Similarly, a binary operation _+_ preserves the underlying relation if:

_Preserves₂_⟶_⟶_ : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c}
        → (A → B → C)
        → Rel A ℓ₁
        → Rel B ℓ₂
        → Rel C ℓ₃
        → Set _
_+_ Preserves₂ P ⟶ Q ⟶ R = ∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)

Properties of binary relations:

Reflexive : ∀ {a ℓ} {A : Set a}
        → Rel A ℓ
        → Set _
Reflexive _∼_ = ∀ {x} → x ∼ x

Sym : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
        → REL A B ℓ₁
        → REL B A ℓ₂
        → Set _
Sym P Q = P ⇒ flip Q

Symmetric : ∀ {a ℓ} {A : Set a}
        → Rel A ℓ
        → Set _
Symmetric _∼_ = Sym _∼_ _∼_

Trans : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c}
        → REL A B ℓ₁
        → REL B C ℓ₂
        → REL A C ℓ₃
        → Set _
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k

Transitive : ∀ {a ℓ} {A : Set a}
        → Rel A ℓ
        → Set _
Transitive _∼_ = Trans _∼_ _∼_ _∼_

Equality