Maude-help mailing list

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

Hi Scott,

Sorry for the delay in replying; there must have been some delay with
the mailing list since I only saw your message today.

There are a number of issues with your specification. Firstly you are
instantiating two copies of LIST, and then bashing them together. As
the advisories indicate this is inadvisable and will cause problems
unless you are very careful with overloaded definitions.

Also you are not handling the case of a list composed of nucleotides
common to both DNA and RNA.

In general when using a container of elements with subsorts, I
recommend creating the container on a  supersort first and then refining
the sort information associated with the constructors. This way any
operators that come with the container and are ignorant of the sort
structure on the elements are defined at the top of the sort structure
and work correctly.

I would use the name Nucleotide for this top sort and use
CommonNucleotide for the intersection sort:

fmod NUCLEOTIDE is
  sorts CommonNucleotide DNANucleotide RNANucleotide Nucleotide .
  subsorts CommonNucleotide < DNANucleotide RNANucleotide < Nucleotide .

  ops A C G : -> CommonNucleotide .
  op T : -> DNANucleotide .
  op U : -> RNANucleotide .
endfm

Now your view just works at the top of the sort structure:

view Nucleotide from TRIV to NUCLEOTIDE is
  sort Elt to Nucleotide .
endv

Now the differnet kinds of sequences can be defined by adding extra
declarations for the list contructor __ . Note that is necessary to
handle sequences of common nucleotides in order for a list like A C G
to have a unique least sort:

fmod SEQUENCE is
  protecting LIST{Nucleotide} .
  sorts CommonSequence DNASequence RNASequence .
  subsort DNANucleotide < DNASequence < NeList{Nucleotide} .
  subsort RNANucleotide < RNASequence < NeList{Nucleotide} .
  subsort CommonNucleotide < CommonSequence < DNASequence RNASequence .
  op __ : DNASequence DNASequence -> DNASequence [ctor ditto] .
  op __ : RNASequence RNASequence -> RNASequence [ctor ditto] .
  op __ : CommonSequence CommonSequence -> CommonSequence [ctor ditto] .
endfm

Now your translation example will work:

fmod transcription is
  protecting SEQUENCE .

  op translate : DNASequence -> RNASequence .

  var aSequence : DNASequence .

  eq translate(A) = A .
  eq translate(C) = C .
  eq translate(G) = G .
  eq translate(T) = U .
  eq translate(A aSequence) = A translate(aSequence) .
  eq translate(C aSequence) = C translate(aSequence) .
  eq translate(G aSequence) = G translate(aSequence) .
  eq translate(T aSequence) = U translate(aSequence) .
endfm

red translate(A T G T C C) .

However it can be improved; now that there is a notion of common
nucleotides, this cases can be collapsed:

fmod transcription is
  protecting SEQUENCE .

  op translate : DNASequence -> RNASequence .

  var aSequence : DNASequence .
  var cNuc : CommonNucleotide .

  eq translate(cNuc) = cNuc .
  eq translate(T) = U .
  eq translate(cNuc aSequence) = cNuc translate(aSequence) .
  eq translate(T aSequence) = U translate(aSequence) .
endfm

red translate(A T G T C C) .

Also you could collapse the two remaining induction cases at the cost
of an extra rewrite per nucleotide:

fmod transcription is
  protecting SEQUENCE .

  op translate : DNASequence -> RNASequence .

  var aSequence : DNASequence .
  var cNuc : CommonNucleotide .
  var Nuc : Nucleotide .

  eq translate(cNuc) = cNuc .
  eq translate(T) = U .
  eq translate(Nuc aSequence) = translate(Nuc) translate(aSequence) .
endfm

red translate(A T G T C C) .

Steven




