Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

The issue is that (a, b, c) and (a, (b, c)) are two distinct terms that 
belong to the same congruence class wrt to the assoc axiom. To get the 
canonical representative that is used for rewriting, you can use the 
descent function metaNormalize():

red metaNormalize(upModule('TEST, false),
                  getTerm(metaParse(upModule('TEST, false), 'a '`, 'b 
'`, 'c, anyType)))
    ==
    metaNormalize(upModule('TEST, false), upTerm((a,b,c))) .

Steven

On 3/24/13 3:18 AM, ZHANG Min wrote:
> Dear all:
>
> I found there are two forms of meta-representations of the same term by using 
> metaParse or upTerm respectively. How could we obtain a uniform term? Here is 
> an example:
>
> fmod TEST is
>         sort Test .
>         op _,_ : Test Test ->  Test [assoc] .
>         
>         ops a b c : ->  Test .
> endfm
>
> fmod TEST-META is
>      inc TEST .
>      inc META-LEVEL .
> endfm
>
>
> When I used the following command, I got:
>
> red upTerm((a,b,c)) .
>
> result GroundTerm: '_`,_['a.Test,'b.Test,'c.Test]
>
>
> The following command gave me the different form:
>
> red getTerm(metaParse(upModule('TEST, false), 'a '`, 'b '`, 'c, anyType)) .
>
> result GroundTerm: '_`,_['a.Test,'_`,_['b.Test,'c.Test]]
>
>
> But at object level, it was  a,b,c. How could I get a uniform 
> meta-representation of a term?
>
>
> http://www.jaist.ac.jp/~zhangmin
> Research Center for Software Verification
> Japan Advanced Institute of Science and Technology (JAIST)
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help