The job of a teacher is to teach students the 'right' way to do things. Then, we also teach them to deal with situations where things are done in chaotic, haphazard ways. It seems that you view employees as automatons: obey or else. In the so-called "knowledge industry", that is a good way to have all your good employees quit on you. I used to be in industry, and I have seen bad bosses (who dictate to employees what needs to be done, even when the boss is quite clearly wrong). Result: all the good programmers left, and for the rest, morale was very low. The boss eventually gets turfed too, because of his combined incompetence and the fact that his team is now devoid of talent. My best employees (then), and my best grad students (now) are the ones who tell me right away when I am wrong, and can prove it. That is the only way I know of keeping intelligent and creative individuals productive and happy. And I like it, because it keeps me on my toes. About mathematically correct answers: one of the reasons that Maple does not always return the right answer is that doing so might take too much time, or cripple the overall power too much [or at least, that's the party line]. Axiom and Derive are two examples of computer algebra software more reliable than Maple, and neither survived contact with the marketplace. On the other hand, I have long fought on the side of 'correctness', even if that means losing some efficiency.

Yes, I had not answered that part of your earlier question. But the ideas are the same: if you call solve(x^6-x^4+12,x) twice, how do you know that the problems are related? What if, by chance, they happened to come from independent sources? Then of course the answers are not related, so that arithmetic expressions that involve the two answers should not ``accidentally'' reduce. In other words, if solve(x^6-x^4+12,x) called twice re-used the same labels, then you might think that the answers are *linearly* related, when they are in fact only algebraically related. So different labels need to be generated, because Maple cannot know if the problems are related or not, and it is safest to assume that they are not. On your last point: solve() is called in people's programs, not just in the GUI. So those labels at the right-hand-side, which are pure GUI creations, cannot be used for intermediate results. Something in the language has to be used. So 'label' = unique stamp is used for that purpose.

Yes, I had not answered that part of your earlier question. But the ideas are the same: if you call solve(x^6-x^4+12,x) twice, how do you know that the problems are related? What if, by chance, they happened to come from independent sources? Then of course the answers are not related, so that arithmetic expressions that involve the two answers should not ``accidentally'' reduce. In other words, if solve(x^6-x^4+12,x) called twice re-used the same labels, then you might think that the answers are *linearly* related, when they are in fact only algebraically related. So different labels need to be generated, because Maple cannot know if the problems are related or not, and it is safest to assume that they are not. On your last point: solve() is called in people's programs, not just in the GUI. So those labels at the right-hand-side, which are pure GUI creations, cannot be used for intermediate results. Something in the language has to be used. So 'label' = unique stamp is used for that purpose.

Mathematics is not an absolute, there are various versions of it. Some theorems rely on some axioms (like the axiom of choice, or even the axiom of excluded-middle, if you are a pure constructivist) that are not universally accepted. So it makes no sense to argue mathematics on the basis of "because I say it is". It needs to be done objectively, via proofs. And not "proof by intimidation"... To use a simple example, x^2+1 used to have not solutions (up until roughly first-year university or the middle ages, whichever way you want to see it). Then people discovered the complex numbers, and lo and behold, new solutions! So if the boss was a non-believer in complex numbers and the employee knew about them, who would be right? The same argument can be made about what the 'right' solution to dsolve(x^2*diff(y(x),x) = 0, y(x)); should be. Maple believes y(x)=0 is the right answer. I believe that Dirac(x) is even better. And you know what, Maple will reluctantly agree, ie odetest(y(x)=Dirac(x), [x^2*diff(y(x),x)], y(x)); returns 0. But dsolve does not return that answer, so I could say that it is wrong. We can get fancier and talk about formally divergent series too, which Maple is happy enough to resum in some cases. As to RootOf, think of how to represent the answer (without using labels) to: 1) {x^2=2, y^2=2} 2) {x^2=2, y=x} The problem is that #1 has 4 solutions, #2 has just 2, but it is hard to write the answer down (in RootOf) form without getting these confused. Of course, you can always expand this out with indexes (or in this case with rationals, but I can always ask the same question with degree 5 polynomials with no closed-form).

