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

[Steven Eker]

On Tuesday 22 November 2005 04:39, Craig Ugoretz wrote:
>  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?

No. Iterated operators are unary operators that have a special internal 
representation and a special i/o representation such that vast towers of 
nested operators can be handled efficiently.

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

For the general case it is necessary to use membership axioms however I would 
stay away from condition membership axioms since termination can be tricky. 
Here are is one way of implementing what you want:

fmod GT9876543210 is
  inc INT .
  sort Gt9876543210 .
  subsort Gt9876543210 < NzNat .

  mb s_^9876543210(N:NzNat) : Gt9876543210 .
endfm

red 1 .
red 9876543210 .
red 9876543211 .
red 100000000000000000000 .

Despite the warning about membership axioms not bein guaranteed to work 
correctly for iterated symbol this particular construction will work since 
the membership axiom only ever needs to be tried at the top of a tower.

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

The cases Zero -> NzNat and NzNat -> NzNat could be declared but would be 
superfluous since these cases are covered be the more general Nat -> NzNat 
declaration. 

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

Since _*_ should reduce on correctly form ground terms, the operator 
declaration NzNat NzNat -> NzNat only comes in to play if there are alien 
subterms or variables and a type computation for _*_ has to be performed.
The operator declarations have be chosen to return the least type that can be 
deduced.

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

Are you talking about operator declarations or equations? sort computation or 
term rewriting? sufficient completeness, ground confluence, confluence, 
termination, inductive completeness (omega-completeness), or arithmetical 
correctness?

The operator declarations (and in the case of RAT equations) I came up with 
manually. Recently they have been checked for sufficient completeness by Joe 
Hendrix using his sufficient completeness checker. NATs and INTs are 
implemented in a built in way which should be terminating and arithmetically 
correct by the algorithms of gmp. I have tried for ground confluence, 
termination and arithmetic correctness for the the RAT equations, but this 
has not been formally proved. General confluence has not been achieved nor 
has inductive completeness (and the latter may well be impossible). I am 
working on a fully algebraic specification of Maude number hierarchy that 
partly addresses some of these questions to help with theorem proving about 
Maude programs - it may be released with some future version.

The choice of operators was influence by what was in gmp and what seemed 
useful to have.

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

For programming in Maude, no. For formally analyzing term rewriting systems, 
yes.

Steven