[Maude-help] Ints greater than 3 (follow up)

[Craig Ugoretz]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.cs.uiuc.edu/mailman/private/maude-help/attachments/20051122/59d44041/attachment.html