agda-stdlib

agda-stdlib copied to clipboard

Sorry if it's trivial but I can't wrap my head around at this moment. I don't see why StrictTotalOrder must be decidable, while TotalOrder itself does not have to be. I think the decidability must come from somewhere, either from strict order, or equivalence, but it's not immediate to me that any one of both can be decidable for sure. If it does not have to be, should we define a Dec variant for strict total order as well?

Don't worry, you're not the first to be tripped up by this. Decidability requires you to prove the negation in some circumstances. Totality doesn't give you anything about the negation and therefore Total does not imply Decidable. In contrast Trichotomous does provide negative information hence allowing you to prove Decidable.

In my opinion, the definition of Trichotomous is "too" strong and the three tri constructors shouldn't give you the negative statements, only the positive statements. This is a design feature (oversight?) dating back from the start of the library. Its so deeply embedded that changing it would break so much code that we're probably stuck with it....

One way to fix this without screwing over people too badly is to define WeakyTrichotomous without the negative proofs, and then rename the current StrictTotalOrder to DecStrictTotalOrder and insert a new record StrictTotalOrder in its place that uses WeaklyTrichotomous instead. Then people would only have to change StrictTotalOrder to DecStrictTotalOrder everywhere in their code.

No hang on. I'm talking nonsense. You could still derive Trichotomous from WeaklyTrichotmous, Irreflexive and Asymmetric. Discard everything I've said above! Hang on while I go back to the drawing board. In the meantime maybe someone whose more on it can explain.

can we define strict total order via total order over \x y -> x < y or x = y? is it weaker?

actually no. total order gets away with this merely because totality cannot decide equivalence, so the negative fragment is not decidable in general. in the case of strict total order, asymmetricity/irreflexivity are so strong that it gives witness to equivalence too. If the problem itself naturally induces decidability then there is probably no need to weaken it. Indeed it's sort of strange for the first glance, but i guess now I understand why it was designed in this way. probably worth document it in the code so that it explains the situation.

I thought about it. I think defining total order over \x y -> x < y -> \bot should produce an undecidable strict order. My intuition is by proving the negative portion of the relation, the computation content should be killed off by falsehood, and we will not be able to obtain x < y anymore, which makes the relation undecidable.

If it's indeed undecidable, we can probably add it for completeness. However, I'd imagine this is not quite helpful, so I guess it can be something like UndecStrictTotalOrder?

The construction \x y -> x < y -> \bot doesn't make much sense to me. It seems to say that the relation is empty. Is that really what you mean?

_≥_ : Rel Carrier _
x ≥ y = x < y → ⊥

this is what I meant. My point is (x < y → ⊥) ⊎ (y < x → ⊥) cannot distinguish x < y and x ≈ y, which I suppose makes the relation undecidable.

Can you give the full record definition for your undecidable strict total order?

Sure. I think IsStrictTotalOrder″ is undecidable in general, because there is just no law that is able to recover computational content to produce a witness of trichotomy.

open import Data.Sum
open import Relation.Nullary

record IsStrictTotalOrder′ {a ℓ₁ ℓ₂} {A : Set a}
                           (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
                           Set (a ⊔ ℓ₁ ⊔ ℓ₂) where

  _≤_ : Rel A _
  x ≤ y = Lift (ℓ₁ ⊔ ℓ₂) (x ≈ y) ⊎ Lift (ℓ₁ ⊔ ℓ₂) (x < y)
  field
    isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
    isTotalOrder         : IsTotalOrder _≈_ _≤_

  open IsTotalOrder isTotalOrder using (total)
  open IsStrictPartialOrder isStrictPartialOrder
  open IsEquivalence isEquivalence using () renaming (sym to ≈-sym)

  -- it's decidable, because asymmetry and irreflexivity are too strong.
  compare : Trichotomous _≈_ _<_
  compare x y with total x y
  compare x y | inj₁ (inj₁ (lift x≈y)) = tri≈ (irrefl x≈y) x≈y (irrefl (≈-sym x≈y))
  compare x y | inj₁ (inj₂ (lift x<y)) = tri< x<y (λ x≈y → irrefl x≈y x<y) (asym x<y)
  compare x y | inj₂ (inj₁ (lift y≈x)) = tri≈ (irrefl (≈-sym y≈x)) (≈-sym y≈x) (irrefl y≈x)
  compare x y | inj₂ (inj₂ (lift y<x)) = tri> (asym y<x) (λ x≈y → irrefl (≈-sym x≈y) y<x) y<x


record IsStrictTotalOrder″ {a ℓ₁ ℓ₂} {A : Set a}
                           (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
                           Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  _≤_ : Rel A ℓ₂
  x ≤ y = ¬ (y < x)
  
  field
    isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
    isTotalOrder         : IsTotalOrder _≈_ _≤_
  open IsTotalOrder isTotalOrder using (total)
  open IsStrictPartialOrder isStrictPartialOrder
  open IsEquivalence isEquivalence using () renaming (sym to ≈-sym)

  compare : Trichotomous _≈_ _<_
  compare x y with total x y
  compare x y | inj₁ y≮x = {!!} -- ???
  compare x y | inj₂ x≮y = {!!} -- ???

Hmm I think that this is probably being better off left as is as it'll greatly complicate things in people's minds, as the hierarchy will no longer be monotonically increasing. Unless you have a compelling use case?

To avoid future confusion, I'll a note to Relation.Binary explaining why StrictTotalOrder is Decidable.

Yeah I agree. It's observably useless definition. I think adding an explanation is enough.

The undecidable version of a strict total order is what is also known as linear order. It could be implemented as follows.

Split : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Split _<_ = ∀ {x y} z → x < y → x < z ⊎ z < y

Connected : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
Connected _≈_ _<_ = ∀ {x y} → ¬ x < y → ¬ y < x → x ≈ y

record IsLinearOrder {a ℓ₁ ℓ₂} {A : Set a}
                     (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
                     Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
    split : Split _<_
    connected : Connected _≈_ _<_

  open IsStrictPartialOrder isStrictPartialOrder public

This could be added without much trouble if one accepts that the naming of the irreflexive orders does not exactly mirror that of the reflexive orders (as StrictTotalOrder really should have Dec in its name). Since it is the undecidable variant, one can add IsStrictTotalOrder.isLinearOrder.

@HuStmpHrrr's suggestion leads to a more general construction, the complement of a binary relation, which is a relation itself:

∁ : ∀ {a b ℓ} {A : Set a} {B : Set b} → REL A B ℓ → REL A B ℓ
∁ _∼_ = λ x y → ¬ (x ∼ y)

As indicated on the nlab page above, one can then define the following conversions.

IsLinearOrder ≈ <      → IsPartialOrder ≈ (∁ <)
IsStrictTotalOrder ≈ < → IsDecTotalOrder ≈ (∁ <)
IsTotalOrder ≈ ≤       → IsStrictPartialOrder ≈ (∁ ≤)
IsDecTotalOrder ≈ ≤    → IsStrictTotalOrder ≈ (∁ ≤)

Thanks, will look into this when I have a bit more time.

Split is Cotransitive (modulo argument re-ordering). The proposed definition of Connected (bad clash with Connex?) is implied by, but weaker than, that of Tight.