[Axiom-developer] Re: [Axiom-mail] complex numbers

[root]

> On Wednesday, December 29, 2004 2:28 AM you wrote:
> > 
> > seems to be a categorical error of some sort.
> > 
> > A: Complex Polynomial Integer
> > 
> > tells the system that 'A' is expected to have a value which is
> > Complex Polynomial Integer.
> > 
> > 'conjugate' works on values, not potential values.
> > 
> > Thus, conjugate(A) has no meaning as 'A' has no value.
> > This should probably be an error.
> > 
> > If axiom could work with so that conjugate worked on the type
> > then axiom could work at some sort of an 'axiomatic' level
> > rather than a symbolic computation level. Perhaps when we join
> > forces with the ACL2 crowd we could state certain theorems and
> > have them applied in the absence of a value.
> > 
> 
> I know that this is opening up the whole big subject again,
> but I do think that Axiom is already "two-faced" about this.
> 
> Consider for example that we can write:
> 
> (7) -> A: Complex Polynomial Integer
>                                          Type: Void
> (8) -> B: Complex Polynomial Integer
>                                          Type: Void
> (9) -> A+B
> 
>    (9)  B + A
>                                Type: Complex Polynomial Integer
> 
> Neither A or B "has a value" but Axiom has no trouble agreeing
> that A+B is still of type Complex Polynomial Integer.
> 
> I do not see any essential difference between this and
> 
> (10) -> A:Integer
>                                          Type: Void
> (11) -> B:Integer
>                                          Type: Void
> (12) -> A+B
> 
>    A is declared as being in Integer but has not been given a value.
> 
> 

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.

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'.

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.

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.

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.


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.

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.

Axiom's main strength has always been as a research platform where
it is possible to work out these ideas and reduce them to practice.

Unfortunately, research funding seems nowhere to be found.

Tim