Francois Maltey <[EMAIL PROTECTED]> writes:
| Gabriel Dos Reis wrote :
| > It probably is difficult because you have consistantly avoided to
| > tell me what the definition of equality of function is, so that I
| > check that the implementation does not something sensible.
| >
| I hope that (at least one of the) axioms could propose
| (a) a practical
| (b) determinist code,
| (c) not a decidable code.
|
| (a) : very often this call will be over calculus (exact or float or
| expressions...)
| and this reduce will work for the extreme case for sum or product void.
Dear Francois,
There is no ambiguity -- at least in my mind -- that reduce should
be supported in an algebraic system.
The discussion had been on a largely orthogonal issue. How equality
of functions is defined should, in principle, have no bearing on
reduction of monoid operations over a sequence.
[...]
| With my naive understanding 2 functions with the same name and the same
| signature are equal because the result is the same. We can suppose that
| axiom doesn't change the definition of a function between the left hand
| side and the right hand side of the equal in f=g
The fundamental problem with equality is not that it does not say x=x.
Its problem is that it is a binary decision. Answering `yes' may have
as much impact as answering `no'. If the equality test says `no',
what is the computational consequence that should be drawn?
Ideally, reduction of monoid operation should not have anything to do
with pointer equality semantics. That some proposes it has means that
we do not quite understand what it is to be fixed.
| (b) :I use too often maple and I really want a proved? determinist code.
| Either the = is always right or is always wrong, but never the test is
| fuzzy.
That is where the problem cripples in. Binary answer. James
Davenport has an excellent paper on the notion of equality in computer
algebra that I would encourage interested people to consider seriously:
"Equality in computer algebra and beyond"
Source
Journal of Symbolic Computation archive
Volume 34 , Issue 4 (October 2002) table of contents
Integrated reasoning and algebra systems
Pages: 259 - 270
Year of Publication: 2002
ISSN:0747-7171
Author
James H. Davenport Department of Computer Science, University of
Bath, Bath BA2 7AY, U.K.
Publisher
Academic Press, Inc. Duluth, MN, USA
No wonder why Lisp has so many equality operators. To offer a quote
(no category theory) that goes to the heart of the concrete matter:
Equality is fundamental in mathematics. As we come to encode
mathematical computation in computer algebra systems or in
automated reasoning systems, we have to define, sooner or later,
precisely what we mean by equality. Although computer algebra dates
back to 1953, the first real discussion of the meaning of equality in
computer algebra seems to have been published in 1969 (Brown,
1969). It is still often necessary to apologize for the apparent
difficulty of equality: Steel (2002) say “Amazingly, testing whether
an element is the zero element of the field turns out to be the most
difficult operation in the whole scheme!”
In practice, computer algebra systems often do not define what their
various meanings of equality actually are. To be fair, there are
also several ambiguities in the mathematical definition of
equality. For example, we refer to Q(x) as “rational functions”,
even though x^2−1/x−1 and x + 1 are not equal as functions from R
to R, since the former is not defined at x = 1, even though they
are equal as elements of Q(x).
The aim of this paper is to point out some of the problems, both with
mathematical equality and with data structure equality, and to
explain how necessary it is to keep a clear distinction between the
two. We conclude by pointing out that, unless algebra system
designers make it clear what their definition(s) of equality are,
interoperability between computer algebra systems and automated
reasoning systems will be difficult and error-prone.
[...]
All I have been trying to get Bill to is to have him spell out his
definition of equality that can be algorithmically defined and
mathematically evaluated. I hope he would eventually appreciate my
invitation.
| (c) I understand that the test can't be perfect (as tests over floats,
| equal for real, stream, series, and so.) So a partial equal like a eq in
| lisp will be enough.
Equality of function is undecidable in full generality. It does not
mean nothing can be done. It means that unless a specific, clearly
articulated restriction is put forward -- that can be tested by
scientific methodoloies -- we have an ill-defined problem and all we do is
playing games with hacks, superstition, etc.
| A perfect code should only recognize that the anonymous functions
| (x,y) +-> x+y, (x,y) +->y+x and +$TheRightDomain are equal.
That one is easy, and does not need a perfect algorithm for function
equality :-)
-- Gaby
-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Don't miss this year's exciting event. There's still time to save $100.
Use priority code J8TL2D2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
