Definition of DCPO

Stream: mathlib4

[Noam Zilberstein]

Hello! I have been looking at the CompletePartialOrder class in Mathlib, and I was a bit surprised that the definition of directed sets does not require non-emptiness. It is typical that a directed set must be nonempty (i.e. Def 2.1.8 of Abramsky and Jung https://www.cs.ox.ac.uk/files/298/handbook.pdf). The supremum of an empty set must be bottom, but some posets do not have a bottom, so CompletePartialOrder in Mathlib is more like a Pointed DCPO than a regular DCPO.

Does anyone know why it is like this? Would folks be open to changing the definition so that a directed set must be nonempty?

[Yaël Dillies]

This seems very reasonable to me. @Christopher Hoskin, thoughts?

[Noam Zilberstein]

Great, thanks for getting back to me. If others agree, then I can start putting together a PR

[Kevin Buzzard]

I am also surprised that the definition of directed set does not require nonemptiness! Isn't this a standard part of the definition? Where exactly are you seeing this in mathlib?

[Noam Zilberstein]

This is the file I was looking at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Directed.html

[Aaron Liu]

maybe we can add a Predirected which does not require nonemptiness

[Noam Zilberstein]

It would be nice too because if DirectedOn implies nonempty, then ScottContinuous would not need to require nonempty: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/ScottContinuity.html#ScottContinuous

[Kevin Buzzard]

Oh wow this is from forever ago. Although Wikipedia doesn't make it clear, directed sets should definitely be nonempty (the empty set needes an upper bound).

[Kevin Buzzard]

Although Wikipedia then goes on to claim that every totally ordered set is directed, which is a claim I am not entirely happy with because in my mental model of emptysetology totally ordered sets can definitely be empty!

[Kevin Buzzard]

The (incorrect-IMO) definition of directed goes back to the birth of mathlib3; the second commit by Mario titled "import content from lean/library/data and library_dev" added it into mathlib3/algebra/lattice/filter.lean (with the inequality the other way around; this was changed later on).

[Noam Zilberstein]

FWIW, I think that Abramsky & Jung 1994 is the most commonly accepted reference for directed sets, so I think it makes sense to follow their definitions

[Christopher Hoskin]

I would be happy for non-empty to be included in the definition of directed sets - I had to add d.Nonempty → all over the place for Scott Continuity which was rather clunky.

[Noam Zilberstein]

Thanks for the discussion everyone, I will work on drafting a PR to implement this change