On Thursday 20 April 2006 16:20, Scott Christley wrote:
> Hello,
>
> I recently downloaded Maude, read through the tutorial and  documentation,
> and am trying to write some modules.  I wanted to do a  simple biological
> example for DNA transcription to RNA; a tricky part  is that DNA and RNA
> share the bases A, C, and G but DNA has T while  RNA has U.  So I created a
> module for nucleotides:
>
> fmod nucleic is
>   sorts Nucleotide .
>
>   ops A C G : -> Nucleotide .
> endfm
>
>
> Then I wanted sequences of DNA and RNA to be lists so that I could  easily
> concatenate bases, e.g. (A T G T C C) for DNA or (A U G U C C)  for RNA.  I
> want Maude to recognize one as DNASequence and the other  as RNASequence
> thus not allow U's in DNA nor allow T's in RNA.  So I  defined these
> modules:
>
>
> fmod DNA is
>   protecting nucleic .
>   sorts DNANucleotide .
>   subsort Nucleotide < DNANucleotide .
>
>   op T : -> DNANucleotide .
> endfm
>
> view DNA from TRIV to DNA is
>   sort Elt to DNANucleotide .
> endv
>
> fmod DNASequence is
>   protecting LIST{DNA} * (sort NeList{DNA} to DNASequence) .
> endfm
>
>
> fmod RNA is
>   protecting nucleic .
>   sorts RNANucleotide .
>   subsort Nucleotide < RNANucleotide .
>
>   op U : -> RNANucleotide .
> endfm
>
> view RNA from TRIV to RNA is
>   sort Elt to RNANucleotide .
> endv
>
> fmod RNASequence is
>   protecting LIST{RNA} * (sort NeList{RNA} to RNASequence) .
> endfm
>
>
> Lastly I make a module which is the transcription machinery, and  there is
> where the problem comes in.
>
>
> fmod transcription is
>   protecting DNASequence .
>   protecting RNASequence .
>
>   op translate : DNASequence -> RNASequence .
>
>   var aSequence : DNASequence .
>
>   eq translate(A) = A .
>   eq translate(C) = C .
>   eq translate(G) = G .
>   eq translate(T) = U .
>   eq translate(A aSequence) = A translate(aSequence) .
>   eq translate(C aSequence) = C translate(aSequence) .
>   eq translate(G aSequence) = G translate(aSequence) .
>   eq translate(T aSequence) = U translate(aSequence) .
> endfm
>
>
> When I load up this module, I get advisories:
>
>
> Advisory: "transcription.maude", line 7 (fmod transcription):  operator nil
> has been imported from both "prelude.maude", line 939 (fmod LIST) and
> "prelude.maude", line 939 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator __ has been
> imported from both "prelude.maude", line 940 (fmod LIST) and
> "prelude.maude", line 940 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator append has
> been imported from both "prelude.maude", line 948 (fmod  LIST) and
> "prelude.maude", line 948 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator head has been
> imported from both "prelude.maude", line 953 (fmod LIST) and
> "prelude.maude", line 953 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator tail has been
> imported from both "prelude.maude", line 956 (fmod LIST) and
> "prelude.maude", line 956 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator last has been
> imported from both "prelude.maude", line 959 (fmod LIST) and
> "prelude.maude", line 959 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator front has
> been imported from both "prelude.maude", line 962 (fmod  LIST) and
> "prelude.maude", line 962 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator occurs has
> been imported from both "prelude.maude", line 965 (fmod  LIST) and
> "prelude.maude", line 965 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator reverse has
> been imported from both "prelude.maude", line 969 (fmod  LIST) and
> "prelude.maude", line 969 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator $reverse has
> been imported from both "prelude.maude", line 973 (fmod  LIST) and
> "prelude.maude", line 973 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator size has been
> imported from both "prelude.maude", line 977 (fmod LIST) and
> "prelude.maude", line 977 (fmod LIST) with no common ancestor. Advisory:
> "transcription.maude", line 7 (fmod transcription):  operator $size has
> been imported from both "prelude.maude", line 981 (fmod  LIST) and
> "prelude.maude", line 981 (fmod LIST) with no common ancestor.
>
>
> And the reduce doesn't work:
>
> reduce in transcription : translate(A T G T C C) .
>
> Warning: sort declarations for constant nil do not have an unique  least
> sort. reduce in transcription : translate(A T G T C C) .
> rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
> result [EmDNASequence,EmRNASequence,NucleotideSequence]: translate(A  T G T
> C C)
>
>
>
> Can anybody tell me what I'm doing wrong?
>
> thanks
> Scott
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help