search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
562 stars 234 forks source link

Where should (Semi)Lattices be? #439

Open HuStmpHrrr opened 5 years ago

HuStmpHrrr commented 5 years ago

There are a few implementations of semilattices/lattices:

https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Structures.agda#L410 https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/Lattice.agda

The ones implemented in Relation.Binary.* are more general, and one can show that the Relation.Binary.Lattice induces ones from Algebra.Structures. However, I do not understand why semilattices/lattices are defined in Relation.Binary? I tend to understand them to be abstract algebras, but with order theoretic settings. Shall we move them to Algebra? Since order theory is rich, we can probably put them in Algebra.OrderTheory.*. What do you think?

JacquesCarette commented 5 years ago

I agree that Algebra.OrderTheory.* would be better than Relation.Binary.Lattice.

HuStmpHrrr commented 5 years ago

So I guess the next question is where should the ones from Alegbra.Structures go if we decide to move the definitions to Algebra.OrderTheory?

WolframKahl commented 5 years ago

@JacquesCarette, partial orders are relational structures, and as such not algebras.

@HuStmpHrrr, the binary-suprema-and-infima characterisation of lattices as special partial orders is (in general) actually equivalent to the algebraic definition.

@JacquesCarette, but it is not of algebraic nature, so Algebra.OrderTheory sounds wrong.

Just OrderTheory.*? Or even just Order.*?

HuStmpHrrr commented 5 years ago

@WolframKahl Is algebra necessarily equational? I am getting confused. The version of Heyting algebra I learned is directly defined over preorder/partial order, and equivalence is not mentioned. From there I do think lattice theory on partial order is an algebra.

In my understanding, algebra cares whatever binary relation, and studies interaction between this relation and various operations on a given structured set. Typical abstract algebras are based on equivalence, which is also a binary relation. I don't understand why the situation is different for preorder/partial order.

WolframKahl commented 5 years ago

@HuStmpHrrr , an algebraic theory is a theory over a predicate logic language that has only function symbols, but no predicate symbols (except equality, which is then frequently considered as a logical symbol). Orderings are predicates.

HuStmpHrrr commented 5 years ago

@WolframKahl thanks. understood. indeed in that sense order theory is out of algebraic theories. Do you think it's better to leave them as relation, or put them in Order.*? I still find surprising to see lattices as binary relation.

MatthewDaggitt commented 5 years ago

Hmm my opinion (an admittedly fairly uninformed one!) is that lattices are algebras as they have operators. I'd also vote for Algebra.OrderTheory.* over OrderTheory.* or Order.* because both of the latter sound like they do actually belong in Relation.Binary.

WolframKahl commented 5 years ago

Lattices defined via two associative, commutative and idempotent operators satisfying the (equational) absorption laws are algebras.

Lattices defined as partial orders where binary suprema and infima exist (via quantified predicate logic formulae) are not algebras.

HuStmpHrrr commented 5 years ago

I want to add a few more points on why I think these theories should at least be pulled out Relation.Binary.*:

  1. These theories all contain an equivalence, so they possess algebras. For example, infimum and supremum are commutative band, and idempotent commutative monoid if they have bounds. However, I am not sure in which way I am supposed to claim that these semilattices have algebraic structures, because these structures should not reside in Relation.Binary.* already.

  2. defining distributive lattice over order theoretic lattice makes use of equivalence reasoning, which makes me feel even stronger that it does not belong to Relation.Binary.*. Defining morphisms will make the strange feeling stronger.

  3. There is a huge intersection between algebraic definitions and order theoretic ones. In my opinion, we should probably formalize them using order theory, and just induce corresponding algebraic structures.

Regarding the topic of algebraic theories, one thing I cannot wrap my head around with, is why Heyting algebra and Boolean algebra are algebras? Especially HA, I often see exponential is defined via order theory and the definition itself is also very elegant. Is that a historical abuse of terminology?

JacquesCarette commented 5 years ago

Sorry to get back to this late. So @WolframKahl is correct that the traditional view is that lattices defined as partial orders is not considered 'algebraic' -- basically because the models do not form a variety but a quasi-variety.

But I've been taking a 'generalized algebraic theory' view on these things (i.e. a la Cartmell), which doesn't worry about these model-theoretic considerations. The kinds of "universal algebra" operations that you can still do on these remains large.

Be that as it may, the layout of a library should be greatly influenced by 'findability'. Burying them in Relation.Binary certainly does not help with findability.

I guess OrderTheory is not too unreasonable.

JacquesCarette commented 5 years ago

@HuStmpHrrr A Boolean Algebra is an Algebra because they have a presentation which is purely algebraic. There are other modes of presentation which are indeed more order-theoretic.

Interestingly, I cannot recall a purely algebraic definition for Heyting "algebras"!

This is not entirely surprising. Mathematics severely abuses the word 'algebra'. The fact that in some instances, it can be made formal at all, is the more surprising thing!

MatthewDaggitt commented 5 years ago

Removing this from the v1.0 milestone, as this doesn't feel like a pressing issue.