[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiomdeveloper] Re: equal or unequal (was: Question concerning types..
From: 
Gabriel Dos Reis 
Subject: 
[Axiomdeveloper] Re: equal or unequal (was: Question concerning types...) 
Date: 
18 Sep 2006 13:21:21 +0200 
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 nonequal in other nonsyntactical
 > 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 builtin or library. For efficient reasons, I would
prefer it builtin  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, nonsense 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
 RE: [Axiomdeveloper] Question concerning types..., (continued)
 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/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 <=
 [Axiomdeveloper] Re: equal or unequal, Ralf Hemmecke, 2006/09/18
 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