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

I was wondering what kind of tools are available (if any) for avoiding pages of bracket manipulations in proving associativity properties.

To be concrete, a (more easily stated) analogue of the particular problem I have in mind is:

We have $M$ a magma (a set with a binary operation) and six elements $a, b, c, x, y, z$. I want to prove that $(xy)z = x(yz)$ and I know that

i) right composition with any of $a, b, c$ is injective (e.g. the map $M \to M$ given by $m \mapsto ma$ is injective),

ii) we have the associativity relation for any triple that does not contain two consecutive expressions that contain one of $x, y, z$, (e.g. $z(ab) = (za)b$ and $y((ab)z) = (y(ab))z$),

iii) any pair consisting of one element of $a, b, c$ and one from $z, y, x$ is commutative (e.g. $ax = xa$).

The idea is to convert $x(y(z(a(bc))))$ into $a(x(b(y(cz))))$ where we can then rearrange the brackets.

It feels to me like there should exist a framework for doing this cleanly without having to dirty my hands or the readers eyes with pages of equations (which by the way, I have already written out for my version of the problem and am dreading converting into LaTeX).

A potential framework to my mind is to write such a nested bracketed expression like this as a tree with the $x, y, z, a, b, c$ as leaves. Then the relations i, ii, iii correspond to operations converting one tree to another. In a perfect world, one can prove that my relations are sufficient to generate all possible trees with $a, b, c, x, y, z$ as leaves.

share|improve this question
    
You need to be more explicit in ii: it is not clear that y((bc)z) or even y(b(cz)) can be arranged to (y(bc))z or (yb)(cz). How do you do that, or do without that? Gerhard "Ask Me About System Design" Paseman, 2011.12.07 –  Gerhard Paseman Dec 8 '11 at 6:38
    
@Gerhard Paseman: True. I apologise, this is an analogous problem to the one I solved, and I didn't translate the hypotheses properly. I've edited the question but its possible that there are still some missing hypotheses. I was hoping the flavour of the problem (independently of its solvability) would be enough to provoke the answer I'm looking for. –  name Dec 8 '11 at 7:29
    
Then essentially Bruce's answer is the way to go. That, or construct the free such object and show it does not have the desired property. Most of my experience has been using the equational route: while converting to trees has been good for visualization, the proofs (for me) don't seem any cleaner. If the real issue is pages of equations, you might be able to refactor your proof and find some useful lemmas. That also takes a while, but is very satisfying when it happens. Gerhard "Ask Me About Finite Bases" Paseman, 2011.12.08 –  Gerhard Paseman Dec 8 '11 at 9:32
add comment

2 Answers

up vote 8 down vote accepted

Thompson's group $F$ is the group "responsible" for associativity relations. It does act on binary trees. I am not sure it will help you much because you would probably have to explain to the readers what Thompson's group is, but in fact proving associativity relation amounts to manipulating with elements of $F$.

share|improve this answer
    
Thanks, thats what I was looking for. –  name Dec 8 '11 at 12:07
add comment

The usual method for proving that a magma is associative is to realise it as a submagma of a monoid.

share|improve this answer
    
Thanks Bruce, at first glance it seems unlikely in my specific case I can do this but I'll have a think about it. –  name Dec 8 '11 at 7:33
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.