Extremal Elements

The various extrema must participate in certain relationships predicted by order theory.

Absorption

Join  A  R  {x,(Meet  A  R  {x,y})}≅x\textbf{Join} \; A \; R \; \{ x, (\textbf{Meet} \; A \; R \; \{ x,y\})\} \cong x

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x,y: A {
      Equivalent[A,R,Join[A,R,x+Meet[A,R,x+y]],x]
    }
  }
} for 10 expect 0
Absorption

Join  A  R  {x,(Meet  A  R  {x,y})}≅x\textbf{Join} \; A \; R \; \{ x, (\textbf{Meet} \; A \; R \; \{ x,y\})\} \cong x

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x,y: A {
      Equivalent[A,R,Meet[A,R,x+Join[A,R,x+y]],x]
    }
  }
} for 10 expect 0
Join as Meet of Above

Join  A  R  S=Meet  A  R  (Above  A  R  S)\textbf{Join} \; A \; R \; S = \textbf{Meet} \; A \; R \; (\textbf{Above} \; A \; R \; S)

sig A { R: set A }

sig S in A {}

check {
  Join[A,R,S] = Meet[A,R,Above[A,R,S]]
} for 10 expect 0
Meet as Join of Below

Meet  A  R  S=Join  A  R  (Below  A  R  S)\textbf{Meet} \; A \; R \; S = \textbf{Join} \; A \; R \; (\textbf{Below} \; A \; R \; S)

sig A { R: set A }

sig S in A {}

check {
  Meet[A,R,S] = Join[A,R,Below[A,R,S]]
} for 10 expect 0
Join versus JoinExt

JoinExt  A  R  A  Y=Join  A  R  Y\textbf{JoinExt} \; A \; R\; A \; Y = \textbf{Join} \; A \; R \; Y

sig A { R: set A }

sig Y in A {}

check {
  { some Join[A,R,Y]
  } implies {
    JoinExt[A,R,A,Y] = Join[A,R,Y]
  }
} for 10 expect 0
Max versus Join

Greatest  A  R  Y  x≡x∈Y∧Join  A  R  Y  x\textbf{Greatest} \; A \; R \; Y \; x \equiv x \in Y \wedge \textbf{Join} \; A \; R \; Y \; x

sig A { R: set A }

sig Y in A {}

check {
  { some Greatest[A,R,Y]
  } implies {
    all x: A {
      Greatest[A,R,Y,x]
      iff
      x in Y and Join[A,R,Y,x]
    }
  }
} for 10 expect 0
Max vs JoinExt

Greatest  A  R  Y=JoinExt  A  R  Y  Y\textbf{Greatest} \; A \; R \; Y = \textbf{JoinExt} \; A \; R \; Y \; Y

sig A { R: set A }

sig Y in A {}

check {
  Greatest[A,R,Y] = JoinExt[A,R,Y,Y]
} for 10 expect 0
MeetExt versus Meet

MeetExt  A  R  A  Y=Meet  A  R  Y\textbf{MeetExt} \; A \; R\; A \; Y = \textbf{Meet} \; A \; R \; Y

sig A { R: set A }

sig Y {}

check {
  { some Meet[A,R,Y]
  } implies {
    MeetExt[A,R,A,Y] = Meet[A,R,Y]
  }
} for 10 expect 0
Min versus Meet

Least  A  R  Y  x≡x∈Y∧Meet  A  R  Y  x\textbf{Least} \; A \; R \; Y \; x \equiv x \in Y \wedge \textbf{Meet} \; A \; R \; Y \; x

sig A { R: set A }

sig Y in A {}

check {
  all x: A {
    Least[A,R,Y,x]
    iff
    x in Y and Meet[A,R,Y,x]
  }
} for 10 expect 0
Min versus MeetExt

Least  A  R  Y=MeetExt  A  R  Y  Y\textbf{Least} \; A \; R \; Y = \textbf{MeetExt} \; A \; R \; Y \; Y

sig A { R: set A }

sig Y in A {}

check {
  { some Least[A,R,Y]
  } implies {
    Least[A,R,Y] = MeetExt[A,R,Y,Y]
  }
} for 10 expect 0

Meet

Below  A  R  S  (Meet  A  R  S)\textbf{Below} \; A \; R \; S \; (\textbf{Meet} \; A \; R \; S)

Empty Range

Below  A  R  (Meet  A  R  ∅)  y\textbf{Below} \; A \; R \; (\textbf{Meet} \; A \; R \; \empty ) \; y

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all y: A {
      Below[A,R,Meet[A,R,none],y]
    }
  }
} for 10 expect 0
One-point

Meet  A  R  {x}≅x\textbf{Meet} \; A \; R \; \{x\} \cong x

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x: A {
      Equivalent[A,R,Meet[A,R,x],x]
    }
  }
} for 10 expect 0
Range Disjunction

Meet  A  R  (S∪T)≅Meet  A  R  (Meet  A  R  S,Meet  A  R  T)\textbf{Meet} \; A \; R \; (S \cup T) \cong \textbf{Meet} \; A \; R \; ({\textbf{Meet} \; A \; R \; S, \textbf{Meet} \; A \; R \; T})

sig A { R: set A }

sig S, T in A {}

