Finite and StepThrough

[Prof. Dr. Johannes Grabmeier privat]

Hi all,

Finite is Missing StepThrough! Any objection against adding a default
step through:

)abbrev category FINITE Finite
++ Author:
++ Basic Functions:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ Description:
++ The category of domains composed of a finite set of elements.
++ We include the functions \spadfun{lookup} and \spadfun{index} to give
a bijection
++ between the finite set and an initial segment of positive integers.
++
++ Axioms:
++   \spad{lookup(index(n)) = n}
++   \spad{index(lookup(s)) = s}
Finite() : Category == Join(SetCategory, ConvertibleTo InputForm,
                            Comparable, StepThrough) with
    --operations
      size : () -> NonNegativeInteger
        ++ size() returns the number of elements in the set.
      index : PositiveInteger -> %
        ++ index(i) takes a positive integer i less than or equal
        ++ to \spad{size()} and
        ++ returns the \spad{i}-th element of the set. This
        ++ operation establishes a bijection
        ++ between the elements of the finite set and \spad{1..size()}.
      lookup : % -> PositiveInteger
        ++ lookup(x) returns a positive integer such that
        ++ \spad{x = index lookup x}.
      random : () -> %
        ++ random() returns a random element from the set.
      enumerate : () -> List %
        ++ enumerate() returns list of elements of the set.
  add
      random() == index((1+random(size()$%))::PositiveInteger)

      enumerate() == [index(i::PositiveInteger) for i in 1..size()]

      convert(x : %) : InputForm ==
          packageCall('index, [convert(lookup(x))@InputForm]
                     )$InputFormFunctions1(%)

      if not(% has OrderedSet) then

          smaller?(x : %, y : %) : Boolean ==
              lookup(x) <$PositiveInteger lookup(y)
     
---------------------------------------------------------------------------
      -- exported functions from StepThrough:
     
---------------------------------------------------------------------------
      init() : % == index(1)
      nextItem(x: %): Union(%, "failed")  ==
        p : PositiveInteger := lookup(x)
        p = size() => "failed"
        index(p+1)

--
Mit freundlichen Grüßen

Johannes Grabmeier

Prof. Dr. Johannes Grabmeier
Köckstraße 1, D-94469 Deggendorf
Tel. +49-(0)-991-2979584, Tel. +49-(0)-151-681-70756
Tel. +49-(0)-991-3615-141 (d), Fax: +49-(0)-32224-192688

[Ralf Hemmecke]

Looks fine to me, but I don't know how this changes the behaviour of the
interpreter.

Can you provide a concrete example (that you care about)that doesn't
work now and works after extending the Finite category?

Thank you
Ralf

[Waldek Hebisch]

On Sun, Jan 05, 2020 at 08:33:58PM +0100, Prof. Dr. Johannes Grabmeier privat wrote:
> Hi all,
>
> Finite is Missing StepThrough! Any objection against adding a default
> step through:

No deep objection. But AFAICS StepThrough is:

- almost unused
- hard to use correctly
- hard to implement correctly for infinite domains build
on top of finite ones

To be more precise, the only actiual use that I found is to
"emulate" random. But it is well-known that sequentialy
stepping trough elements can lead to very bad runtime
compared to using random elements.

AFAICS implementation of StepTrough in SparseUnivariatePolynomial
is still incorrect: it will produce duplicates when 0 is not
the first element in the sequence.

So, if you have good use for StepTrough, then we can add it to
Finite. But otherwise I would rather look towards removal of
StepTrough.

--
Waldek Hebisch