[Maude-help] Ints greater than 3 (follow up)
eker at csl.sri.com
Wed Nov 30 14:22:39 CST 2005
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
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 .
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
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
> 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
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,
More information about the Maude-help