Misnomer: `Relation.Binary.Core.Total`

[WolframKahl]

I find that the current Total for binary relations is a misnomer: Currently there is:

Total : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Total _∼_ = ∀ x y → (x ∼ y) ⊎ (y ∼ x)

But a binary relation R is normally called total iff Reflexive (R relCompose (converse R)), so ripping this name out of the context of a poor naming of linear orders is, in my opinion, very unfortunate.

[HuStmpHrrr]

Aren't they the same relation though? I do see this definition in other reference: https://ncatlab.org/nlab/show/total+relation

[WolframKahl]

@HuStmpHrrr , ncatlab is a somewhat surprising source for relation-algebraic terminology. A more common starting point, which I am also using in RATH-Agda, is the following textbook:

@Book{Schmidt-Stroehlein-1993,
  author = {Gunther Schmidt and Thomas Str{\"o}hlein},
  title = {Relations and Graphs, Discrete Mathematics for Computer Scientists},
  year = 1993,
  series = {EATCS-Mono\-graphs on Theoret.\null{} Comput.\null{} Sci.},
  publisher = Springer,
  DOI = {10.1007/978-3-642-77968-8},
  abstract = {Relational methods can be found at various places in
               computer science, notably in data base theory,
               relational semantics of concurrency, relational type
               theory, analysis of rewriting systems, and modern
               programming language design. In addition, they appear in
               algorithms analysis and in the bulk of discrete
               mathematics taught to computer scientists. This book
               devoted to the background of these methods. It is the
               first to explain how to use relational and graph-
               theoretic methods systematically in computer science.
               The powerful calculus of relation algebra is developed
               with respect to applications to a diverse range of
               problem areas. Results are first motivated by practical
               examples, often visualized by both Boolean 0-1-matrices
               and graphs, and then derived algebraically.}
  ISBN = {3-540-56254-0, 0-387-56254-0}
}

[MatthewDaggitt]

Hypothetically what would you suggest as a replacement name?

Unfortunately this can't be deprecated and is a reasonably large breaking change as it would require renaming the record field in TotalOrder.

[JacquesCarette]

Wikipedia uses connex for that particular relational property.

[WolframKahl]

@MatthewDaggitt, you could choose to not change that field name, arguing that some people use the name “total” for this property in the order context.

(However, I still much prefer “linear order” over “total order”, but I admit that “linear” does not stand alone much better than “total”...)

[gallais]

I don't know if Wikipedia got edited in the meantime or something but connex now makes the following distinction:

• connex: ∀ {x y} → x ≢ y → x ∼ y ⊎ y ∼ x
• strongly connex: ∀ {x y} → x ∼ y ⊎ y ∼ x

So _<_ would for instance be connex.

[MatthewDaggitt]

Marking this as something to address in v2.0

[jamesmckinna]

:+1: to Linear, as out of 900+ uses in the library, 800+ occur as instances of ...TotalOrder or ...TotalPreorder, in each of which 'linear' carries the 'usual' (first order model-theoretic, eg (D)LO) meaning. But that's a lot of knock-on viscosity ;-) Sigh.

Ob DenseLinearOrder: Dense isn't defined anywhere!?