axiom-developer
[Top][All Lists]

## [Axiom-developer] Re: equal or unequal

 From: Ralf Hemmecke Subject: [Axiom-developer] Re: equal or unequal Date: Tue, 19 Sep 2006 01:24:53 +0200 User-agent: Thunderbird 1.5.0.5 (X11/20060719)

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
(3) -> foo(1$Integer) Compiling function foo with type Fraction Integer -> Boolean (3) false (4) -> foo(1$Fraction(Integer))

(4)  false

)abbrev package RHXPKG RHxPkg

RHxPkg(): with
foo: Integer -> Boolean
foo: Fraction Integer -> Boolean
foo(x: Integer): Boolean == true
foo(y: Fraction Integer): Boolean == false

)clear all
(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.

)abbrev package RHXPKG2 RHxPkg2
F ==> Fraction
Z ==> Integer
RHxPkg2(): with
tst: (Z, Z) -> OutputForm
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)

(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