Bill Page <bill.p...@newsynthesis.org> writes:
| On Tue, Jun 23, 2009 at 5:24 AM, Gabriel Dos Reis wrote:
| > Bill Page <bill.p...@newsynthesis.org> writes:
| >
| > 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.
|
| But what guarantee is there that this specification is sufficient to
| uniquely determine 'i'?
What do you mean by 'uniquely'?
We all know that an extension is unique up to its automorphism.
| > 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.
|
| Ok.
|
| > 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).
|
| So what I now understand you to be saying is that you would expect the
| interpreter to be able to perform function selection on the output of
| unary functions (or constants) - something that it does not do now.
somehow, yes.
| Given 1+%i, it would not be looking for coercions from
| PositiveInteger and Complex(Integer) to types that export +, but
| rather finding a solution for the types of functions 'one',
| 'imaginary' and '+' that make this expression type-correct. E.g.
|
| one()@Complex(Integer) + imaginary()@Complex(Integer)
|
| Right?
Almost. The system would interpret 1 + %i as finding an operation
+ that takes
forall(D: Monoid) . D
forall(R: CommutativeRing) . Complex(R)
and gives the result as a constant of type
forall(R: CommutativeRing) . Complex(R)
Note that Complex(Integer) is just one instantiation of that type.
This machinery is essentially known to people doing qualified
polymorphic types (which Spad categories are). However, more work
need to be done to adapt it to the interpreter.
| > ...
| > | 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.
|
| No I did not mean to suggest that.
OK, I'm relieved to read 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.
|
| That is exactly what I meant.
|
| > 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.
| >
|
| So do you think that the interpreter can manage entirely without
| "automatic" coercions and rely only on polymorphism? If not, what
| process would have priority?
I do not know. But, I do think that we need to get the interpreter
follow first principles, and where it can't (there always be such cases,
otherwise we are sure to get to solve undecidable problems) then we must
clearly document ad hoc solutions that we will push toward more
principled explanation. Yes, if it sounds `research', it is because it
is :-) There are lot of mathematical insight that can tip the balance
one way or the other make push make decisions that has been made
differently in other communities facing similar problems.
| How will the interpreter resolve ambiguities if there are no built-in
| assumptions about which types are basic. If I write just
|
| imaginary()
|
| Should the interpreter silently select imaginary()$Complex(Integer)
| over imaginary()$Complex(Float) or complain?
Why? That is committing to a decision before knowing all the facts.
After all, if I'll be computing in Complex(K) where K is some
field that contains all values that I'll need in my calculations
(e.g. sqrt(%i)), then an informed premature choice has been made.
|
| > |
| > | > 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
| > | ...
| > | 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.
| >
|
| What I mean is that sqrt(-1) is multi-valued but %i is not. There is
| no unique way to interpret sqrt(-1) as %i.
sqrt(-1) is no more or no less `multi-valued' than %i. Both designate
the same thing: one of the solutions of the equation %i^2 = -1. Once a
choice is made, one should consistently stick with that choice;
otherwise madness happens.
| > | 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.
| >
|
| Right.
|
| > | 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?
| > ...
| > |
| > | 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?
| >
|
| It is not clear to me in what way a domain like S above would be
| superior to EXPR Complex INT. Is it because in S there is no way to
| express sqrt(-1) except as %i?
No, it is because we don't know what EXPR Complex INT is.
| But there is no way to express sqrt(%i)
| either ... Where do we go from here?
|
| Perhaps as Waldek suggests it is necessary to choose a particular way
| of handling complex muli-valued functions such as assuming that all
| such functions in Expression are holomorphic in spite of the
| unpleasant fact that analytic continuation means functions like 'imag
| sqrt(%i)' are complex-valued. On the other hand perhaps there are
| partial solutions that do not yet such unexpected behavior?
multi-valued functions are just one aspect of the problem. They don't
really make the problem go away, e.g. what is the mathematically correct
answer (including the type of the answer?)
-- 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
