[Axiom-developer] Mixing up variables: (was Re: conditionally defined functions)

[William Sit]

Hi Martin:

You wrote (referring to my axiom code (10) to (11) below):
> > As to why I think if it works, it works wrongly:
>  > Try this:
>  > 
>  > (1) -> )clear all
>  > (1) -> y:=3*x + 1
>  >     (1) 3x+1                Type: Polynomial Integer
>  > (2) -> z: UP(x, POLY INT)
>  >                             Type: Void
>  > (3) -> z:=3*x + 1
>  >     (3) 3x+1                Type: UnivariatePolynomial(x,Polynomial 
> Integer)
>  > (4) -> t:=variables(y)
>  >     (4) [x]                 Type: List Symbol
>  > (5) -> s:=variables(z)
>  >     (5) ["?"]               Type: List SingletonAsOrderedSet
>  > (6) sx:=s.1
>  >     (6) "?"                 Type: SingletonAsOrderedSet
>  > (7) member?(sx,t)
>  >     (7) true                Type: Boolean
>  > 
>  > Is this correct? How?
>  > 
>  > (8) sxx:=convert(sx)
>  >     (8) ?                   Type: Symbol
>  > (9) tx := t.1
>  >     (9) x                   Type: Symbol
>  > (10) g:Boolean:= sxx=tx
>  >     (10) false               Type: Boolean
>  > (11) g:= sx = tx
>  >     (11) true               Type: Boolean
>  > 
>  > How do you explain (11) that two items of different type can be equal, and 
> (10),
>  > after conversion to the same type, are not?
> 
> (6) -> variables((3*x+1)::UP(x, POLY INT)).1=variables((3*x+1)).1
> 
>    (6)  x= x
>                                Type: Equation UnivariatePolynomial(x,Integer)
> 

> The reason is that the interpreter thinks (quite rightly) that 
> 
> sx = tx has Type: Equation UnivariatePolynomial(x,Integer)
> 
> and (create()$SAOS)::UP(x,INT) returns x.
> 

Unfortunately, this does not correspond to what I find. I set )set mess bot on
and found that this is not how the interpreter works. Rather it goes this way:

sx which is in SAOS, is first coerced into POLY INT then to UP(x, POLY INT),
then "lifted" to UP(x, INT). tx (in Symbol) is also lifted to UP(x, INT) and
then the two are equality tested, returning true. At no time is Equation
involved.

I then tested this (see attachment at end) and as you can see, it gives a
contradiction to transitivity! (Unfortunately, the contradiction is the only
correct answer!)

So I think this is a bug in the interpreter. Instead of trying to be helpful to
search for an "=" that returns Boolean for the types given on the lhs and rhs,
it should simply first check whether the two sides have the same type and then
whether equality testing "=" exist for that type. No automatic coercion should
be done.

> I started a discussion of (6) in 
> 
> http://page.axiom-developer.org/zope/mathaction/DesignIssues

I am not familiar with using this resource, so I have not posted my reply there.
Please feel free to post this if you like.

On that page, you wrote:
> Maybe it would be possible to somehow query functions provided by packages: 
> after all there is a function
> variables:FRAC POLY INT->LIST SYMBOL, only, it is not provided by FRAC POLY 
> INT but by RF INT...

This is correct. As you have pointed out, the reason is very simple. FRAC is a
general constructor for quotient field of an integral domain, which need not
have [variables]. Perhaps ideally, this should be included with something like:

  if R has POLYCAT(...) or any other similar categories then
    variables: FRAC R -> List Symbol

but unfortunately, this is not easy since the ... in POLYCAT varies with the way
R is constructed. This is the reason why it is put in RF. This may fall under
the "Don't ask, just tell" policy :-). Note that indeed, FRAC UP(x, INT) also
has no [variables] because no one has implemented a UnivariateRationalFunction
package or domain. Similarly for FRAC DMP(...) and others. Because of the
generality that Axiom constructors have, it is very difficult to ask about the
constructors --- unless, for each domain constructor, we provide the functions
that return the parameters and the constructor --- but even that is no simple
thing to do ... lots of catch-22 situations. The safest way is to implement this
in an auxilliary package where one has more control over the parameters of the
polynomial domain. I believe this is the correct design.

You suggested:

> to move the
> operation variables from RF and POLYCATQ to QFCAT : 
> 
>     if S has variables: S -> List Symbol then
>       variables: % -> List Symbol
>       variables f ==
>          mymerge(variables(numer(f)), variables(denom(f)))

As you pointed out, this is not general enough, because there are other domains
with [variables] with the more general codomain LV: List OrderedSet. Ideally,
perhaps we can try:

     if S has variables: S -> List V where V:OrderedSet then
       variables: % -> List V
       variables f ==
          mymerge(variables(numer(f)), variables(denom(f)))

