[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiomdeveloper] Re: equal or unequal
From: 
Ralf Hemmecke 
Subject: 
[Axiomdeveloper] Re: equal or unequal 
Date: 
Tue, 19 Sep 2006 01:24:53 +0200 
Useragent: 
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
)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 builtin or library.
I never want it builtin. 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, nonsense 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
 Re: [Axiomdeveloper] Question concerning types..., (continued)
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 [Axiomdeveloper] equal or unequal (was: Question concerning types...), Ralf Hemmecke, 2006/09/18
 [Axiomdeveloper] Re: equal or unequal (was: Question concerning types...), Gabriel Dos Reis, 2006/09/18
 [Axiomdeveloper] Re: equal or unequal,
Ralf Hemmecke <=
 RE: [Axiomdeveloper] Question concerning types..., Bill Page, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Bertfried Fauser, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 RE: [Axiomdeveloper] Question concerning types..., Bill Page, 2006/09/18
 RE: [Axiomdeveloper] Question concerning types..., C Y, 2006/09/18
 RE: [Axiomdeveloper] Question concerning types..., Bill Page, 2006/09/18