Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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

share|improve this question
    
If your semigroup is not assiciative, then it is not a semigroup... In, say, the first order theory of semigroups, the proof that the operation is associative is trivial, as it is directly an axiom. –  Mariano Suárez-Alvarez Apr 8 '10 at 22:05
    
It is not true, on the other hand, that classically it is not important to prove that objects satisfy the properties they are supposed to satisfy. There is a proof that the sum of Peano numbers is associative, for example! –  Mariano Suárez-Alvarez Apr 8 '10 at 22:06
    
Even when associativity is an axiom, you still need to show that it is 'true' in a putative model. So what do you do with that proof once you have it? –  Jacques Carette Apr 8 '10 at 22:08
1  
As for your second comment: you misunderstood my question there. I know that Peano numbers are associative if I'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. –  Jacques Carette Apr 8 '10 at 22:11
    
Jacques, I changed a word in the title, which didn't make sense before. Hope I've conveyed the intended meaning. –  Tom Leinster Apr 8 '10 at 22:48
show 1 more comment

2 Answers 2

up vote 3 down vote accepted

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

share|improve this answer
    
So why does Coq (and Isabelle and ...) keep the proof object? –  Jacques Carette Apr 9 '10 at 0:15
    
Isabelle doesn't have to! IIRC, it's an option you can flip on or off, depending on whether you want speed or an audit trail. Coq has multiple models, including ones in which the kind Prop is just the booleans as above. This is why the computation of a Set is never allowed to depend on the inhabitant of a Prop. It also has models where propositions do have nontrivial structure (this is why homotopy theorists have gotten interested in type theory), but naturally these are not basic topos models. –  Neel Krishnaswami Apr 9 '10 at 8:34
1  
I'm late to the party, I know, but: Coq keeps the proof object because otherwise type-checking would be undecidable. In order to check whether $(S,*)$ has type semigroup, the type-checker would need to decide whether there exists a proof of $\forall x,y,z : S. (x*y)*z = x*(y*z)$, and this is undecidable in general. –  user7247 Jul 28 '10 at 10:50
add comment

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

share|improve this answer
    
Actually, this was meant to be prover-generic, I just picked Coq to be a bit more specific. But thanks for the added details. –  Jacques Carette Dec 3 '11 at 2:56
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.