Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!zaphod.mps.ohio-state.edu!cis.ohio-state.edu!ucbvax!bloom-beacon!eru!hagbard!sunic!cs.umu.se!fridhem!bylund
From: bylund@cs.umu.se (Stefan Bylund)
Newsgroups: comp.theory
Subject: Re: Term/tree-rewriting systems with monoidal subsystems?
Message-ID: <bylund.675609253@fridhem>
Date: 30 May 91 13:14:13 GMT
References: <1991May21.213311.12104@cs.ubc.ca>
Sender: news@cs.umu.se (News Administrator)
Organization: Dep. of Info.Proc, Umea Univ., Sweden
Lines: 67

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