login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit

 Submitted by : (unknown) at: 2007-11-17T23:03:16-08:00 (12 years ago) Name : Axiom Version : default friCAS-20090114 Axiom-20050901 OpenAxiom-20091012 OpenAxiom-20110220 OpenAxiom-Release-141 Category : Axiom Aldor Interface Axiom Compiler Axiom Library Axiom Interpreter Axiom Documentation Axiom User Interface building Axiom from source lisp system MathAction Doyen CD Reduce Axiom on Windows Axiom on Linux Severity : critical serious normal minor wishlist Status : open closed rejected not reproducible fix proposed fixed somewhere duplicate need more info Optional subject :   Optional comment :

> Clearly you're right and I agree with you.
>
> The problem, as I see it, is that there are subtle degrees of meaning
> that are easily stepped around when you work on paper but must be
> clarified in computational mathematics.
Why cannot we allow all?  I expect I should be able to coerce A+1 to
an Integer, Polynomial Integer, Expression Integer, etc.  The default
seems to be Integer, which seems fine.
The error seems to be in the Polynomial domain:
(16) -> c:Complex Integer
Type: Void
(17) -> conjugate(c)            c is declared as being in Complex Integer but has not been given a
value.
(17) -> c:Complex Polynomial Integer
Type: Void
(18) -> conjugate(c)
(18)  c
Type: Complex Polynomial Integer

Adding the Polynomial to its domain causes this to go wrong...
(19) -> c:Polynomial Complex Integer
Type: Void
(20) -> conjugate(c)
There are 4 exposed and 1 unexposed library operations named
conjugate having 1 argument(s) but none was determined to be
...
I'm surprised this doesn't work.  A Polynomial on a Ring is still a
member of that ring and should inherit its functions.  (in this case,
conjugate)  It also strikes me that Polynomial Complex Integer is the
proper type here, not Complex Polynomial Integer...clearly they are
inequivalent.
> A: Integer
>
> might mean that 1) A will hold a value which is an integer
> under interpretation (1)
>
> A+1
>
> is an error since A has no value. But what does the type of
> an unbound thing mean? Lisp assigns types to the values, not
> the boxes. This is like labeling a box television.
This is the approach taken by Integer, Complex, and Float it seems.
> or perhaps that 2) A is an indefinite object of type integer
> under interpretation (2)
>
> A+1
>
> is another indeterminant integer, where + comes from Integer.
>
> or perhaps that 3) A obeys the laws applied to integers
> under interpretation (3)
>
> A+1
>
> is a polynomial with 2 integers, representing a constant, where
> + comes from Polynomial.
I cannot seem to construct an example of type (3).  Given: c:Integer and
I want to construct a Polynomial Integer containing c, how would I do
it?
> or perhaps that 4) A is a symbol which hold integers
> under interpretation (4)
>
> A+1
>
> is a polynomial in A with integer coefficients ignoring 'A's type
> where + comes from Polynomial.
The type of A cannot be ignored since A+1 must Polynomial must have
a Field such as Integer in its constructor.
> or perhaps that 5) A is an element of a Ring and theorems can be applied
> under interpretation (5)
>
> A+1
>
> is B, a new member of the Ring since + is a ring operator and both
> A and 1 are ring elements. Ideally Axiom's types would be decorated
> with axioms, like the ring axioms making reasoning about unbound but
> typed objects possible. The + comes from the Category axioms of Integer.
Now this truly is a research project.  ;)
> The exact interpretation chosen appears to be dictated by the
> underlying code and is not the same everywhere.
>
> Axiom is the product of many people, some of whom have chosen
> different interpretations. Indeed, some of the interpretations
> didn't exist before the computational aspects of mathematics
> came into play.
I think this must be clarified, and a unifying set of assumptions be
applied across all domains.
> There are quite a few areas of research that could be followed.
> Indeed, working out the implications of the several meanings of
> A is a PhD topic, and a rather hard one at that. The issue
> heads off into questions of provisos, questions of reasoning with
> theorems and axioms, etc.
This does not seem so hard, but maybe I am being naive.


On Fri, 28 Jan 2005, Tim Daly wrote:

Hi,

perhaps I miss the point, but I want to comment a few statements:

> The problem, as I see it, is that there are subtle degrees of meaning > that are easily stepped around when you work on paper but must be clarified in computational mathematics.

I wouldn't even call this subtle, but a core problem.

Why cannot we allow all? I expect I should be able to coerce A+1 to an Integer, Polynomial Integer, Expression Integer, etc. The default seems to be Integer, which seems fine.

Why I would have no problem to coerce A to all (anything), I see a problem with the 1, since eg a Ring may not have a 1 and 1 may not even mean unit (of multiplication, eg an additive group)

I'm surprised this doesn't work. A Polynomial on a Ring is still a member of that ring and should inherit its functions.

A polynomial on a Ring is not an element of the Ring! The value of a polynomial on a Ring element is a ring element (not even its roots, and not even limits of polynomials in the dgree may have this property). A polynomial lives (relatively natural) in the product ring RxRxR?... of the ring R, where addition, multiplication etc are inherited canonically. However, one can make RxRx?... in quite different ways into a Ring (and thats needed eg in topology) so AXIOM will need to know what one assumes about this extension.

(in this case, conjugate) It also strikes me that Polynomial Complex Integer is the proper type here, not Complex Polynomial Integer...clearly they are inequivalent.

You shoul be aware that the complex numbers, seen as a field, and the ring C, seen as R-algebra (R real numbers, eg. pairs of real numbers) are not isomorphic objects w.r.t. complex conjugation. Only the R-algebra C has the obvious complex conjugation, while C as a filed has infinitely many inequivalent (non constructive) conmplex conjugations. Hence AXIOM is right to be careful here.

Is this of any help? ciao BF.

% PD Dr Bertfried Fauser % Institution: Max Planck Institut for Math, Leipzig % Privat Docent: University of Konstanz, Phys Dept % contact|->URL : http://clifford.physik.uni-konstanz.de/~fauser/ % Phone : Leipzig +49 341 9959 735 Konstanz +49 7531 693491

property change
Tue, 08 Mar 2005 05:40:58 -0600 reply

this behaviour is well documented --kratt6, Fri, 28 Dec 2007 14:19:30 -0800 reply
Category: Axiom Mathematics => Axiom User Interface Status: open => closed

 Subject:   Be Bold !! ( 15 subscribers )