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

[Gabriel Dos Reis]

Ralf Hemmecke <address@hidden> writes:

| 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,

it certainly isn't, sorry.

| but I very much believe that
| there are situations where one person wants to consider two things as
| equal and another doesn't.

if we are discussing abstract unknown "things" in general, then the
discussion is contentless, as that is symbolic computation issue 101.

However, here you put forward a very specific example.  Which, as far
as I can determine, does not support your claim. 

[...]

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

Ralf, for an integral domain D, Quotient(Quotient(D)) = Quotient(D),
where Quotient is the "quotient field functor".

[...]

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

think "coerce".  Now, a practical issue is whether I would want that
corce to be built-in or library.  For efficient reasons, I would
prefer it built-in -- until systems have progress to the point where
they attain zero abstraction penalty.

Another issue is whether the disction is practically useful.  Here,
opinions vary.


 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?

anyone in any algebra book I've read so far.

| 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? 

dependent types will depend on *values*, not just syntactic objects.
Consequently, when you compare types, you don't just compare them on
syntax, but on their canonical values.
Fraction is idempotent for integral domains.

| You also don't want
| 
| SparseUnivariatePolynomial SparseUnivariatePolynomial Integer
| 
| to be just
| 
| SparseUnivariatePolynomial Integer

what is the connection?

| > | 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?

I would not.  I'm just using the same logic you used to say that
(2/1)/(3/1) is NOT identical to 2/3.

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

that is a weakness, non-sense in the "type system", not anything
fundamentally, and mathematically, meaningful.

Assume you have thaught the system to understand that Fraction is
idempotent on integral domains.  Why would you still have that problem?

| 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?)

Why do you think I would have changed my mind when you scrupulously base
your deduction of partial fragments of what I want?

As I said, I want the system powerfull enough to understand algebraic
properties, in particular idempotency.  Also, think of commuting
constructors, that is another area where you have lot of troubles.

-- Gaby