Gaby,
I feel much better having read this reply to Francois since you
explain in a straight forward manner what you are trying to get me to
do instead of just issuing challenges. That seems like a much more
pleasant manner in which to proceed. :-)
>
> Francois Maltey who writes:
On Wed, Apr 9, 2008 at 4:28 PM, Gabriel Dos Reis replied to:
>...
> 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.
>
Yes I agree completely. The issue for 'reduce' is how to identify
those monoid operations and the associated identities. One (imperfect)
way is
if S has Monoid and (f=_*)$Mapping(S,S,S) then ...
You might ask why does the function '*' appear explicity in this
approach. The answer has to do with how monoids are currently
represented in Axiom. '*' is just the name of the monoid operation in
Monoid. Similarly '+' is the name of the monoid operation in
AbelianMonoid. But checking just for these names is not sufficient
since the same name can be used for entirely different functions in
the same domain provided that they have *different signatures*. As it
often happens, Integer for example belongs to both of the above
mentioned monoid categories, i.e. it is a monoid in more than one way.
So just knowing the domain is not sufficient either. And worse, in
Axiom there are many other domains that have monoid operations but do
not belong to either of these categories. This is what Martin has
called the "monoid problem" in Axiom but it is a general feature of
the current Axiom library affecting other domains and categories as
well.
In Axiom the structure that represents a function includes both it's
name and it's signature. As I understand it, the equality (=) in the
Mapping domain currently compares these structures that describe
functions rather than the functions themselves (which in general is
much harder). When I have used the phrase "syntactic equality" in
previous emails it is this comparison of structures that is performed
by the Lisp EQ function to which I refer. I think the this definition
is sufficient for the purposes of defining 'reduce' and many other
things that we might want to do in Axiom. But of course this is not
the "smallest" equivalence relation possible on a collections of
functions and so technically it is *not* actually an "equality".
> ...
> 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?
>
That is very true. In many cases it is possible to write code in an
"open", "one-sided" manner that assumes that there are things that we
know to be true and then other things that we do not know to be true -
which is definitely to be interpreted differently than knowing that
something is false. In other words the "logical of knowing" is not
Boolean. In an "open world" semantics by convention we consider "true"
and "false" as representing only the first two possibilities. But of
course this is only half of the story and as Gaby says: it is
sometimes rather difficutl to decide what consequences (if any) should
be drawn in the case of "false" ...
Because of Gaby's oddly adverse reactions, I am reluctant to bring up
category theory again, but in my opinion this is one of the areas
where topos theory (categorical set theory) could play a very
significant role. Besides the "logic of knowing" there are other
non-Boolean "logics" that might be appropriate for other situations.
But this is a whole other area of research.
> 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.
>
Again I completely agree with this. Axiom needs a better
representation of monoids and monoid operations. For any given
function of the form:
(S,S)->S
we need to say whether it a monoidal operation or not and if so, what
is the associated identity. One way to do this would be for each
domain containing monoid operations to provide a higher-order
operation
MonId : ((S,S)->S) -> Union(identity: S, "false")
with the obvious implementation.
Then in 'reduce(f,l) ' we could write:
if #l=0 and MonId(f) case Identity then return MonId(f)
No more need to worry about equality of functions!
> ...
> 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:
<< clip excellent quote from James Davenport ... >>
> "Equality in computer algebra and beyond"
thanks Gaby. But why "no category theory"? :-(
>
> [...]
>
> 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.
>
:-) I do appreciate the invitation by not the manner of it's delivery!
I do have some (categorical) ideas about equality but as I said above
(and apparently Gaby agrees), I do not think this has much to do with
the current issue.
> ...
> 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.
>
There you go applying those "politically inappropriate" terms again!
>
> | 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 :-)
>
Agreed.
Regards,
Bill Page.
-------------------------------------------------------------------------
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