However, I am a bit worried with other integral domains that satisfy the
condition but has nothing to do with indeterminates. Fortunately, there are no
such domains in Axiom at present. So this may be better than the 

    if R has POLYCAT(...) then

construct, testing for existence of a function is ok.

> and add the following to UP and MPOLY : 
> 
>     if R has variables: R -> List Symbol then
>       coerce(r:R):% ==
>         if member?(x, variables(r)) then
>           error "coefficient contains variable"
>         else coerce(r)$Rep

If this coercion is done for UP, MPOLY, then it should also be done for any of
the domains in POLYCAT, since there is now no reason not to have say DMP([x,y],
POLY INT). Any tower construction would be allowed.

There is one problem with the 

    member?(x, variables(r))

condition. If R is EXPR INT, and if x occurs in r say as 1/x or as sin(x), I
would think that variables(r) would have x as a member, and so you would receive
the error message when coerce is called. But according to your intention, you
may still want to coerce r (that is, in my terminology, reformat r) to look like
UP(x, EXPR INT).

BTW, I also just found that you can simply [pun intended] coerce without any new
code to do what you want:

)clear all
q:EXPR INT:=x*sin(x)
p:=q::UP(x, EXPR INT)
degree p
coefficient(p,1)

However, this is not fullproof:
q:=q^2+q+cos(x)
p:=q::UP(x, EXPR INT) -- works fine degree p is 2
q:= p/x
p:=q::UP(x, EXPR INT)
degree p  -- no good degree p is 0

This suggests that the success to such reformatting depends very much on the
data representation.

pn:=numer p
pd:=denom p
p:= (pn::UP(x,EXPR INT))/(pd::UP(x,EXPR INT))
degree p -- no good, degree is 2

More trouble. This is all because the x wears two hats and Axiom does not know
how to simplify them or identify them. Here they were wrongly distinguished. In
the session below, they were wrongly identified.


William
--- Transcript from Axiom session
Starts dribbling to martin2 (Fri Sept 22 22:24:28 2004)

G82322 (4) -> )clear all
   All user variables and function definitions have been cleared.
G82322 (1) -> z:UP(x, POLY INT):=3*x+1

   (1)  3x + 1
                             Type: UnivariatePolynomial(x,Polynomial Integer)
G82322 (2) -> y:POLY INT:=3*x+1

   (2)  3x + 1
                                                     Type: Polynomial Integer
G82322 (3) -> upx:=variables(z).1

   (3)  "?"
                                                  Type: SingletonAsOrderedSet
G82322 (4) -> px:=variables(y).1

   (4)  x
                                                                 Type: Symbol
G82322 (5) -> )set mess bot on
G82322 (5) -> g:Boolean:=(upx = px)

 Function Selection for =
      Arguments: (SAOS,SYMBOL) 
      Target type: BOOLEAN 
   -> no function = found for arguments (SAOS,SYMBOL) 

 Function Selection for =
      Arguments: (SAOS,OVAR [x]) 
      Target type: BOOLEAN 
   -> no function = found for arguments (SAOS,OVAR [x]) 

 Function Selection for =
      Arguments: (SAOS,POLY INT) 
      Target type: BOOLEAN 
   -> no function = found for arguments (SAOS,POLY INT) 

 Function Selection for map by coercion facility (map) 
      Arguments: ((POLY INT -> INT),UP(x,POLY INT)) 
      Target type: UP(x,INT) 
 
 [1]  signature:   ((POLY INT -> INT),UP(x,POLY INT)) -> UP(x,INT)
      implemented: slot (UnivariatePolynomial x (Integer))(Mapping (Integer) (

Polynomial (Integer)))(UnivariatePolynomial x (Polynomial (Integer))) from 

UPOLYC2(POLY INT,UP(x,POLY INT),INT,UP(x,INT))
 [2]  signature:   ((POLY INT -> INT),UP(x,POLY INT)) -> UP(x,INT)
      implemented: slot (UnivariatePolynomial x (Integer))(Mapping (Integer) (

Polynomial (Integer)))(UnivariatePolynomial x (Polynomial (Integer))) from UP2(

x,POLY INT,x,INT)
 

 Function Selection for =
      Arguments: (SAOS,UP(x,INT)) 
      Target type: BOOLEAN 
 
 [1]  signature:   (UP(x,INT),UP(x,INT)) -> BOOLEAN
      implemented: slot (Boolean)$$ from UP(x,INT)
 

   (5)  true
                                                                Type: Boolean

G82322 (6) -> --So Symbol was coerced first to POLY INT then to UP(x, POLY INT),
then polylifted to UP(x, INT), and SAOS was also lifted to UP(x, INT) and then
the equality test from UP(x,INT) is used. Never in here ever was Equation
involved. This result is wrong since I can change x to another symbol and the
result would be the same:

G82322 (6) -> )set mess bot off
G82322 (6) -> w:POLY INT:= 3*t+1

   (6)  3t + 1
                                                     Type: Polynomial Integer

