Maude-help mailing list

[Francisco Durán <duran AT lcc.uma.es>]

Hi Scott,

I need further information to give you a solution, but let me give you a few 
hints.

Operationally, equations are used as rewrite rules from left to right. If 
your specification is Church-Rosser (terminating, confluent and 
sort-decreasing) then your mathematical model coincides with your operational 
model. Your spec is not confluent, and from there your confusion, your 
equations are not really equalities. 

The first thing you need to have clear in your mind is what is the form of 
your normal forms, that is, what are your constructors. And then define your 
derived operators on all possible cases (completeness, or at least sufficient 
completeness).

I don't know where you get your statement ids, but I guess you don't want to 
exhaustively define it for every single possible statement. But perhaps you 
can provide a definition for it in terms of genes and mrns, if at all 
possible. If you have gene ids in the range 0..n and mrns ids in the range 
0..m you can get some unique statement id with something like 

 id(transcribe(G, R)) = id(G) x n + id(R)

but still you need to provide unique identifiers to genes and mrns. But maybe 
they don't need to be natural numbers. An alternative would be to use 
identifiers by using their own ones. I suppose you already have identifiers 
for genes and mrns, so why not using as an identifier something like id(G, R) 
?

Cheers,

Francisco


On 10/06/2013, at 23:19, Scott Christley wrote:

> 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
> 
> 
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help