Where should (Semi)Lattices be?

[HuStmpHrrr]

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]

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

[HuStmpHrrr]

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]

@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]

@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]

@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]

@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]

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]

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]

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]

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.