Contents Previous Next


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 __ __ __