Re: [Axiom-developer] StepThrough

[Martin Rubey]

"Bill Page" <address@hidden> writes:

> According to the documentation:
> 
> http://wiki.axiom-developer.org/axiom--test--1/src/algebra/CatdefSpad
> 
> StepThrough denotes:
> 
> "A class of objects which can be 'stepped through'.  Repeated applications of
> \spadfun{nextItem} is guaranteed never to return duplicate items and only
> return "failed" after exhausting all elements of the domain.  This assumes
> that the sequence starts with \spad{init()}.  For infinite domains, repeated
> application \spadfun{nextItem} is not required to reach all possible domain
> elements starting from any initial element."
> 
> -------
> 
> So 'init()$SomeDomain' is not required to be uniquely defined.  It can in
> principle be any member of the domain. But some choices might be more
> convenient then others because of the requirements of 'nextItem'.

Well, there are hardly any requirments on nextItem. Only duplicates are
forbidden, that's not much.

> > How do you define what element comes "after" another element?
> 
> Since all representable members of a domain must have some
> finite representation (i.e. internally represented by some
> finite pattern of bits), so every member can be sorted in
> at least this way with respect to all other members. In specific
> cases, other orderings may be more convenient.
> 
> > I suppose Positive Real [sic] Integers would be obvious -
> > init()->0, after that comes 1, etc., but you suggest "Float"
> > should have StepThrough implemented? 

NO. Float is -- although obviously different from the reals -- a *model* for
them. So it would *not* have COUNTABLE.

> 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. However, it is *necessary* for implementing
nextItem$COUNTABLE for the Fractions, for example. Here comes some code:

This would replace STEP in catdef.spad:

)abbrev category COUNTABLE Countable
++ Description:
++ A class of objects which is countable. Intended as a replacement for
++ StepThrough. Repeated applications of \spadfun{nextItem} is guaranteed never
++ to return duplicate items and only return "failed" after exhausting all
++ elements of the domain.  This assumes that the sequence starts with
++ \spad{init()}.  For infinite domains, repeated application of
++ \spadfun{nextItem} is guaranteed to reach all possible domain elements
++ starting from the initial element.
++ Conditional attributes:
++   infinite\tab{15}repeated \spad{nextItem}'s are never "failed".
Countable(): Category == SetCategory with
    --operations
      init: constant -> %
        ++ init() chooses an initial object for stepping.
      nextItem: % -> Union(%,"failed")
        ++ nextItem(x) returns the next item, or "failed" if domain is 
exhausted.
      prevItem: % -> Union(%,"failed")
        ++ prevItem(x) returns the previous item, or "failed" if x=init().


Some comments:

This is only the bare minimum of operations. Very often (but not always) it
will be possible to implement an efficient operation nthItem. This might be
interesting for the generation of random elements of the domain according to
some distribution.

For many domains it will be possible to implement nextItem as a GrayCode...


And here is an example for an implementation for the domain FRAC in
fraction.spad:


    if S has StepThrough then
       init() == init()$S / 1$S

       nextItem(n) ==
         r := numer n
         if r = 0 then return 1
         s := denom n
         if (d1 := init()$S) = 0 then 
           d2: Union(S, "failed") := nextItem(d1)
           d2 case "failed" =>
             error "QuotientFieldCategory: a finite IntegralDomain _
                    should be a field"
           d1 := d2
         repeat
           if r = d1 then
             num := nextItem(s)
             den := r::Union(S, "failed")
           else
             num := prevItem(r)
             den := nextItem(s)

           (num case "failed") or (den case "failed") =>
             error "QuotientFieldCategory: a finite IntegralDomain _
                    should be a field"
           if numer(m:=(num::S/den::S)) = num::S then 
             return m
           else
             r := num::S
             s := den::S

It is a straightforward implementation of the diagonal argument I posted in a
previous mail.


> I am not sure what Martin means here about working code for 'fraction.spad'
> since it seems to me that it already has some working code for 'StepThrough',
> but I would encourage him to put something in the SandBox on the Axiom wiki
> so that you can start to play with it.

Now you hopefully see what I meant: The above is code for an implementation of
COUNTABLE for FRAC...

I claim that STEP is braindead, because it achieves much less than what can be
achieved.

> * univariate polynomials with coefficients in a counatble set, since
> the union of countably many countable sets is countable... Can you 
> find an effective enumeration?


C Y <address@hidden> writes:

> Define effective...  

Given a statement like "this set is countable", "effective" means that we can
implement an algorithm that enumerates all elements of the set -- possibly in
infinite time, though.

"Ineffective" would be, if we knew for some reason that a set is countable, but
we do not know how to give an enumeration.

For example, the wikipedia says -- correctly:

THEOREM: (Assuming the axiom of choice) The union of countably many countable
         sets is countable.

Thus we know now that the set of polynomials with coefficients in a countable
set and variables from a countable set is countable. Let's do univariate
polynomials in the variable x for a start:

Let R=(c1, c2, c3, ...) be the set of coefficients

Let P_d be the set of univariate polynomials of degree d with coefficients in
R.

Lemma: P_d is countable:

Proof: 

indices sum up to d

c1 + c1 x + c1 x^2 + ... + c1 x^d
                   
indices sum up to d+1
     
c2 + c1 x + c1 x^2 + ... + c1 x^d
                        
c1 + c2 x + c1 x^2 + ... + c1 x^d
                        
c1 + c1 x + c2 x^2 + ... + c1 x^d

...

c1 + c1 x + c1 x^2 + ... + c2 x^d

indices sum up to d+2

c2 + c2 x + c1 x^2 + ...             + c1 x^d

c2 + c1 x + c2 x^2 + ...             + c1 x^d

c2 + c1 x + c1 x^2 + ...             + c2 x^d

...

c1 + c1 x + c1 x^2 + .. + c2 x^(d-1) + c2 x^d

c3 + c1 x + c1 x^2 + ... + c1 x^d
                        
c1 + c3 x + c1 x^2 + ... + c1 x^d
                        
c1 + c1 x + c3 x^2 + ... + c1 x^d

...

c1 + c1 x + c1 x^2 + ... + c3 x^d

indices sum up to d+3

c2 + c2 x + c2 x^2 + ...             + c1 x^d

...

See how it goes on?              [end of Proof]

Now let

Let P be the set of univariate polynomials with coefficients in R.

Proposition: P is countable

Proof: P = U_{d>=0} P_d          [end of Proof]

The proof of the Lemma is effective, but the proof of the Proposition is not.
However, it is quite easy to give an effective proof. Try it!

By the way, I was wrong in one point. I said

> Thus, FLOAT, EXPR, AN are examples of domains that should *not* have STEP.

This is incorrect, since the Wikipedia says:

By a similar development, the set of algebraic numbers is countable, 

Thus AN should have COUNTABLE. (FLOAT and EXPR should not, that was correct.)

If you embark on this, I advise you to do the easy domains first:

NNI, PI, INT, FRAC.

SYMBOL might be a little more difficult in terms of implementation.

When you have done this, I suggest that you try to find an effective proof of
the Proposition above, or, if you do not succeed, I'll help. In any case, I
think it would be a good project for you, since the mathematics is easy to
follow, but the implementation might be difficult.

Finally, it would be necessary to document the operations that currently *use*
STEP, i.e., the operations in GENPGCD and in PFBRU.

Martin