[Axiom-developer] Again a problem, probably about dependend types...

[Martin Rubey]

Dear all,

in my effort to teach axiom expanding products in Puiseux series, I ran into a
new problem. We touched this before, it seems to me, but maybe our knowledge
has increased since then.

To make it brief, the following signature is given (I have little possibility
of changing it):

)abbrev package TEST Test
Test(R, FE, Expon, UPS, z:Symbol): Exports == Implementation where
  R     : Join(OrderedSet, GcdDomain)
  FE    : Join(FunctionSpace R, CombinatorialOpsCategory)
  Expon : OrderedAbelianMonoid
  UPS   : UnivariatePowerSeriesCategory(FE, Expon)

this is roughly the signature of FS2UPS. z is supposed to be the variable of
the series the packages is dealing with.

To expand a product

product(a(i,z),z=1..m)

into a Puiseux series, I can expand a(i,z) into a Puiseux series and apply the
product afterwards. For example, if a(i,z)=1/(i-z), we have

(45) -> s:=series(1/(i-z),=0)

         1    1      1  2      3
   (45)  - + -- z + -- z  + O(z )
         i    2      3
             i      i
                        Type: UnivariatePuiseuxSeries(Expression Integer,z,0)
(46) -> ps := prodToUPS(s,i,1,m)$Test(INT, EXPR INT, NNI, UTS(EXPR INT, z, 0), 
z)

   (46)
       m          m       m
     ++-++  1   ++-++  1 --+     1
      | |   - +  | |   - >      ---z
      | |   i    | |   i --+    %IF
     i= 1       i= 1    %IF= 1
   + 
                      %IF - 1
                        --+     1
                        >      ---
        m       m       --+    %IH     m       m
      ++-++  1 --+    %IH= 1         ++-++  1 --+      1   2      3
     ( | |   - >      ------------ +  | |   - >      ----)z  + O(z )
       | |   i --+         %IF        | |   i --+       2
      i= 1    %IF= 1                 i= 1    %IF= 1  %IF
                         Type: UnivariateTaylorSeries(Expression Integer,z,0)

To do so, I believe I currently extract the stream of coefficients of the
series corresponding to a(i,z) and then consider all compositions of k to
obtain the coefficient of z^k.

This works well for Taylor series, apart from the fact that it is obviously an
exponential problem: there are 2^(k-1) compositions of k, so it *really* works
only if we say something like

)set stream calculate 3

before.

However, the although the mathematics works just as well for any Puiseux
series, I don't see how to extract a stream of coefficients from a UPS in my
package. To illustrate the problem, suppose that the series is retractable to a
Taylor series, i.e., only nonnegative, integral exponents occur.

In this case I would like to retract the series to a Taylor series, but this
cannot be done without knowing the center, since the target type is unknown: I
would like say

     prodToUPS(series, var, lo, hi) ==
       if UPS has retract: UPS -> UnivariateTaylorSeries(FE, z, center(series))
       then 
         ps := retract(series)$UPS
         series prodseries(coefficients ps, var, lo, hi)
       else error "no coefficients"

but this fails. (It compiles, but then aborts with memory damage :-)

Is there any way to correct this?

Martin