"Bill Page" <[EMAIL PROTECTED]> writes: [...]
| 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. There are at laest two things I find wrong about the above attempt at reduction: (1) it focuses on a representation of a value (S) as being monoid; and (2) it brings in equality test on functions. monoid structure really is a property of an operation, not the values being operated on -- because it is the mapping that endowes the set with some structure, and the set of values can serve as domain for more than one monoid operation. Secondly, even the non-computational definition of monoid does not mention equality of function. Now, I understand that Axiom's algebra is currently defective as I pointed out in the old days http://www.archivum.info/[EMAIL PROTECTED]/2006-03/msg00004.html that I subsequently termed `the monoid problem'. And as I would repeat myself, the fact that it is currently defective is no excuse to pile more hacks on top of it. I understand you're very sensitive to the word `hack', but the current state of affair is just that: pile of hacks (some fortunate, some unfortunate). We can't just solve them by putting more hacks on top. And frankly, we can't just pretend that category theory is the answer and at the same time wave ourselves from to the rigour of computational category theory. [...] | 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. And I precisely disagree because reduction has nothing to do with equality of functions. If we agree that reduce is broken and has to be fixed, then it should be fixed. It should not be hacked up. Furthermore, I cannot marry your suggested `fix' with your often repeated injunction that Spad should be more categorial. Either we decide we do science, or we decide we just hack up something. My belief is that the Axiom family should be about science. We have enormous job ahead of us because there are so many things broken. [...] | > ... | > 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. When one gets serious about an undecidable problem and try to solve useful parts of it, one either precisely describe which sub-classes one is working on (i.e. the restrictions), or one works with tri-valued Boolean logic (yes, no, dontknow). | 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. I would like you to get the record straight: I'm not adverse to category theory. Quite the contrary. I'm against worship in category theory. That is a very different thing. [...] | 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! In my local tree, I have forall(T: Type) Monoid(f: (T,T) -> T): Structure == SemiGroup(f) with 1: T and in your reduce, you would write: null? l and Monoid(f) => 1$Monoid(f) (yes, Monoid(f) and decay to a Boolean saying that if was asserted to make up a monoid, and it also serves as a scope). Not everything is working right, right now; so that is why you don't see me bragging about it. [...] | > 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! There is nothing politically inappropriate in the terms `hack' and `superstition' -- they are appropriate to the situation. All we can complain about is that they are not strong enough to describe the current state of affairs. -- 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
