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'...)

isa proof that the sum of Peano numbers is associative, for example! $\endgroup$ – Mariano Suárez-Álvarez Apr 8 '10 at 22:06ifI've done things correctly. But what if I have not? I need to know that what I am claiming is associative isn't. Think of it as marking a student assignment (where they define + for PA incorrectly), or as debugging a type error in a program. $\endgroup$ – Jacques Carette Apr 8 '10 at 22:111more comments