check {
  { Preorder[A,R]
    some Meet[A,R,S+T]
    some Meet[A,R,S]
    some Meet[A,R,T]
  } implies {
    Equivalent[A,R,
      Meet[A,R,S+T],
      Meet[A,R,Meet[A,R,S]+Meet[A,R,T]]
    ]
  }
} for 10 expect 0

Alternatively:

sig A { R: set A }

sig S, T in A {}

check {
  { AllMeets[A,R]
  } implies {
    Equivalent[A,R,
      Meet[A,R,S+T],
      Meet[A,R,Meet[A,R,S]+Meet[A,R,T]]
    ]
  }
} for 10 expect 0

Binary Operator

Associativity

Meet  A  R  ({Meet  A  R  {x,y},z})=Meet  A  R  ({x,Meet  A  R  {y,z}})\textbf{Meet} \; A \; R \; (\{\textbf{Meet} \; A \; R \; \{ x,y \}, z \}) = \textbf{Meet} \; A \; R \; (\{ x,\textbf{Meet} \; A \; R \; \{ y, z \} \})

sig A { R: set A }

associativity: check {
  { AllMeets[A,R]
  } implies {
    all x,y,z: A {
      Meet[A,R,Meet[A,R,x+y]+z] = Meet[A,R,x+Meet[A,R,y+z]]
    }
  }
} for 10 expect 0
Correspondence

R.x.y≡x=Meet  A  R  {x,y}R.x.y \equiv x = \textbf{Meet} \; A \; R \; \{x, y \}

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x,y: A {
      x->y in R
      iff
      Meet[A,R,x+y,x]
    }
  }
} for 10 expect 0
Idempotence

Meet  A  R  {x,x}≅x\textbf{Meet} \; A \; R \; \{x, x\} \cong x

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x: A {
      Equivalent[A,R,Meet[A,R,x+x],x]
    }
  }
} for 10 expect 0
Symmetry

Meet  A  R  {x,y}=Meet  A  R  {y,x}\textbf{Meet} \; A \; R \; \{x, y\} = \textbf{Meet} \; A \; R \; \{y, x\}

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x,y: A {
      Meet[A,R,x+y] = Meet[A,R,y+x]
    }
  }
} for 10 expect 0

Join

Above  A  R  S  (Join  A  R  S)\textbf{Above} \; A \; R \; S \; (\textbf{Join} \; A \; R \; S)
sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    Above[A,R,S, Join[A,R,S]]
  }
} for 10 expect 0
Empty Range

Above  A  R  (Join  A  R  ∅)  y\textbf{Above} \; A \; R \; (\textbf{Join} \; A \; R \; \empty ) \; y

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all y: A {
      Above[A,R,Join[A,R,none],y]
    }
  }
} for 10 expect 0
One Point

Join  A  R  {x}≅x\textbf{Join} \; A \; R \; \{x\} \cong x

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x: A {
      Equivalent[A,R,Join[A,R,x],x]
    }
  }
} for 10 expect 0
Range Disjunction

Join  A  R  (S∪T)≅Join  A  R  (Join  A  R  S,Join  A  R  T)\textbf{Join} \; A \; R \; (S \cup T) \cong \textbf{Join} \; A \; R \; ({\textbf{Join} \; A \; R \; S, \textbf{Join} \; A \; R \; T})

sig A { R: set A }

sig S, T in A {}

check {
  { Preorder[A,R]
    some Join[A,R,S+T]
    some Join[A,R,S]
    some Join[A,R,T]
  } implies {
    Equivalent[A,R,
      Join[A,R,S+T],
      Join[A,R,Join[A,R,S]+Join[A,R,T]]
    ]
  }
} for 10 expect 0

Alternatively:

sig A { R: set A }

sig S, T in A {}

check {
  { AllJoins[A,R]
  } implies {
    Equivalent[A,R,
      Join[A,R,S+T],
      Join[A,R,Join[A,R,S]+Join[A,R,T]]
    ]
  }
} for 10 expect 0

Binary Operator

Associativity

Join  A  R  ({Join  A  R  {x,y},z})=Join  A  R  ({x,Join  A  R  {y,z}})\textbf{Join} \; A \; R \; (\{\textbf{Join} \; A \; R \; \{ x,y \}, z \}) = \textbf{Join} \; A \; R \; (\{ x,\textbf{Join} \; A \; R \; \{ y, z \} \})

sig A { R: set A }

associativity: check {
  { AllJoins[A,R]
  } implies {
    all x,y,z: A {
      Join[A,R,Join[A,R,x+y]+z] = Join[A,R,x+Join[A,R,y+z]]
    }
  }
} for 10 expect 0
Correspondence

R.x.y≡y=Join  A  R  {x,y}R.x.y \equiv y = \textbf{Join} \; A \; R \; \{x, y \}

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x,y: A {
      x->y in R
      iff
      Join[A,R,x+y,y]
    }
  }
} for 10 expect 0
Idempotence

Join  A  R  {x,x}≅x\textbf{Join} \; A \; R \; \{x, x\} \cong x

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x: A {
      Equivalent[A,R,Join[A,R,x+x],x]
    }
  }
} for 10 expect 0
Symmetry

Join  A  R  {x,y}=Join  A  R  {y,x}\textbf{Join} \; A \; R \; \{x, y\} = \textbf{Join} \; A \; R \; \{y, x\}

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x,y: A {
      Join[A,R,x+y] = Join[A,R,y+x]
    }
  }
} for 10 expect 0
PreviousBelowNextRelation Division

Last updated