Re: [Axiom-developer] StepThrough

[Martin Rubey]

Dear Bill, Cliff,

Clifford, are you still there? I'm not quite sure about your status now, are
you interested in pursuing this project?

"Bill Page" <address@hidden> writes:

> > Float is -- although obviously different from the reals 
> > -- a *model* for them. So it would *not* have COUNTABLE.
> 
> I am not exactly sure what you mean by *model* in this case but I do not
> think Float is any more of a model for reals than is Fraction Integer. 
> It is no more difficult to define 'nextItem' in Float than it is in Fraction
> Integer. Instead of 'numer' and 'denom' we have 'mantissa' and 'exponent'.

OK, I surrender.

> On the other hand there is some very important work on "Exact Real Numbers"
> and "Computable Numbers". See:
> 
> http://wiki.axiom-developer.org/RealNumbers
> 
> which in my opinion might well be said to be models for the reals. Although
> these numbers are "computable" it seems to me that it might be rather hard to
> construct a useful total ordering and to compute something like 'nextItem'.

Since the set of computable numbers is countable and we can clearly only define
domains containing computable numbers in Axiom, all domains would have
COUNTABLE. Of course for some domains it will be more difficult to come up with
an enumeration than for others.

I had the feeling that FLOAT and EXPR INT were domains which should not be
countable, but it seems that this feeling should not be trusted.

In any case, it does make sense to sharpen the meaning of StepThrough.

-------------------------------------------------------------------------------
  
> > > As far as I know there is no operation of 'prevItem' anywhere in Axiom
> > > and implementing it in addition to 'nextItem' or 'memberOf' might be
> > > challenging in some peculiar cases.
> > 
> > No, it is trivial given nextItem.
> 
> In what sense? Of course you can always write
> 
>  prevItem(x) ==
>   n=init()
>   repeat
>     p=n
>     n=nextItem(n)
>     x=n ==> p
> 
> But this could take a long time or a lot of space. 

Yes. Of course, I did not claim that it would be efficient. However, in all
cases I considered, it was trivial.

I suspect that it will usually be only a simply modification of the algorithm
for nextItem.

> > Here comes some code:
> >
> > This would replace STEP in catdef.spad:
> > ...
> > ++ For infinite domains, repeated application of
> > ++ \spadfun{nextItem} is guaranteed to reach all possible
> > +  domain elements starting from the initial element.
> 
> So the main difference between Countable and the original
> StepThrough category:
> 
> > ++ For infinite domains, repeated application
> > ++ \spadfun{nextItem} is not required to reach all possible
> > ++ domain elements starting from any initial element.
> 
> is replacing 'not required to' with 'guaranteed to' 

Yes. Well, it's the only difference.

> Yes I see. The current code in Fraction is:
> 
> if S has StepThrough then
>   init() == init()$S / 1$S
>   nextItem(n) ==
>     m:= nextItem(numer(n))
>     m case "failed" =>
>       error "We seem to have a Fraction of a finite object"
>     m / 1
> 
> So although it obviously is not guaranteed to reach all
> possible domain elements, it does "StepThrough" it.
> 
> > I claim that STEP is brain-dead, because it achieves much less 
> > than what can be achieved.
> 
> I agree. But worse than that, it seems that the current
> implementation of 'nextItem' in 'Fraction' does not even meet
> the requirements of 'StepThrough' for finite Fraction objects!

Fraction takes an integral domain as parameter, and a finite integral domain is
a field. In fact, the domain Fraction should really test whether it's parameter
is a field and in this case return an error -- the interpreter does
this. Alternatively, we could say that in this case the denominator is always
equal to one.

It is not difficult to extend my code to "finite fraction objects". In fact, I
coded it that way first, until I discovered that the parameter domain is not
allowed to be finite.

Thus, it might be better to implement nextItem in the domain Localize.

Martin