Maude-help mailing list

[Scott Christley <schristley AT mac.com>]

Hello,

I'm having difficulty with defining some operators where I'm using equations 
to reduce my "statements" to a canonical form.  Here is a simple test module 
to illustrate:

***
mod definitions is
  including NAT .

  sort gene .
  sort mrna .
  sort statement .

  op transcribe : gene mrna -> statement .
  op _ is transcribed into _ : gene mrna -> statement .

  *** canonical form
  var G : gene .
  var R : mrna .
  eq G is transcribed into R = transcribe(G, R) .

  op statementID : statement -> Nat .

  op lasR-gene : -> gene .
  op lasR-mRNA : -> mrna .

endm

mod model is
  including definitions .

  op statement1 : -> statement .
  eq statement1 = lasR-gene is transcribed into lasR-mRNA .

  *** this does not work
  eq statementID(statement1) = 1 .

  *** this works
  ***eq statementID(transcribe(lasR-gene, lasR-mRNA)) = 1 .

endm
***

When I do a reduction:

Maude> reduce statementID(statement1) .
reduce in model : statementID(statement1) .
rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: statementID(transcribe(lasR-gene, lasR-mRNA))

I don't get back what I want, which is the number 1.

To explain further, in the test example I have two operators which I 
considered equivalent:

  op transcribe : gene mrna -> statement .
  op _ is transcribed into _ : gene mrna -> statement .

The basic idea being that there are different ways to "describe" the same 
thing, so what I do is define a canonical form for all statements that have 
the same semantics.  That is the reason for this code:

  *** canonical form
  var G : gene .
  var R : mrna .
  eq G is transcribed into R = transcribe(G, R) .

So when I do a reduce of "lasR-gene is transcribed into lasR-mRNA" then it is 
put in canonical form "transcribe(lasR-gene, lasR-mRNA)".  Later I define 
rewrite rules and etc on the canonical forms.

That all works fine.  The problem is I want to attach some additional 
operators, for example a statement ID number:

  op statementID : statement -> Nat .

Then I equate a statement to a specific number, so that I can retrieve it 
later

  op statement1 : -> statement .
  eq statement1 = lasR-gene is transcribed into lasR-mRNA .
  eq statementID(statement1) = 1 .

but this doesn't work as shown with the reduce output above.  The problem is 
that I need to define that equation using the canonical form, so if I did 
this instead:

  eq statementID(transcribe(lasR-gene, lasR-mRNA)) = 1 .

then the reduce works.

Maude> reduce statementID(statement1) .
reduce in model : statementID(statement1) .
rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
result NzNat: 1

However, I don't know the canonical form of the statement ahead of time.  I'm 
generating the module "model" automatically, and the statement ID number is a 
way for me to keep track of the "statements" I send to maude, which connects 
them to other external data.

Any idea how to do this?  Is there some attribute or way I write the 
operator/equation that allows me to define it using the non-canonical form?

The only thing I can think of is to manually reduce each "statement" 
individually, extract the canonical form from the maude result, then compose 
the "model" module, but this is a lot of work and kinda defeats using maude 
in the first place.

I could use rewrite rules if that would work, or maybe use the meta operators 
in full maude?

thanks
Scott