Re: structural congruence

[Robin Milner <Robin.Milner@xxxxxxxxxxxx>]

The structural congruence (sc) of Engelfriet and Gelsema is a very
nice result, and because of their extra laws it seems much more
tractable than the "original".  The main virtue of the original sc 
is that, in some sense. the law !P == P | !P is "all you need"
to allow copies of P to be created arbitrarily.

Anyway,	I spent several days thinking about decidability of the original
sc, one or two years ago.  I immediately created this subproblem:

	Decide the word problem for the algebraic theory with
	one unary and one binary operator, called * and x say, 
	and three equations: x is associative and commutative,
	and *A = A x *A.  

Anyone with a taste for word problems should try it.  (Add a unit for
x if you like; it doesn't seem to help or hinder.)  I came to the
conclusion that I could probably solve it, but using some fairly
structures (since there is no obvious normal form).  It was quite
hairy.  Does Gelsema's message imply some progress with this?

I also noticed that even with a solution, extending it to the original
sc (i.e. adding restriction at least) would not be easy.

Robin Milner

 
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html