RE: structural congruence

["Gelsema, drs. T.E." <TGSA@xxxxxx>]

Hello all,

Joost and I showed that the decidability of Milner's 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.  
> 

amounts (more or less) to solving a system of linear equations with integer
coefficients. The decidability of the sc without the
scope-extrusion/intrusion law (call this congruence rigid-sc) is a
straightforward implication of this result. Indeed, due to the apparent lack
of a suitable normal form (the congruence classes of r-sc are associated
with linear subspaces), we focussed this time on the decidability of r-sc
rather than on the construction of a model.

However, we also found that

> ... extending it to the original
> sc (i.e. adding restriction at least) would not be easy.

Thus, to our knowledge, the decidability of original sc is still open, but
from our point of view there are at least two ways of tackling it: either
'restrict' the use of our law of replicating components of processes

!(P | Q) == !(P | Q) | P

so that it 'mimics' the original law !P == !P | P, or reduce the
decidability of sc to that of r-sc. Again, this is not trivial at all: the
real trouble seems to stem from the subtle 'interaction' of the law(s) of
replication with the scope extrusion law.

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