Mathematics is not an absolute, there are various versions of it. Some theorems rely on some axioms (like the axiom of choice, or even the axiom of excluded-middle, if you are a pure constructivist) that are not universally accepted. So it makes no sense to argue mathematics on the basis of "because I say it is". It needs to be done objectively, via proofs. And not "proof by intimidation"... To use a simple example, x^2+1 used to have not solutions (up until roughly first-year university or the middle ages, whichever way you want to see it). Then people discovered the complex numbers, and lo and behold, new solutions! So if the boss was a non-believer in complex numbers and the employee knew about them, who would be right? The same argument can be made about what the 'right' solution to dsolve(x^2*diff(y(x),x) = 0, y(x)); should be. Maple believes y(x)=0 is the right answer. I believe that Dirac(x) is even better. And you know what, Maple will reluctantly agree, ie odetest(y(x)=Dirac(x), [x^2*diff(y(x),x)], y(x)); returns 0. But dsolve does not return that answer, so I could say that it is wrong. We can get fancier and talk about formally divergent series too, which Maple is happy enough to resum in some cases. As to RootOf, think of how to represent the answer (without using labels) to: 1) {x^2=2, y^2=2} 2) {x^2=2, y=x} The problem is that #1 has 4 solutions, #2 has just 2, but it is hard to write the answer down (in RootOf) form without getting these confused. Of course, you can always expand this out with indexes (or in this case with rationals, but I can always ask the same question with degree 5 polynomials with no closed-form).

As a member of the board of trustees of the Calculemus Network and past (co-)Chair of the Calculemus conference, both of which are dedicated to joining computer algebra and theorem proving, you could say that I definitely a believer. One of my papers (with Bill Farmer and Jeremie Wajs) Trustable Communication between Mathematics Systems gives you a snapshot [in the introduction] of what was available 3 years ago (which has not changed much since). Beyond Maple-PVS, there is also Maple-HOL, Maple-Isabelle, and Maple-COQ. If you look at many papers published in the Calculemus conferences over the years, you'll see that the answer to your last question is undeniably "yes".

The problem here is that the terminology is not well-defined anywhere! There is no single place where one can go and find formal definitions of these various terms (in this case: indexed RootOf, labelled RootOf, what _EnvExplicit really means, etc). So it is impossible to have a proper mathematical discussion, since we don't have proper definitions to start from. As I have taught my Software Engineering students: no spec, no bug. How can something (short of a crash) be considered a bug (incorrect, whatever you want to call it), if there is no specification against which you can check the expected behaviour? Fuzzy specifications (like solve's help page) do not really help there either. Just for fun, we could try: what should 'solve' do? What is the input-output relation called 'solve'?

The problem here is that the terminology is not well-defined anywhere! There is no single place where one can go and find formal definitions of these various terms (in this case: indexed RootOf, labelled RootOf, what _EnvExplicit really means, etc). So it is impossible to have a proper mathematical discussion, since we don't have proper definitions to start from. As I have taught my Software Engineering students: no spec, no bug. How can something (short of a crash) be considered a bug (incorrect, whatever you want to call it), if there is no specification against which you can check the expected behaviour? Fuzzy specifications (like solve's help page) do not really help there either. Just for fun, we could try: what should 'solve' do? What is the input-output relation called 'solve'?

is() checks that certain properties, via doing some computations, appears to hold. For most bugs in Maple, I can transform that into a usage of is() that would ``show'' that 0=1. Furthermore, is() does not return a proof, but just true/false/FAIL, which is rather unsatisfactory, no? Useful, often, yes. But not a 'proof'. On top of that, you don't know which axioms is() uses, nor what deduction rules; how would you then know that it is ``proving'' a theorem of the theory you are interested in?

