From 85b191cd3134102c7205c1771806ee16f73b3a89 Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Sun, 7 Aug 2022 23:35:19 +0100 Subject: Write about equivalence relations --- doc/Tutorial.html | 43 +++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 41 insertions(+), 2 deletions(-) (limited to 'doc/Tutorial.html') diff --git a/doc/Tutorial.html b/doc/Tutorial.html index ae77959..5336f7a 100644 --- a/doc/Tutorial.html +++ b/doc/Tutorial.html @@ -44,5 +44,44 @@

  • constructing types with an equality relation that’s better behaved than Idris’s built-in Equal type.

  • types with an equality relation that carries additional information

    • -

    Basic interface

    -


    +

    If you want to see the source-code behind this tutorial, check the source-code out.

    +

    Equivalence relations

    +

    A relation over a type ty in Idris is any two-argument type-valued function:

    +
    namespace Control.Relation
+  Rel : Type -> Type
+  Rel ty = ty -> ty -> Type
    +

    This definition and its associated interfaces ship with idris’s standard library. Given a relation rel : Rel ty and x,y : ty, we can form x `rel` y : Type: the type of ways in which x and y can be related.

    +

    For example, two lists overlap when they have a common element: record Overlap {0 a : Type} (xs,ys : List a) where
      constructor Overlapping
      common : a
      lhsPos : common Elem xs
      rhsPos : common Elem ys

     Lists can overlap in exactly one position: Ex1 : Overlap [1,2,3] [6,7,2,8]
    Ex1 = Overlapping
      { common = 2
      , lhsPos = There Here
      , rhsPos = There (There Here)
      }
     But they can overlap in several ways: Ex2a ,
    Ex2b ,
    Ex2c : Overlap [1,2,3] [2,3,2]
    Ex2a = Overlapping
      { common = 3
      , lhsPos = There (There Here)
      , rhsPos = There Here
      }
    Ex2b = Overlapping
      { common = 2
      , lhsPos = There Here
      , rhsPos = Here
      }
    Ex2c = Overlapping
      { common = 2
      , lhsPos = There Here
      , rhsPos = There (There Here)
      }
     We can think of a relation rel : Rel ty as the type of edges in a directed graph between vertices in ty:

    + +

    An equivalence relation is a relation that’s:

    + +

    record Equivalence (A : Type) where
      constructor MkEquivalence
      0 relation: Rel A
      reflexive : (x       : A) -> relation x x
      symmetric : (x, y    : A) -> relation x y -> relation y x
      transitive: (x, y, z : A) -> relation x y -> relation y z
                                -> relation x z

    +

    We equip the built-in relation Equal with the structure of an equivalence relation, using the constructor Refl and the stdlib functions sym, and trans: EqualityEquivalence : Equivalence a
    EqualityEquivalence = MkEquivalence
      { relation = (===)
      , reflexive = </span>x => Refl
      , symmetric = </span>x,y,x_eq_y => sym x_eq_y
      , transitive = </span>x,y,z,x_eq_y,y_eq_z => trans x_eq_y y_eq_z
      }

    +

    We’ll use the following relation on pairs of natural numbers as a running example. We can represent an integer as the difference between a pair of natural numbers: infix 8 .-.

    record INT where
      constructor (.-.)
      pos, neg : Nat

    record SameDiff (x, y : INT) where
      constructor Check
      same : (x.pos + y.neg === y.pos + x.neg)
     The SameDiff x y relation is equivalent to mathematical equation that states that the difference between the positive and negative parts is identical:
    xpos − xneg = ypos − yneg
    But, unlike the last equation which requires us to define integers and subtraction, its equivalent (.same) is expressed using only addition, and so addition on Nat is enough.

    +

    The relation SameDiff is an equivalence relation. The proofs are straightforward, and a good opportunity to practice Idris’s equational reasoning combinators from Syntax.PreorderReasoning: SameDiffEquivalence : Equivalence INT
    SameDiffEquivalence = MkEquivalence
      { relation = SameDiff
      , reflexive = </span>x => Check $&nbsp;<span class="IdrisFunction">Calc</span>&nbsp;$
          |~ x.pos + x.neg
          ~~ x.pos + x.neg …(Refl)
     This equational proof represents the single-step equational proof:

    +

    "Calculate:

    +
      +
    1. xpos + xneg
      2. +
    2.  = xpos + xneg (by reflexivity)"
      3. +
    +

    The mnemonic behind the ASCII-art is that the first step in the proof starts with a logical-judgement symbol ⊢, each step continues with an equality sign =, and justified by a thought bubble (...).

    +

      , symmetric = </span>x,y,x_eq_y => Check $&nbsp;<span class="IdrisFunction">Calc</span>&nbsp;$
          |~ y.pos + x.neg
          ~~ x.pos + y.neg ..<(x_eq_y.same)
     In this proof, we were given the proof x_eq_y.same : x.pos + y.neg = y.pos + x.neg and so we appealed to the symmetric equation. The mnemonic here is that the last bubble in the thought bubble (...) is replace with a left-pointing arrow, reversing the reasoning step.   , transitive = </span>x,y,z,x_eq_y,y_eq_z => Check $&nbsp;<span class="IdrisFunction">plusRightCancel</span>&nbsp;<span class="IdrisKeyword">\_</span>&nbsp;<span class="IdrisKeyword">\_</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$ Calc $<br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">|~</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.neg</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span>&nbsp;<span class="IdrisData">3</span>&nbsp;<span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">{</span><span class="IdrisBound">a</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span>&nbsp;$
                                         (X 0 .+. X 1) .+. X 2
                                      =-= X 0 .+. (X 2 .+. X 1))
          ~~ x.pos + (z.pos + y.neg) …(cong (x.pos +) $&nbsp;<span class="IdrisBound">y\_eq\_z</span><span class="IdrisFunction">.same</span><span class="IdrisKeyword">)</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span>&nbsp;<span class="IdrisData">3</span>&nbsp;<span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">{</span><span class="IdrisBound">a</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span>&nbsp;$
                                         X 0 .+. (X 1 .+. X 2)
                                     =-= (X 0 .+. X 2) .+. X 1)
          ~~ (y.pos + x.neg) + z.pos …(cong (+ z.pos) ?h2)
          ~~ z.pos + x.neg + y.pos   …(solve 3 Monoid.Commutative.Free.Free
                                         {a = Nat.Additive} $
                                         (X 0 .+. X 1) .+. X 2
                                     =-= (X 2 .+. X 1) .+. X 0)
      }
     This proof is a lot more involved:

    +
      +
    1. We appeal to the cancellation property of addition: a + c = b + c ⇒ a = b
      2. +
    2. We rearrange the term, bringing the appropriate part of y into contact with the appropriate part of z and x to transform the term.
      3. +
    +

    Here we use the idris library Frex that can perform such routine rearrangements for common algebraic structures. In this case, we use the commutative monoid simplifier from Frex. If you want to read more about Frex, check the paper out.

    +

    Idris’s Control.Relation defines interfaces for properties like reflexivity and transitivity. While the setoid package doesn’t use them, we’ll use them in a few examples.

    +

    The Overlap relation from Examples 1 and 2 is symmetric: Symmetric (List a) Overlap where
      symmetric xs_overlaps_ys = Overlapping
        { common = xs_overlaps_ys.common
        , lhsPos = xs_overlaps_ys.rhsPos
        , rhsPos = xs_overlaps_ys.lhsPos
        }
     However, Overlap is neither reflexive nor transitive:

    + -- cgit v1.2.3