Clean up basic order theory definitions

[jmougeot]

Was working with @TOTBWF to port over some domain theory from the 1lab, and noticed that the definitions of joins/meets in preorders are a bit all over the place both in terms of naming and semantics.

• What is typically called a top element is referred to as a Maximum; likewise for bottom elements and Minimum.
• Similarly, the definitions of Suprema and Infinima are defined in terms of binary operators that assign pairs of elements to a binary join/meet: this makes it impossible to say that a particular element is an join/meet of two elements. Also, these are defined under Relation.Binary.Lattice.Definitions.
• There are no definitions for joins/meets of families (that we are aware of!)

I suggest that we perform the following rationalisation:

1. Deprecate Maximum and Minimum in favor of IsTop and IsBottom
2. Deprecate Supremum and Infininum in favor of IsBinaryJoin and IsBinaryMeet in Relation.Binary.Definitions, which both state that a particular element is a binary meet/join of a pair of elements.
3. Add IsJoin and IsMeet to Relation.Binary.Definitions, which express that a particular element is a meet/join of a family.
4. Provided bundled versions of all the above.

I'm open to alternative names and locations. Note that this would be a breaking change, so we would have to take the necessary steps towards deprecation.

[jamesmckinna]

Nice issue to raise... the challenge/paradox of making naming choices in a 'standard' library:

• what may be "typically" called one thing (eg 'top') in one area of mathematics (eg. domain theory) may be called something else (eg. 'maximum') in another area (even a cognate one, eg. general theory of ordered structures)
• choosing one over another privileges the choice, and may (or may not!) fit badly with any particular user's preferred choice of terms-of-art (I'm not even going to get into issues around varieties of English as contemporary lingua franca for mathematics, compared to... earlier historical choices)
• but/when/if it's necessary to choose, one should be conscious of the choice, and of the distinguished gloss that places on certain names/symbols, and accept that you can't please everyone all the time.

Here, domain theory is being taken as the dominant/prevailing discourse (presumably, because Agda is often seen as a language/metalanguage for the metatheory of programming languages and their semantics, but I think we are all infinitely worse off for taking that as its distinguished mode-of-use, despite whatever I may have written making such a choice), and with that a particular set of name choices which break with the existing library.

I would like to enter a counter argument, that we do not make such changes, but rather that for preorders-which-are-(pre)domains, as a distinguished mode-of-use, that we take greater care with renaming directives, and even syntax declarations, to introduce 'appropriate' synonyms/symbology to reflect such modes of use. Historically, we don''t seem to have been very subtle, or fine-grained, about such practice(s), but an issue like this is a good opportunity to debate them...?

For example: I conjecture that we speak of 'top' and 'bottom' much more since LaTeX, as names for the macros \top and \bot which define the symbols ⊤ and ⊥, which themselves only really came into common currency since Scott/Plotkin and co. (Moreover, NB, ⊤ almost never since complete lattices qua domains gave way to structures with 'weaker' properties).

So: why not instead use the symbols as syntax for their order-theoretic names, and Top and Bot for the definitions which anchor such syntax, so that non-domain-theoretic usages can be kept 'standardised apart'. I realise that won't perhaps be a popular suggestion, nor in the minds of others necessarily a defensible one. It would, moreover, require perhaps a great deal (unacceptably so?) more discipline in namespace management/use of qualified names, in order to keep everything in order (sic), but I think it's worth paying that price.

So far, I've only addressed the naming of definitions part, rather than the properties vs. definitions aspects, which make good points, that equally well could operate mutatis mutandis in terms of IsMaximum etc. and are, I think, worth doing.

But I thought I should at least, in the first instance, challenge the (implied) certainty of the OP as to the 'rightness' of the proposed choices.

[TOTBWF]

Completely agree that naming is hard! I am not aware of any area of computer science/mathematics where bottom and top elements are called minimum and maximum elements though. The terms "maximal" and "minimal" elements are in common use, but these are distinct notions. The terms "greatest element" and "least element" are occasionally used in older texts (EG: Birkhoff 1940) but have fallen out of popularity even in general order theory.