Stephen's post really hits the major notes. I just want to add a few items. Quite surprisingly, the two big ``formal'' activities of mathematics, namely computing and proving, have led to completely different sets of software. On the one hand, there are computer algebra systems (with the best example being Maple, naturally), and on the other various theorem provers. My favourite introduction is by my friend F. Wiedijk: The seventeen provers of the world. What is different about these 17 pieces of software? Two things: 1) they are essentially bug-free, and 2) they are astonishingly difficult to use. And, generally speaking, they can't "compute" much, certainly not in the sense of what Maple can compute. Logicians really really care that every theorem that they prove is in fact true, so they care a lot about correctness; they are willing to suffer through a lot of things to guarantee that. Since from false assumptions you can prove anything you want, any single tiny bug renders a theorem prover completely useless for its task. Maple has bugs [many documented on this very site] (hearsay: Mathematica has more). I know of a number of different ways to get Maple to ``show'' that 0=1. On the other hand, Maple is usually correct. And it is quite usable. In fact, Maple is very usable for that third mathematical activity which I have not talked about yet: exploration. This is where you have a problem you wish to understand better, and so you use (mathematical) tools to 'poke' at it, in different ways. Maple is very very useful for that. The theorem provers, pretty much hopeless at that task.

Yes, the output with many different labels is an issue here. There were proposals to return the full answer, or at least an easy way for the user to ask for that. But at the time the powers-that-be vetoed that, because that would cause simple polynomials to come out with big answers. Who would want 18 identical-looking RootOfs (with different 'index'es) when just 2 nested RootOfs could encode the same thing? The question is actually quite deep: what is the proper mathematical specification for 'solve'? I mean, what exactly is its input, and what exactly is its output? However, on your last question (implicit vs explicit), the answer is still 'implicit': it is easier to ``label'' various RootOfs with numerical approximations to the roots (ie good enough approximations that a Newton's method would be guaranteed to converge) rather than using 'explicit' forms. Once the roots are uniquely identified, then figuring out which are real, and which are in which part of the complex plane, is not so difficult. Doing the same with explicit forms is actually much much harder, because the usual formulas found in textbooks are astonishingly ill-behaved. The Maple library makes moderate use of labelled RootOfs. It was a controversial feature that never fully caught on.

Yes, the output with many different labels is an issue here. There were proposals to return the full answer, or at least an easy way for the user to ask for that. But at the time the powers-that-be vetoed that, because that would cause simple polynomials to come out with big answers. Who would want 18 identical-looking RootOfs (with different 'index'es) when just 2 nested RootOfs could encode the same thing? The question is actually quite deep: what is the proper mathematical specification for 'solve'? I mean, what exactly is its input, and what exactly is its output? However, on your last question (implicit vs explicit), the answer is still 'implicit': it is easier to ``label'' various RootOfs with numerical approximations to the roots (ie good enough approximations that a Newton's method would be guaranteed to converge) rather than using 'explicit' forms. Once the roots are uniquely identified, then figuring out which are real, and which are in which part of the complex plane, is not so difficult. Doing the same with explicit forms is actually much much harder, because the usual formulas found in textbooks are astonishingly ill-behaved. The Maple library makes moderate use of labelled RootOfs. It was a controversial feature that never fully caught on.

But then how do you compute the set R? I guess a remove call on the original set? You are still doing 2 full traversals, but the intermediate memory allocations might be smaller. Worth a try.

If you dig into allvalues enough (ie `allvalues/rootseq`), you'll see that it 1) duplicates some code from solve, and 2) calls solve. allvalues itself plays around with _EnvExplict. My hunch is that there are no real advantages one way or another -- that one can come up with test cases to justify either. Having said that, in my experience, implicit representations are more computationally effective, so that I would lean towards using _EnvExplicit := false ! Explicit answers are mostly for show. There are definitely routines in Maple which set _EnvExplicit (sometimes to false by the way). I don't remember offhand which they were.

If you dig into allvalues enough (ie `allvalues/rootseq`), you'll see that it 1) duplicates some code from solve, and 2) calls solve. allvalues itself plays around with _EnvExplict. My hunch is that there are no real advantages one way or another -- that one can come up with test cases to justify either. Having said that, in my experience, implicit representations are more computationally effective, so that I would lean towards using _EnvExplicit := false ! Explicit answers are mostly for show. There are definitely routines in Maple which set _EnvExplicit (sometimes to false by the way). I don't remember offhand which they were.