Re: [Axiom-developer] Am I posing this solve problem wrong?

[Bill Page]

On Mon, May 5, 2008 at 5:31 PM, Ralf Hemmecke wrote:
> ...
>>>
>>> I refer again to what I wrote in
>>> http://lists.gnu.org/archive/html/axiom-developer/2008-05/msg00022.html
>>>
>>> --BEGIN quote
>>> Suppose, I consider the above input expression as an element in R[y]]
>>> where the coefficient domain R is Z[C1,D1,y1,x]. And I would like
>>>
>>>  solve(E1=0,y)
>>>
>>> to stand for "find a (or several) z \in R such that E1[y<--z]=0" where
>>> E1[y<--z] is my (fancy) notation for substitution of y by z in E1.
>>> --END quote
>>>
>>> I have a polynomial E1 in R[y] and I am looking for those z \in R
>>> which make this (univariate) Polynomial vanish. If there are no
>>> such z \in R then Axiom should return an empty list (or empty
>>> set).
>>>
>>
>> Ok, so this is some other form of 'solve' not like those already
>> available in Axiom? Maybe it is something like
>> 'solveLinearPolynomialEquation' in SUP?
>
> I don't think that I meant that. But anyway, I am sure that nobody
> remembers that name when he wants to find a y such that E1=0.
>
>>>> You need Expression in order to include
>>>> kernels involving 'sqrt'.
>>>
>>> I am not looking for the most general expression.
>>
>> Ok. But I thought that was the intention of this thread.
>
> Hmm, the "Subject" does not say anything that "solve" should always
> return the most general solution. If it is the general opinion that a
> function with name "solve" should always return the most general
> solution, I should rather be quiet.
>

I do not know what is the general opinion, but in my opinion all
operations like 'solve' should have a well-defined and fairly simple
relationship to other operations in the same domain.  For example
something like the following should always be true:

    eval(E,solve(E,...))

We should be able to specify the behavior of 'solve' in terms of such
axioms. For example,

(1) -> EQ1:=x+1=0

   (1)  x + 1= 0
                                            Type: Equation Polynomial Integer
(2) -> reduce(_and,[eval(EQ1,s) for s in solve(EQ1)],true)

   (2)  true
                                                                Type: Boolean
(3) -> EQ2:=[x+1=0,y+1=x]

   (3)  [x + 1= 0,y + 1= x]
                                       Type: List Equation Polynomial Integer
(4) -> reduce(_and,concat [map(x+->eval(x,s),EQ2) for s in solve(EQ2)],true)

   (4)  true
                                                                Type: Boolean

And in the case given by Cliff at the start of this thread:

(5) -> E1:EXPR INT := x^2*D1^2+(y-y1)^2*C1^2 - C1^2*D1^2

          2  2      2         2 2     2 2     2  2
   (5)  C1 y1  - 2C1 y y1 + C1 y  + D1 x  - C1 D1
                                                     Type: Expression Integer
(6) -> reduce(_and,[eval(E1=0,s) for s in solve(E1=0,y)],true)

   (6)  true
                                                                Type: Boolean

>>>> Or did you have something else in mind?
>>>
>>> Yep. I was looking for solutions that live in R.
>
>> Ok. A different problem, I think.
>
> It depends. Cliff did not say where he expects the result to live.
>

Yes, therein lies the problem that the Axiom interpreter attempts to solve.

Without additional information Axiom fails:

(1) -> E3 := x^2*D1^2+(y-y1)^2*C1^2 - C1^2*D1^2

          2  2      2         2 2     2 2     2  2
   (1)  C1 y1  - 2C1 y y1 + C1 y  + D1 x  - C1 D1
                                                     Type: Polynomial Integer
(2) -> reduce(_and,[eval(E3=0,s) for s in solve(E3=0,y)],true)

   >> Error detected within library code:
   left hand side must be a single kernel

So I would say that Cliff's initial question was appropriate. Axiom
did something that was unexpected to him. 'solve' returned something
that is not consistent with 'eval'.

>>
>>> Consider the simple equation.
>>>
>>>  x + 1 = 0
>>>
>>> What does "solve for x" actually mean? It is ambiguous.
>>> I would like to say
>>>
>>>  solve(x+1=0, x)$Set(PositiveInteger)
>>>  solve(x+1=0, x)$Set(Integer)
>>>
>>> (or similar) and get different results.
>
> Ooops, I should have written "@Set(...)" above, because I wanted to specify
> the result type. But maybe, it would even be better to give it as an
> argument like
>
>  solve(x+1=0, x, PositiveInteger)
>
> or so.
>

No I think your first idea was correct. It should be possible to
specify the desired output in order to aid the function selection
process. Unfortunately the Axiom interpreter still fails to find the
solution in this case:

(1) -> E3 := x^2*D1^2+(y-y1)^2*C1^2 - C1^2*D1^2

          2  2      2         2 2     2 2     2  2
   (1)  C1 y1  - 2C1 y y1 + C1 y  + D1 x  - C1 D1
                                                     Type: Polynomial Integer
(2) -> solve(E3,y)@List Equation Expression Integer
   There are 20 exposed and 3 unexposed library operations named solve
      having 2 argument(s) but none was determined to be applicable.
      Use HyperDoc Browse, or issue
                              )display op solve
      to learn more about the available operations. Perhaps
      package-calling the operation or using coercions on the arguments
      will allow you to apply the operation.

   Cannot find a definition or applicable library operation named solve
      with argument type(s)
                             Polynomial Integer
                                 Variable y

      Perhaps you should use "@" to indicate the required return type,
      or "$" to specify which version of the function you need.

But of course this works if we give the interpreter enough help...

(2) -> solve(E3::Expression Integer, y)@List Equation Expression Integer

               +----------+                 +----------+
               |   2     2                  |   2     2
            D1\|- x  + C1   + C1 y1    - D1\|- x  + C1   + C1 y1
   (2)  [y= -----------------------,y= -------------------------]
                       C1                          C1
                                       Type: List Equation Expression Integer


>> Well as I said above, by design of the interpreter what actually
>> happens is a consequence of the algorithm that is used to select
>> the appropriate "solve" operation. If I say nothing else, then the
>> interpreter says:
>>
>> (1) -> x+1 = 0
>>
>>   (1)  x + 1= 0
>>                                            Type: Equation Polynomial
>> Integer
>
>> So this is what is uses to begin the process of finding an appropriate
>> version of "solve".
>
>> (2) -> solve(x+1=0,x)
>>
>>   (2)  [x= - 1]
>>                              Type: List Equation Fraction Polynomial
>> Integer
>
> I know that it is not the most simple task for the interpreter to find out
> what the user actually wanted, but you asked my for an ideal AXIOM.
>

Yes, I think this is a worthwhile subject and your comments are quite
appropriate.

It seems to me that like most of Axiom, the Axiom interpreter is built
in a manner which attempts to solve the most general problem rather
than catering to specific requirements or user "whims". The whole
system should be specified by "axiomatically". This applies both to
the underlying system, SPAD compiler, and interpreter as well as the
Axiom library.  I think the idea is to build a tool in which solutions
to specific problems should seem to arise in a natural or even
intuitive manner (once the general design is understood).

I have been thinking specifically about the algorithms that the Axiom
interpreter uses to do type inference and function selection. Some
part of the behaviour is "hard coded" into the interpreter and not
easy to change, but a large part of it depends on interaction with the
design of the Axiom library, i.e. the coercions and other operations
that are exported by exposed domains. It seems to me that in many
cases not enough attention has been paid to "tuning" the Axiom library
so that the Axiom interpreter produces fewer surprises for the new
user.

Regards,
Bill Page.