With that in mind, it seems like we should use the standard order-theoretic names. This isn't just a philosophical question: these names pose a real discoverability problem. We had to spend quite a while poking through the library to find them! Some renaming shims /could/ help this a bit, but would lead to a fragmentation of lemma/definition names. I'm not sure it would be worth maintaining two separate sets of names if one of them is non-standard.

[JacquesCarette]

Another way to put it: if someone is arguing for Maximum and Minimum as being the "right" choices, backing that up with some references where those are the 'standard' names would be quite useful.

If the argument is instead that the current literature is broken and that Maximum and Minimum are the names that we should force upon the community, because we're being brave / forward looking / (something else), then that would also be nice to know.

The current names seem to originate from @MatthewDaggitt (or so says 'git blame') so perhaps he can enlighten us on the rationale for the choices?

[JacquesCarette]

I will note that PR #243 from stdlib 0.16 moved these around. From what I can tell, these definitions pre-date stdlib being on github!

[jamesmckinna]

NB. I'm not intending to die on the hill of Minimum and Maximum (thanks for the schooling in order theoretic terminology), but I am willing to insist on:

• being as conservative/non-breaking as we can be in any change, and it seems as though there's a clear separation available here between non-breaking additions, and breaking name changes (though they probably could be handled more deftly via deprecation? I haven't checked)
• not letting the domain theory tail wag the order theory dog in terms of fixing names/notation; it's a distinguished mode of use, and if its vocabulary is more specialised, then make appropriate additions to reflect that

To the first point: there are eg some very old usages come from @nad who maintains a lot of legacy code for both teaching and research. I've no wish to force breakages on those if I/we can help it. More generally, the current names do seem to enjoy currency with out Swedish colleagues, so there may be other reasons for what might seem 'occult' usage to Anglophones...

To the second: a recent, cognate example, is my deprecation of the use of 'minus' to notate the quasigroup _\\_ operation on (Is)Group, introduced solely for the sake of then inheriting it in AbelianGroup (where of course it makes sense). The distinct mode-of-use in the commutative case being over-generalised for the non-commutative, in a way which seems mathematically just ... wrong.

The other parts of the issue definitely do make sense, distinguishing the property (and its unique-up-to-ness) from the operator symbol, but in the type theoretic context, I think it's worth having both (I could do first-order model theory with only a relational language and no functions symbols, but why, in practice?). So I don't think it's a case of 'function symbols bad; must be replaced only with universal property' as 1-4 above seem to suggest. I think we should have both, and with such, a raft of further choices as to what is reified as a manifest field of a structure, under *.Structures, and what a lemma under *.Properties.

The more nuanced among us might comment on categories having limits vs. categories with assigned choices of limits, and the various preservation properties of such under (pseudo-)functors of various kinds, but I think that the use of type theory as a metalanguage inclines towards the latter rather than the former in its theory of representation. And certainly stdlib to date has reflected that (eg we don't define (Is)Group via the existence of an inverse, and then its uniqueness as such in possessing the IsInverse property... is that really what we want?).

It may very well be that 1lab makes different choices/is organised on a different conceptual basis... but as with agda-categories never-yet landing in stdlib... but if we are proposing to refound the library on new lines, then this deserves more discussion than piecemeal via individual issues/PRs?

[nad]

To the first point: there are eg some very old usages come from @nad who maintains a lot of legacy code for both teaching and research. I've no wish to force breakages on those if I/we can help it.

The module Relation.Binary.Lattice was added as late as 2016, so I don't think you need to worry about my code.

[TOTBWF]

For the "chosen join" vs. "is join" I completely agree that you want both.

As for a less piecemeal discussion, where would be the best venue for that?

[jamesmckinna]

Ach! (re: where to discuss the "future directions" for the library)
We don't have one, though Jacques has attempted several times to mobilise/motivate us to discuss this on the wiki, here but no real pick up on that (yet), so a thread on the Agda Zulip #stdlib channel might also be appropriate (with potentially a wider franchise for 'controversial' decisions?)