agda-stdlib
agda-stdlib copied to clipboard
agda
Misnomer: `Relation.Binary.Core.Total`
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.
Aren't they the same relation though? I do see this definition in other reference: https://ncatlab.org/nlab/show/total+relation
@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}
}
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.
@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”...)
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.
:+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!?
