What is a semigroup or, what do I do with that associativity proof?

Question

Mathematically, I know what a semigroup is: It is a set S along with an associative binary operation $* : S \times S \rightarrow S$. So far, so good.

From a computational perspective, one can represent a semigroup as the tuple $\left< S,* \right>$, or my preference, as a record { S: type; $* : S \times S \rightarrow S$} which is dependently typed. So, for example, {S = $\mathbb{N}$; $* = + $} is a semigroup [assuming I have the naturals with addition already built].

Well, actually, it's not -- who says that I defined $+$ properly? Maybe I made a mistake and the $+$ that I used for $\mathbb{N}$ isn't associative. So I sure shouldn't be able to build {S = $\mathbb{N}$; $* = + $} and have that have 'type' semigroup.

So is the proof of associativity part of the type 'semigroup' (as it is in Coq for example), or is it part of the input to the 'constructor' for the semigroup type ? [The constructor is allowed to then forget the proof, at least for computational purposes].

One wrinkle here is that while the proof of associativity doesn't seem to say much, for the term algebra over the semigroup, it does induce two 'associator' functions which can perform the rewrite of $\lceil a * (b * c) \rceil \leftrightarrow \lceil (a * b) * c\rceil$ (where I use the $\lceil\ \cdot\ \rceil$ brackets to denote working over terms since semantically $a*(b*c)$ and $(a*b)*c$ denote the same thing so there is nothing to do). That associator is really quite useful [and much more so when you go to things like rings and fields, where the induced rewrites on the term algebra give rise to what can rightly be called a 'simplifier']. So the proof is quite useful in that sense.

The question boils down to: where does the 'proof' that the binary operation is associative really belong in the theory of a single semigroup, where by 'theory' here I mean both the semantic theory and the induced equational theory of the term algebra? Once I have established that $*$ is associative, can I really throw away the proof as it is not going to be used again?

(I would really want to also ask why is it that in classical mathematics, proofs are crucial, but somehow not so important that definitions of standard objects omit them. Asking that would likely be ruled as off-limits for MO as being too 'philosophical'...)

Answer 1

The answer to your real question is that all proofs are typically equated in set theories (more accurately, in topoi). That is, the interpretation of a proposition is as an element of the lattice of truth values, which in classical logic can take on either the value true or false.So, this means that if you give a semigroup as a dependent record (indexed over some family of small sets $U$, to avoid thinking about size issues):

$$(S \in U, * \in S \to S \to S, assoc : \forall x,y,z \in S.\; (x * y) * z = x * (y * z))$$

then for any two elements of this set, the $assoc$ component corresponding to the associativity proof is always the value true. This means the set of semigroups is trivially isomorphic to the subset

$$\{ (S \in U, * \in S \to S \to S) \;|\; \forall x,y,z \in S.\; (x * y) * z = x * (y * z)) \}$$

This holds even in intuitionistic topoi, since the key point is that in this setting the meaning of propositions are elements of a lattice of truth values, and the truth of a proposition is its equality to the lattice element true.

(As an aside, this highlights the fact that a theory may have an intuitionistic entailment relation, but not have a constructive reading of propositions such as a realizability or props-as-types reading. This happens a lot whenever you work relative to some open-endedly extensible gadget -- the property that propositions about your gadget should continue to be valid under extensions basically ends up defining a Kripke structure.)

Answer 2

So is the proof of associativity part of the type 'semigroup' (as it is in Coq for example), or is it part of the input to the 'constructor' for the semigroup type ? [The constructor is allowed to then forget the proof, at least for computational purposes].

Both: it is a computationally irrelevant part of the semigroup type.

The only tricky issues come up when you have to answer the following question: given two semigroups with identical underlying sets and identical multiplication operations, yet different associativity proofs, are the two semigroups equal? This question is tougher than it looks. Ideally you'd like the answer to be "yes" (which is what it is for set theorists), but when implementing a type theory it is nearly impossible (or at the very least an open research question) how to do that and still have decidable type checking. Set theorists don't care much about decidability, which lets them side-step this.

By the way, it sounds like you actually have a fairly concrete Coq question underlying this MO question. You might want to post it to the coq-club list (I sort of wish there were a Coq StackExchange).