G82322 (7) -> pt:=variables(w).1

   (7)  t
                                                    Type: Symbol
G82322 (8) -> )set mess bot on                                                  
 

              
G82322 (8) -> g:=upx = pt

 Function Selection for =
      Arguments: (SAOS,SYMBOL) 
      Target type: BOOLEAN 
   -> no function = found for arguments (SAOS,SYMBOL) 

 Function Selection for =
      Arguments: (SAOS,OVAR [t]) 
      Target type: BOOLEAN 
   -> no appropriate = found in SingletonAsOrderedSet 
   -> no appropriate = found in OrderedVariableList [t] 
   -> no appropriate = found in Symbol 
   -> no appropriate = found in Boolean 
   -> no appropriate = found in SingletonAsOrderedSet 
   -> no appropriate = found in OrderedVariableList [t] 
   -> no appropriate = found in Symbol 
   -> no appropriate = found in Boolean 

 Modemaps from Associated Packages 
   no modemaps

 Remaining General Modemaps 
   [1] (FortranScalarType,FortranScalarType) -> Boolean from 
            FortranScalarType
   [2] (D1,D1) -> Equation D1 from Equation D1 if D1 has TYPE
   [3] (D,D) -> Boolean from D if D has BASTYPE
   -> no function = found for arguments (SAOS,OVAR [t]) 

 Function Selection for =
      Arguments: (SAOS,POLY INT) 
      Target type: BOOLEAN 
   -> no function = found for arguments (SAOS,POLY INT) 

 Function Selection for map by coercion facility (map) 
      Arguments: ((POLY INT -> INT),UP(t,POLY INT)) 
      Target type: UP(t,INT) 
   -> no appropriate map found in UnivariatePolynomial(t,Polynomial Integer) 
   -> no appropriate map found in UnivariatePolynomial(t,Integer) 
   -> no appropriate map found in Integer 
   -> no appropriate map found in Polynomial Integer 
   -> no appropriate map found in Integer 

 Modemaps from Associated Packages 
   [1] ((D4 -> D5),D3) -> D1
            from UnivariatePolynomialCategoryFunctions2(D4,D3,D5,D1)
            if D4 has RING and D5 has RING and D1 has UPOLYC D5 and D3 
            has UPOLYC D4
   [2] ((D5 -> D7),UnivariatePolynomial(D4,D5)) -> UnivariatePolynomial
            (D6,D7)
            from UnivariatePolynomialFunctions2(D4,D5,D6,D7)
            if D4: SYMBOL and D5 has RING and D7 has RING and D6: 
            SYMBOL
   [3] ((D4 -> D5),SparseUnivariatePolynomial D4) -> 
            SparseUnivariatePolynomial D5
            from SparseUnivariatePolynomialFunctions2(D4,D5)
            if D4 has RING and D5 has RING
 
 [1]  signature:   ((POLY INT -> INT),UP(t,POLY INT)) -> UP(t,INT)
      implemented: slot (UnivariatePolynomial t (Integer))(Mapping (Integer)
(Polynomial (Integer)))(UnivariatePolynomial t (Polynomial (Integer))) from
UPOLYC2(POLY INT,UP(t,POLY INT,INT,UP(t,INT))
 [2]  signature:   ((POLY INT -> INT),UP(t,POLY INT)) -> UP(t,INT)
      implemented: slot (UnivariatePolynomial t (Integer))(Mapping (Integer)
(Polynomial (Integer)))(UnivariatePolynomial t (Polynomial (Integer))) from
UP2(t,POLY INT,t,INT)
 

 Function Selection for =
      Arguments: (SAOS,UP(t,INT)) 
      Target type: BOOLEAN 
   -> no appropriate = found in SingletonAsOrderedSet 
   -> no appropriate = found in UnivariatePolynomial(t,Integer) 
   -> no appropriate = found in Boolean 
   -> no appropriate = found in SingletonAsOrderedSet 
   -> no appropriate = found in Boolean 
 
 [1]  signature:   (UP(t,INT),UP(t,INT)) -> BOOLEAN
      implemented: slot (Boolean)$$ from UP(t,INT)
 

   (8)  true
                                                 Type: Boolean

G82322 (9) -> -- this is also wrong.

G82322 (9) -> )set mess bot off

G82322 (9) -> g:= (px = pt)

   (9)  false
                                                  Type: Boolean

G82322 (10) -> -- This is correct. If (5) and (8) were correct, it should follow
that (9) returns true by transivity: upx = px, upx = pt, hence px = pt.

G82322 (10) -> g:= (px::UP(x,INT) = pt::UP(t, INT))

   (10)  false
                                                  Type: Boolean
G82322 (11) -> -- This is correct; the interpreter puts everything into UP(x,
UP(t, INT)).

G82322 (11) -> )spool

Finished dribbling to martin2.