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

[Martin Rubey]

William Sit writes:

> Martin Rubey wrote:

> > I'm not so sure about "wrong". One (not me...) could argue that the two
> > univariate polynomials 3*x+1 and 3*t+1 are the same. On the other hand, I
> > (!)  would say that this behaviour should be reserved for SUPs.

> Yes, when univariate polynomials are interpreted as functions in the
> mathematical sense, 3*x+1 and 3*t+1 are the same (x, t are dummy variables or
> placeholders for the functions). But this is seldom the interpretation in
> symbolic computation.  Here, we are getting closer to a discussion on what
> "equality" means, a well-understood problem with many possibilities but no
> clear choice that would work for all situations. I am not sure what "this
> behaviour" refers to, or why SUPs are more appropriate.

I mean (using your terminology): 

"interpreting polynomials as functions" -> "use SUPs, please!"

> > And indeed, axiom does say that
> > ((x::UP(x, INT))=(t::UP(t, INT)))::Boolean
> > is false.

> Again, at the risk of being repetitve, be careful here. 

Oops, thank you. I did not really understand. This made it clear to me:

> In the first instance, it looks for a domain T: Type and a signature for
> [equation:(T,T)->Equation(T)], while in the latter, a domain S:SetCategory
> and a signature for ["=": (S,S)-> Boolean].

-----------------------------------------------------------------------

> Equation(T) only needs T:Type. Equation(T) has CoercibleTo(Boolean) if
> T:SetCategory.  I wish Axiom had not overloaded the operator "=" but say used
> "=?" for boolean (indeed, I like it to always use an identifier ending with ?
> for all functions with codomain Boolean). There is really no good reason to
> coerce lhs and rhs to a common S:SetCategory if lhs and rhs are not already
> in the same domain, then they are not equal, period, even if a test for
> equality has not been implemented. Note that lhs and rhs are always evaluated
> (and presumably simplified to $Rep form) before the test. If they do not
> belong to the same domain, why should they be equal in a super-domain? Of
> course, if they do not belong to the same domain (without coercion), no ["="]
> will be found and so no result will be output; but in that case, an error
> message is the correct response (and the error should be trapped via a
> throw/catch mechanism) -- it is like someone writes an *equality* where the
> lhs and rhs does not have the same fundamental dimensions of time, length,
> mass -- it is an error that should be caught. Note that to coerce the lhs and
> rhs to a common domain T to use [equation] would make sense in some cases,
> because after all, we could have written the equation as lhs-rhs=0 if the
> domain T has AbelianGroup and we may want to solve the equation.

I think you are right. When I get to it, I'll set up a MathAction page
summarizing all this.

-------------------------------------------------------------------------------

The following is all under the hypothesis that we want to find valid and clear
semantics for domains like UP(x, EXPR INT). (I believe we do)

> > For any polynomial (or series) domain that has a specified list of
> > variables, I want that axiom ensures that any coefficient of a member does
> > not contain one of these variables. Examples:

> > (1/x)::UP(x, EXPR INT) produces an error
> > x*2^x::UP(x, EXPR INT) produces an error
> > (1/x)::UP(x, FRAC POLY INT) produces an error
> > (1/x)::UTS(FRAC POLY INT,x,0) produces an error

> I am not sure. If UP(x, EXPR INT) is a valid domain (which it is at present),
> then all the above can be regarded as in the ground ring EXPR INT.

Well, this depends on the semantics we want for a domain like UP(x, EXPR
INT). I argue that, *if* we want that something like UP(x, EXPR INT) makes
sense, then the only sane choice is, that the "outermost" domain "takes" all
the variables. Otherwise we will run into trouble sooner or later. Moreover,
I don't see any need for a domain UP(x, EXPR INT) as it is interpreted
currently, i.e., that allows members like 1/x or x*sin(x). 

> > More generally, the "outermost" domain "takes" all the variables.

> In that case, you would forbid expressions like x^2 sin(x) - cos(x)/x in
> UP(x, EXPR INT), where the expression can either be considered as in the
> ground ring EXPR INT, or as a polynomial of degree 2.

Yes. Given x^2 sin(x) - cos(x)/x, no sane mathematician will say that this
could be viewed as a polynomial. Of course, this argument is based on the idea
that x=x, i.e, there shouldn't be different x's in one expression.

