[comp.theory] Term/tree-rewriting systems with monoidal subsystems?

andrews@cs.ubc.ca (Jamie Andrews) (05/22/91)

     Has anyone done any work on term- or tree-rewriting systems
which have monoidal subsystems?  What I mean is, a system in
which we have a binary function symbol "concat" and a nullary
function symbol "null", and in which the following rewrites and
their inverses are possible:

concat(concat(X, Y), Z) => concat(X, concat(Y, Z))
concat(null, X) => X
concat(X, null) => X

     Have there been efficient algorithms developed for the
"rewrites to" relation for such systems?  (I assume the
consequences for general algorithms would be pretty severe.)
What are the consequences for the theoretical basis of the
systems?  (That is, are some important theorems easier, harder,
impossible to prove?)

     Please respond by e-mail if you can.  Thanks.

     The application I have in mind is to logic grammars.

--Jamie.
  andrews@cs.ubc.ca

bylund@cs.umu.se (Stefan Bylund) (05/30/91)

In <1991May21.213311.12104@cs.ubc.ca> andrews@cs.ubc.ca (Jamie Andrews) writes:

>     Has anyone done any work on term- or tree-rewriting systems
>which have monoidal subsystems?  What I mean is, a system in
>which we have a binary function symbol "concat" and a nullary
>function symbol "null", and in which the following rewrites and
>their inverses are possible:

>concat(concat(X, Y), Z) => concat(X, concat(Y, Z))
>concat(null, X) => X
>concat(X, null) => X

>     Have there been efficient algorithms developed for the
>"rewrites to" relation for such systems?  

You can specify 2nd and 3rd rule above as equations (remove all > directions) 
and complete these rules modulo the associativity of Your _concat_ function
and thereby get a Church-Rosser TRS with which You can for example prove 
syntactical term equivalence by computing unique normal forms.  
The problem is completion modulo associativity since You then need a 
unifier working modulo associativity, and I'm not sure such a finite
unifier exists. (I think it has been shown not to).

On the other hand, we maybe can complete equations modulo the empty theory.

>What are the consequences for the theoretical basis of the
>systems? 

Perhaps that a Church-Rosser TRS cannot be obtained from equations,
depending on what other things than monoids You have.

A nice thing is that I'm getting a Church-Rosser TRS when completing
(modulo the empty theory) these equations in my system uUTRL 
(ftp: ftp.cs.umu.se) which to the input

	val F = [("null",0),("concat",2)]; (* OPERATORS *)
	val V = ["x","y","z"];

	declareSignature (F,[],V);

	val e1 = concat( x, null) == x;     (* EQUATIONS *)
	val e2 = concat( null, x) == x;
	val e3 = concat( concat( x, y), z) == concat( x, concat( y, z));

	precedence [("concat",1),("null",2)]; (* RPO ORDERING *)

	val R = E_completion [e1,e2,e3] [] [] rpoOrdering 1 [];

spits out the following Church-Rosser TRS:

    concat(null, x) --> x
    concat(x, null) --> x
    concat(concat(x, y), z) --> concat(x, concat(y, z))

Hence every term will have a unique normal form rewrited in this TRS,
and we can prove things by checking syntactical equivalence.

>--Jamie.
>  andrews@cs.ubc.ca

                                         - stefan

-- 
Internet: bylund@cs.umu.se   | ``Capacity to Terminate
    / \    *                 |   Is a Specific Grace.''
    \ /   / \   /\/*\/\      |  
     *    \ /   \/\*/\/      |          - E. Dickinson