Maude-help mailing list

[Scott Christley <schristley AT mac.com>]

Thanks for the feed back Francisco.

I see, your idea seems to be a possibility, perform a Godelization (if that's 
the right term) of each possible statement.  My statement ids are coming from 
an external source, specifically they are index numbers into a database.  The 
statements are entered and stored in the database, then passed to Maude where 
I perform some logical operations on them.  I need the statement id, so that 
I can take the results of those logical operations and map them to the 
original statement in the database.

The logical operations I perform on the statements is Church-Rosser, so I see 
that my problem is I'm trying to assign ids in a non-confluent manner to the 
statements, so yeah they are not really equalities.  I therefore need to 
construct a one-to-one mapping between the statement ids in the database and 
the Godelization number for a particular statement.  This is somewhat my 
workaround idea.  I need to perform on a reduce on each statement 
individually to get its Godelization number, then store that alongside its 
statement id in the database.

thanks
Scott

On Jun 11, 2013, at 4:02 AM, Francisco Durán wrote:

> 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
>