Monoid and Partial Monoid

[eupp]

This PR features the monoid and partial monoid structures (the latter inherits from the former). The partial monoid is intended to be a base class for synchronization algebra later #59. Partiality is encoded using the binary orthogonality relation (see [1] for details).

Why did we decide to invent the wheel here? Below are alternative formalizations of monoids and the reasons why we abandoned them.

1. mathcomp
   Here the monoids are used primarily in the context of so-called big operations. The canonical instances are linked to operations themselves rather than to types. We decided that for our use cases, it makes more sense to attach the instance to the type.

2. relation-algebra
   Relation-Algebra has a very heavyweight notion of "monoid". First, it uses its own tricks to pack several operations into one structure and then enable/disable modularly (see this file). This design has some advantages but overall it seems too complex for our needs. Also, relation-algebra has heterogeneous typed monoids, which is also an overkill for us.

3. fcsl-pcm
   In fcsl-pcm package, the PCMs (partial commutative monoids) are at the top of the hierarchy. We don't want to enforce commutativity for our synchronization algebras. Besides that, we've decided to try out the alternative encoding of partiality through the orthogonality relation, instead of validity predicate.

Question

Let's discuss a couple of questions about this PR.

1. I used the notation \+ for the monoidal operation (borrowed from fcsl-pcm package) and id for the unit.
   Do we have better suggestions? My minor concern, is that id is shorthand for identity, but using \+ and 1 as a unit of monoid a bit frustrating... Also, perhaps we want a notation for the unit, like 0, 1, or \eps etc?

2. For the orthogonality I picked the \perp latex notation (Unicode)? Any alternative suggestions?

3. Also, we got some inspiration from fcsl-pcm, so perhaps we should mention the authors? What is a proper way to do this? @anton-trunov

[1] Bart Jacobs --- Convexity, Duality and Effects

[anton-trunov]

Also, perhaps we want a notation for the unit, like 0, 1, or \eps etc?

Some more possible alternatives:

• neu or \neu (neutral);
• \unit (so there is no confusion with the unit type);
• \0.

For the orthogonality I picked the \perp latex notation (Unicode)? Any alternative suggestions?

I'm fine with \perp. A possible alternative could be FCSL's \orth?

Also, we got some inspiration from fcsl-pcm, so perhaps we should mention the authors? What is a proper way to do this?

I think mentioning this in the README file and in the commit message should be fine.

[anton-trunov]

Ah, in my previous comment I missed we use Unicode for orthogonality. Perhaps we should use ⊕ for the monoidal operation?

[eupp]

In the end, I've decided to choose the following names :)

• zero and \0 for monoidal unit
• plus and \+ for monoidal operation