Bill Page <bill.p...@newsynthesis.org> writes: | On Tue, Jun 23, 2009 at 12:35 AM, Gabriel Dos Reis wrote: | > | > I have been thinking about your patch for a while. As I said | > in the bug audit trail, I fully agree that the bug originates from | > explogs2trigs. However, the more I think about it, I more I | > become undecided what the proper fix should be -- this is not | > a criticism of your patch, I really just don't know the actual fix | > should be. For several reasons. | > | | Great. Thanks for passing on your thoughts. I also have doubts some of | which I have also recently discussed with Waldek on the FriCAS list. | | > First, assuming the the operation makes sense, there is an | > immediate issue of branch cuts -- the decision has to be made | > and done consistently across the symbolic and numeric spectrum, | > otherwise this is just a disaster waiting to happen and most likely | > harder to debug. To get branch cuts done effectively, we would | > need to propagate properties about (symbolic) expressions that | > we currently do. | > | | I think that deciding on branch-cuts is in general an unsolvable | problem. What is needed instead is some convenient method for
Branch cuts for definite numeric values and constructive reals is decidable. Branch cuts in general is undoable without further propagations of the properties of the expressions. | specifying branches. At the moment I favor the view that multi-valued | functions ought to be defined with signatures like the following: | | sqrt: Union(pos:Float,neg:Float) -> Float | | and then I would have to write: | | sqrt(neg 9.0) | | indicating the negative branch, to obtain | | -3.0 | | where 'pos' and 'neg' are injections into the Union. Of course Union | doesn't actually work like that but see for example | http://axiom-wiki.newsynthesis.org/SandBoxSum . Unions of this kind | should be viewed as an abstraction of a kind of "manifold". In the | Complex domain sqrt would be viewed as holomorphic map between such | manifolds. I know you like Unions a lot -- and you know I believe we should do without them when we can. I believe that is not a debate we solve today or tomorrow or even after tomorrow. So, the question is where do we go from there? | Of course this might not be viewed as "convenient" by most people and | we would need a convention that allows the interpreter to | automatically choose a coercion based on the 'pos' injection. In | library code however we would be stuck having to do it the hard way. | | But this is (obviously) still only a half-baked idea. | | > Second, the expression '%i' currently has type defaulted to | > Complex Integer -- this is a pure hack in the interpreter because we | > do not have true polymorphic type in the system yet, but this is a | > debate I do not want to have now; that was just an observation. | | Ok, I suppose you mean that it's type should be something like | 'exists(R,IntegralDomain).Complex(R)' without actually saying exactly | what domain R stands for? No, not really. I meant that in math, when we say the imaginary quantity `i', we don't mean the imaginary quantity from Gaussian integers. Rather, what we want to say is that quantity in any complex ring of fields such that i^2 = -1. In OpenAxiom, that is expressed by the operation: imaginary: () -> R ++ imaginary() = sqrt(-1) = %i. in the category ComplexCategory. That operation is reported by the database as )di op imaginary [1] -> D from D if D has COMPCAT D1 and D1 has COMRING which is just another notation for forall (D: CommutativeRing) . imaginary: () -> D that is a (qualified) polymorphic type. Note that while the library really wants '%i' to be a polymorphic constant (as intended in math), the interpreter is currently defective in that it does not have the same capability to handle polymorphic types (yet). Consequently, a hack was introduced in the interpreter so that '%i' is defined macro that expands to 'complex(0,1)', and crossing fingers that somehow wih enough coercions, things would just magically work out. Sometimes, the magic works. Sometime it doesn't. Ideally, the type of '%i' should be forall(D: CommutativeRing) . Complex(R) as intended by the library. | But the interpreter also says: | | (1) -> 1 | | (1) 1 | Type: PositiveInteger | | which surely is a similar "hack". Two wrongs don't make a right. I never said that wasn't a hack. | The point being that the interpreter | will also freely choose coercions which make this choice the obvious ^^^^^^^^^^^^^^^^^^^^^^ | kind of "minimal assumption" from which other types are derived as ^^^^ This is where we get surprises: things are not as obvious as they look. | required by the function selection algorithm. Similar coercions exist | for Complex Integer. | | It is not obvious to me how a "true polymorphic type" should interact | with such coercions. Your seem to suggest that 'polymorphic type' are not already the foundation of Spad -- if that impression is true, then I'm surprised you believe that. Polymorphic types are there, and are the foundation of the Spad type system; that is not going to go away. How polymorphic types interact with coercions is obvious in the compiler. That interaction is not obvious in the interpreter, and that is why so few people (if any) actually understands the coercion mechanism in the interpreter AND can explain it succinctly from first principles. And, that is also why people get so confused by the operation selection process -- there is almost no coherent set of first principles, only ad hoc short-cuts. | | > Now, what should be the domain of sqrt(%i)? Surely, it cannot be | > Complex Integer. The choice of Expression Complex Integer, in my | > opinion, is over-reaching -- Expression T is at the current state a sort | > of 'black hole' that tends to attract everything and we not know yet | > how to effectively handle expressions of such type. | | Agreed, although perhaps it is not quite that bad. | | > Complex AlgebraicNumber? Or Complex of an extension of | > Fraction Integer by sqrt(2)? In each case, why not? | > | | Complex AlgebraicNumber? | | No, because | | (1) -> sqrt(-1)::Complex AN | | Complex AlgebraicNumber is not a valid type. But that does not answer why that is wrong. It only says what the current system (which has many bugs) says. That does not explain why it should be incorrect. | but we already have: | | (1) -> q:= sqrt(sqrt(-1)) | | +---+ | \|- 1 + 1 | (1) ---------- | +-+ | \|2 | Type: AlgebraicNumber | | The problem is that %i is not sqrt(-1) in this domain. That is what the implementation says. We should not just trust it. We should seek the (computationally) mathematically correct answer and then confront the implementation. | Complex of an extension of Fraction Integer by sqrt(2)? Well, after all, many integration algorithms have to consider extensions of QQ with some radicals. And those may contain %i. | Maybe something like this? | | (1) -> S:=Complex SAE(FRAC INT,SUP FRAC INT,x^2+2) | | (1) | Complex SimpleAlgebraicExtension(Fraction Integer,SparseUnivariatePolynomial | Fraction Integer,+?*?2) | Type: Domain | | But support for using SimpleAlgebraicExtension in this way seems | rather poor. Agreed. But, again, my question is what should be the mathematically correct answer -- not what the implementation currently says. If the mathematically correct answer requires better support, then what does it take to make it work. If the price is too high, then we may want to document the short cut and apologize. Otherwise, maybe it is worth the efforts? | This was the best I could manage to come up with in the | current version of OpenAxiom: | | (1) -> S:=SAE(FRAC INT,SUP(FRAC INT),x^2-2) | | (1) | SimpleAlgebraicExtension(Fraction Integer,SparseUnivariatePolynomial Fraction | Integer,+?*?-2) | Type: Domain | (2) -> sqrt(2)==generator()$S | Type: Void | (3) -> sqrt(2)^2 | | (3) 2 | Type: SimpleAlgebraicExtension(Fraction | Integer,SparseUnivariatePolynomial Fraction Integer,+?*?-2) | | (4) -> p:=(%i::Complex(S)+1)/sqrt(2) | | 1 1 | (4) - ? + - ? %i | 2 2 | Type: Complex SimpleAlgebraicExtension(Fraction | Integer,SparseUnivariatePolynomial Fraction Integer,+?*?-2) | | (5) -> p^2 | | (5) %i | Type: Complex SimpleAlgebraicExtension(Fraction | Integer,SparseUnivariatePolynomial Fraction Integer,+?*?-2) | | (6) -> (p^2)::Complex EXPR INT::Complex INT | | (6) %i | Type: Complex Integer | | --- | | With a lot of work this might be made more transparent. Can we really | avoid the "black hole" this way? That is some of the question I would like to have answers for. Is it the mathematically correct answer? Does it scale? What are the alternatives? What are the costs? Can we do it in way that requires less plumbing? -- Gaby ------------------------------------------------------------------------------ Are you an open source citizen? Join us for the Open Source Bridge conference! Portland, OR, June 17-19. Two days of sessions, one day of unconference: $250. Need another reason to go? 24-hour hacker lounge. Register today! http://ad.doubleclick.net/clk;215844324;13503038;v?http://opensourcebridge.org _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
