Maude-help mailing list

[Craig Ugoretz <craigugoretz AT gmail.com>]

Dear Steven,

 

        Thank you for your prompt and descriptive reply to my previous email.  After reviewing your response, I have some questions to ask you.

 

1)  In your response, you mention the term "interated tower".  I looked this term up in the Maude reference manual, but was not able to find it.  I did find the term "reflective tower".  Are these two terms related somehow?

 

2)  What if I desired to write a functional module that defines a sort for integers greater than 9876543210?  The technique that you used, although very effective for small numbers, does not seem to hold in terms of ease of programming for larger integers.  Is this the case?  However, I do feel like I understand what you demonstrated - the s_ constructor cause the rewriting to "move up" the connected component defined by the sort and subsort constructs.

 

3)  Reference to the term "number hierarchy" in your response prompted me to look at section 6.6.4 of the Maude reference manual, and the to begin with, the PEANO-NAT functional module in particular.  I have four questions about it:

 

      a)  In the case of the s_ constructor, it has an arity of type Nat and a coarity of type NzNat.  I understand this much: natural numbers include zero, and nonzero natural numbers do not include zero.  For this reason, the arities account for the case where a zero (a Nat) is incremented by one into a one (a NzNat).  Is it true that it would not be within reason to overload the s_ constructor to account for the cases Zero -> NzNat and NzNat -> NzNat since no variable is declared for Zero (but a constant is) and the coarity for NzNat -> NzNat is covered by the fact that NzNat is a subsort of Nat?

 

      b)  In the case of the _*_ operator with the signature NzNat NzNat -> NzNat [comm], why is subsort overloading of the _*_ operator with the signature Nat Nat -> Nat [comm] used?  Is out of the necessity to define the equations appropriately for Peano natural numbers?  Which leads to the third question ...

 

      c)  How has it been determined that the equations given satisfy the requirements for Peano natural numbers?  Is the list of operators given in this example comprehensive?  If not, how was the choice of operators made?  How was testing done?

 

      d) Finally, I read in the manual that term rewriting is recursive, requiring a base case and cases to induct on.  In general, would it be helpful to go beyond the material in the Maude manual in order to effectively employ term rewriting?  For example, there is a book on the market titled " Term Rewriting and All That" by Franz Baader and Tobias Nipkow that seems introductory.  Would I need to use a book like this to go beyond my basic knowledge of recursion?

 

                                                                                   Thanks,

                                                                                   Craig