[Axiom-developer] equal or unequal (was: Question concerning types...)

[Ralf Hemmecke]

Hi Gaby,

> | OK, let's turn this into a mathematical example. | | A := Fraction
> Complex Integer; a: A := 1 | B := Complex Fraction Integer; b: B := 1
>  | | Clearly A and be are isomorphic as fields, but they are NOT
> identical.
>
> As syntactic obejcts, no, they are not.  The issue can be rephrased
> as whether they should remain non-equal in other non-syntactical 
> intepretation.   I think no.

Ah, you said it. You have a map inbetween to make things equal, namely
the "interpretation".

Maybe the above is not the best example, but I very much believe that
there are situations where one person wants to consider two things as
equal and another doesn't. They might have different focus. So if you
"design" the two things (like A and B) to be ALWAYS equal, you basically
prevent the second person from finding your CAS appropriate for his work.

> | Not identical in Axiom and not identical in mathematics.

> You have lost me on the last part.  My book says that both A and B
> are the same mathematical object.  Why do you believe they are not?

Let Z denote integer.

Let R denote a ring then C(R), the complex numbers over R is defined as
R[x]/(x^2+1). Let E and I denote the equivalence classes of 1 and x in
C(R) then an element of C(R) can be written as x*E+y*I.

Let R denote a ring without zero divisors. Then Q(R) is defined as
R^2/~ where (x,x') ~ (y,y') :<==> xy'=x'y. The equivalence class of
(x,x') in Q(R) is written as x/x'.

An element in A=Q(C(Z)) looks like (x*E+y*I) / (u*E+v*I).
An element in B=C(Q(Z)) looks like (x/y)*E + (u/v)*I.

(x,y,u,v all elements of Z)

If you now say that you can find two elements of A and B that are
mathematically equal (what does that mean, by the way?), then you
basically try to find a way to make them equal.

If you say that A=B that requires a proof.

A simpler example is Z itself. N is constructed by the peano axioms.
Z = N^2/~ where (m,n) ~ (m',n') :<==> m+n' = m'+n.

By construction, if n\in N then n \not\in Z.

Very often we say something like

  By abuse of notation we identify n and the class  [(n,0)] in Z and
  simply write n\in Z.

I haven't seen any computer algebra system that has addressed such
"abuse of notation". Actually all just abuse the notation and one cannot
do things that where not designed into the system. (It's a different
type of problem, but note how difficult it is to teach Maple or
Mathematica that your * is not commutative.)

> | Note, we had a discussion whether "Fraction Fraction Integer"
> should | be implemented to be the same as "Fraction Integer".

> Under the mathematical interpretation they are the same.

What is THE mathematical interpretation?

I am sure William Sit can elaborate on this.

> I believe they should also be the same in Axiom -- at least if you
> take dependent types seriously.

Could you tell in which sense this has to do with dependent types? You 
also don't want

SparseUnivariatePolynomial SparseUnivariatePolynomial Integer

to be just

SparseUnivariatePolynomial Integer


> | Although I had even given code to do that, I believe it should
> | not be implemented that way. Because an element that looks like
> | (2/1)/(3/1) is NOT identical to 2/3.

> By the same token we should prevent Axiom from simplifying 3+2 to 5.

You are mixing things. Let's suppose 3, 2, 5 are from Integer. Then 
there is +: (Integer, Integer) -> Integer. So we can simply apply that 
function to 3 and 2. Why would you forbid that?

The above is different.

First let's make it equal. If you type (2/1) and (3/1) they are of type 
Fraction Integer. Fraction Integer is a field and allows the operation 
/: (%, %) -> %. So that operation can be applied and yields 2/3.

Now make it different. If I interpret the second / in (2/1)/(3/1) as 
/$Fraction(Fraction Integer) (note that Fraction(S) has an operation 
/:(S,S)->%), then (2/1)/(3/1) is simply an element of 
Fraction(Fraction(Integer)) and is not equal to 2/3 because it has a 
different type.

For some reason the Axiom designers decided to put some knowledge into 
the interpreter which forbids to build "Fraction(Fraction(Integer))".
(But you agreed to put no such knowledge into interpreter or compiler. 
Or do you change your mind now?)

Ralf