[Axiom-developer] Re: equal or unequal

[Ralf Hemmecke]

On 09/18/2006 01:21 PM, Gabriel Dos Reis wrote:
> Ralf, for an integral domain D, Quotient(Quotient(D)) = Quotient(D),
> where Quotient is the "quotient field functor".

If = means "are isomophic as fields" then I agree. If = means 
"identical" then I don't agree. I don't even agree that it exists *THE* 
"quotient field functor". A lot of things in mathematics are "equal" up 
to isomorphism. Whether a person wants to see something as equal or not 
very much depends on his/her focus.

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

In Axiom I can say

z: Integer := 1
q: Fraction Integer := 1
b: Boolean := z = q

in SPAD I would have to say

b: Boolean := (z :: Fraction(Integer)) = q

for the last line.

So in some sense Axiom addresses this "abuse of notation" issue.
And it "supports" it by forbidding me to define two functions

---BEGIN aaa.input
foo(x: Integer): Boolean == true
foo(y: Fraction Integer): Boolean == false
---END aaa.input

)clear all
)read aaa.input
(3) -> foo(1$Integer)
   Compiling function foo with type Fraction Integer -> Boolean

   (3)  false

(4) -> foo(1$Fraction(Integer))

   (4)  false


Whereas SPAD allows it.

---BEGIN bbb.spad
)abbrev package RHXPKG RHxPkg

RHxPkg(): with
  foo: Integer -> Boolean
  foo: Fraction Integer -> Boolean
 == add
  foo(x: Integer): Boolean == true
  foo(y: Fraction Integer): Boolean == false
---END bbb.spad

)clear all
)co bbb.spad
(1) -> foo(1$Integer)
   Loading /home/hemmecke/scratch/RHXPKG.NRLIB/code for package RHxPkg

   (1)  true

(2) -> foo(1$Fraction(Integer))

   (2)  false

So, that is an instance of where the interpreter give different results 
than the code that SPAD compiles.
(BTW, is it possible to do without wrapping the functions by a package 
in the SPAD code?)

> Now, a practical issue is whether I would want that
> corce to be built-in or library.

I never want it built-in. Only the interpreter could be allowed (as it 
is now) to apply certain coercions.

> | What is THE mathematical interpretation?
>
> anyone in any algebra book I've read so far.

Interesting that some mathematicians think that 0 is a natural number 
and some don't. But maybe you apply an indeterministic interpretation 
function. ;-)

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

Hopefully, the programmer who implemented Fraction knew that.

---BEGIN aaa.spad
)abbrev package RHXPKG2 RHxPkg2
F ==> Fraction
Z ==> Integer
RHxPkg2(): with
  tst: (Z, Z) -> OutputForm
 == add
  tst(a: Z, b: Z): OutputForm ==
    p: F Z := a/3
    q: F Z := b/7
    ffz: F F Z := p / q
    ((numer ffz) :: OutputForm) / ((denom ffz)::OutputForm)
---END aaa.spad

)co aaa.spad
(1) -> tst(1,2)

         7
         -
         6
   (1)  ---
         1

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

It is not the same logic. The / in the middle of (2/1)/(3/1) is a 
different function from the other two /. I am sure you have heard of 
operator overloading.

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

OK. We disagree.

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

If the system knew that Fraction were idempotent, then no problem. But 
see the code in RHXPKG2. Fraction in the Axiom library code is not 
idempotent.

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

Are we discussing system matters or personal issues?

Ralf