> I don't think the second view is necessarily "wrong," just that Axiom at
> present does not do this conversion consistently. I gave some examples where
> the built-in coercions led to inconsistencies in [degree].

I'm pretty sure that it is next to impossible to do this conversion
consistently. For example:

(14) -> x::UP(x, EXPR INT)/x::UP(x, EXPR INT)

   (14)  1
                    Type: Fraction UnivariatePolynomial(x,Expression Integer)
(15) -> x::UP(x, EXPR INT)/x::EXPR INT

         1
   (15)  - x
         x
                             Type: UnivariatePolynomial(x,Expression Integer)

are both completely correct, given the strange semantics of UP(x, EXPR INT).

> > POLY EXPR INT would be the domain of polynomials with coefficients that do 
> > not
> > contain any variables. For example,
> > 
> > (x*sin(2))::POLY EXPR INT would be ok
> > (x*sin(y))::POLY EXPR INT would produce an error.
> 
> Again, I am not sure why the second one should be an error and the first is 
> not,
> if POLY EXPR INT is allowed at all. In both cases, the element may be
> interpreted either as in EXPR INT, or a linear polynomial with coefficient in
> EXPR INT. Neither is mathematically wrong and each is useful. 

I agree that the second example is on the borderline. However, if we were to
allow it, the description of the new semantics of POLY EXPR INT would be
considerably more complicated. (I even doubt that we could find a good 
description)

> The problem is each element may have two different data representations, and
> the[:: POLY EXPR INT] does not say specifically what data representation
> should be used.

I wouldn't think in terms of data representations yet. My credo: First
determine good semantics, then worry about how to implement/represent them.

> We need a clearer way to make the choice. Using a hidden and probably
> unjustified convention that the "outer domain takes all the variables" is
> questionable.

I disagree: I am convinced that this convention is clear. The only other choice
for me would be to depreciate these domains.

> > The domain EXPR POLY INT would be strictly the same as EXPR INT, I think.

> No, we are not talking about mathematics, but data structure. I think we
> agree that the current semantics allowed is ambiguous and for this reason,
> any reformating should be done with specific variables.

I would like to have a mapping from maths to axiom as clear as possible. And
given the convention that the "outermost" domain "takes" all the variables (it
can), EXPR POLY INT and EXPR INT would be the same mathematically, since any
polynomial is an EXPR. Of course, the representations could be different in the
two domains.

-------------------------------------------------------------------------------

I agree on everything you say about expressions with specified variables.


> > ---------------------------------------------------------------------------

I don't have anything clever to say right now about defining a wrapper of
"variables" that has values in Any.

If we want to follow the convention "outermost domain takes all variables it
can" we can simply add a function "variables: % -> List Symbol" to QFCAT (or
wherever it should go), since we only want to test for symbols right now.

Note that only the interpreter catches bogus like UP(x, UP(x, INT)) right
now. It may be an option to change the interpreter rather than the library, but
I think this is the wrong direction to go. BTW: Do you (or anybody else reading
this) know how the interpreter catches this? In fact, it is broken anyway:

(12) -> x::UP(x,UP(x,INT))
 
   UnivariatePolynomial(x,UnivariatePolynomial(x,Integer)) is not a 
      valid type.
(12) -> monomial(1,1)$UP(x,UP(x,INT))

   (12)  x
                Type: UnivariatePolynomial(x,UnivariatePolynomial(x,Integer))

Thus I think the direction to go is to put these checks into the compiler.

> > -------------------------------------------------------------------------
> > 
> > just for the record:
> > 
> > > > I agree, if there remains a clear design. For example, I find the 
> > > > wealth of
> > > > polynomial domains and packages a little confusing:
> > > >
> > > > polycat.spad
> > > > poly.spad
> > > > newpoly.spad
> > > > rf.spad
> >     gdpoly.spad
> >     multpoly.spad
> >     prtition.spad
> >     xlpoly.spad
> >     xpoly.spad
> >     wtpol.spad
> >     ...
> > 
> Wait till we get all the varieties of EXPR (and dare I mention DPOLYCAT or
> DEXPR?)

What would DPOLYCAT or DEXPR be?

Martin