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

[Martin Rubey]

Dear William,

hope I'm not annoying you...

William Sit writes:

 > I am again pressed for time, but many of your questions were answered in my
 > previous email, which probably crossed with yours.

yes indeed...

 > 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:

[...]

 > 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 
[the domain] 
 > Equation involved.

You are quite right. My fault.

 > This result is wrong since I can change x to another symbol and the result
 > would be the same:

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. And indeed, axiom
does say that

((x::UP(x, INT))=(t::UP(t, INT)))::Boolean

is false. 

 > 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'm very unsure about this. Note that when you look at the corresponding EQ
types (if you do not coerce to Boolean), everything looks sane. I do understand
that the domain EQ is not involved when you do ask for a boolean immediately,
but I wouldn't hurry here.

 > > 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.

I will update the page from time to time. I think that discussing all this via
mathaction would produce to much noise...

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

It seems that there is a fundamental misunderstanding concerning my intention
with regards to the semantics of UP(x, POLY INT). You wrote

 > 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).

In fact, an error message is exactly what I'd like to see for 
(1/x)::UP(x, EXPR INT).

I try to get it right now: (It may be that my current position differs from
that I had some months ago, but it was constant in the last few weeks. Save I
made a mistake)

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

however, for example

x*2^y::UP(x, EXPR INT) is ok.

More generally, the "outermost" domain "takes" all the variables:

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.

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

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

However, currently this seems unachievable. At least I don't know how to do
it. Your suggestion to extend axiom to allow

 > 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)))

seems most appealing to me, although I don't think this could be done in the
near future. I read a bit about the "post-facto" extensions provided by aldor,
maybe they adress this problem too. I'm not sure that I've understood them well
enough, though.

PS: In fact, I can think of a way to do it: provide a function 
variables2: % -> List Any in POLYCAT that simply wraps up the function 
variables:% -> List VarSet.

Then I can provide a function variables2 in QFCAT. The only tricky part is that
I need the operation "<" from VarSet in QFCAT (for mymerge) and I don't know of
a *good* way to get it. I do know an ugly way: provide a function 
(Any, Any)->Boolean in POLYCAT that wraps "<" from VarSet.

Maybe there is a better way, but I'm tired now.

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

On the other hand, there is a completely different solution to the original
problem, i.e., providing a domain like UP(x, EXPR INT) with good semantics:

> > Yes. I'm inclined to think that this is the best way to go: create a domain
> > EXPR(VarSet, CoeffSet) and forbid all of the above constructions: UP(x, POLY
> > ?), UP(x, FRAC POLY ?), UP(x, EXPR ?) and so on...
> 
> Good. I am glad we are beginning to agree. However, your point of creating
> something like sin(2) x somewhere should be considered carefully.

sin(2)*x would be in UP(x, EXPR([], INT)). Did you mean that?

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

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
    ...

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

> I am more confused than you are. You have taught me to look into things I 
> never
> knew. See what I mean that 70% of time in Axiom is in coercion? If I weren't
> conservative, I'll say 90%. That is the curse of strong typing.

You are flattering me...

Martin