On Tue, Aug 5, 2008 at 9:10 PM, Bill Page <[EMAIL PROTECTED]> wrote: > On Tue, Aug 5, 2008 at 9:26 PM, Gabriel Dos Reis wrote: >> Bill Page writes: >> | >> | Ok. What do you think of this solution (passing symbols) that I have >> | been discussing with Ralf? >> | >> | http://axiom-wiki.newsynthesis.org/SandBoxAbelianDuck >> | >> | )abbrev category ASSOC Associative >> | ++ m(m(a,b),c) = m(a,m(b,c)) >> | Associative(m:Symbol):Category == with >> | m:(%,%) -> % ++ multiplication >> >> >> I think I already offered my opinion about this when we were in >> Hagenberg. My problem with this is that it associate the associative >> property with a symbol, not an operation. > > That is not how I interpret the above code. In fact, if I write: > > MyDomain(): Associative("*") > > The compiler does generate code with > > *:(%,%) -> % > > The associative property is associated with the category 'Associative("*")' > but > > *:(%,%) -> % > > is exactly what is exported by this category so it is precisely that > map to which this property applies.
But then the associative property is associated (no pun intended) with the symbol "*": Now you have a category domains with associative "*". I cannot name the operation and describe its property. I can only name the operator name. > >> That is a problem because an operation is not just an symbol. An >> operation is described by a name, a domain of computation (or package) >> and its signature. > > Yes. That is exactly what I see above. > >> Otherwise, one gets into the same trap as the M&M who as able to >> evaluate M * N - N * M to *integer* 0, no matter what M and N might >> be. > > I don't see that happening here. Could you explain? Oh, I suspected you would do the same think for commutative operator, Assuming "*" is commutative, how to you simplify the expression M*N - N*M? > >> >> I believe I already sketched a solution that I'm working on (I hoped >> Yixin would pick it up, but that is not coming). It realies on the >> notion of `modemap'. So in the typical System F/AXIOM style, >> I would write the above as >> >> Associative(T: Type, Modemap(T,T,T): op): Category == with nil > > You meant? > > Associative(T: Type, op:Modemap(T,T,T)): Category == with nil Yes, sorry -- very hard to switch from C++ to Spad. > >> >> There is no export because associativity is essentially a logical >> axiom. > > All category declarations are "logical axioms" in this sense. well, some of them are purely logical, some are non logical. A category that meaningfully exports an operation is not purely logical -- it has a computational content. > >> >> In Implicit System F, or in a forall-quantified style I would write >> >> forall(T: Type) . >> Associative(Modemap(T,T,T): op): Category == with nil >> >> so that when I say Associative(_+$Integer), T gets deduced to >> Integer. You can see how this relates to the issue Stephen and >> I discussed at the workshop in Hagenber. >> > > Yes, I thought it was an interesting discussion but this machinery > strikes me as being to "heavy" for what seems to me to be a relatively > simple problem. I am afraid that such changes lead away from the > original intend of Spad/Aldor as fundamentally an *algebraic* > language. But my ideas about this are only partially formed, so I do > want to keep an open mind. That is interesting. I would be highly interested in knowing what you think is not algebraic about a universally quantified type. As for heavy, well; that is a valid *opinion*. We can have a more objective measurement if we have implementations of both ideas in concrete algebras and can test them -- as opposed to evaluating piecemeal solutions. > >> | --------- >> | >> | where the compiler does already replace 'm' with the symbol passed >> | as an argument. The problem with this approach actually occurs at >> | a later stage in the compilation where the parameter occurs to the >> | right of the ==. E.g. >> | >> | )abbrev category ID Identity >> | ++ m(u,a)=a and m(a,u)=a >> | Identity(u:Symbol,m:Symbol):Category == Commutative(m) with >> | u: () -> % ++ unit >> | >> | ------- >> | >> | Somewhere else we get the complaint: >> | >> | >> System error: >> | |Identity;| [or a callee] requires more than one argument. >> | >> | -------- >> | >> | Is the cause clear to you? >> >> I have to have a complete working system to get my head around the >> problem. >> > > Is there something more that I could provide you that is not included > on the above mentioned web page? not at the moment. > >> | >> | I recall Stephen Watt's comment during the recent workshop that >> | they (meaning the ScratchPad project I presume) tried to make >> | this sort of solution work but abandoned it for reasons which he >> | did not elaborate. Do you have some ideas about what these >> | reasons might have been? >> >> In fact, as it turned out at the workshop Stephen was also solving >> that same problem; but from a different angle; I'm not sure he >> abandoned. I think we did not finish the discussion -- but I >> mentioned that I was solving it by making modemaps more real; >> he observed that also permits ML-style polymorphism. >> > > Yes, that is what I referred to above as a "heavy non-algebraic" kind > of solution. I think it is "easy" to label any proposal with any adjective; so I hope you will elaborate on the `non-algebraic' part -- we will with the `heavy' part later. > I am sorry to use such a vague characterization. Maybe I > will be able to do better at some time in the future. Well, it is very important to get those on firms grounds because they are heavily loaded words (no pun intended) :-) > > I took that fact that this approach of passing symbols that are > evaluated as names of exported functions "almost works" as evidence > that some changes were made to Spad that were intended to make this > possible. (Why else evaluate the function names?). I suspect the right question is why category expressions are evaluated at compile time. The answer is to get the list of exported operations. > It seems to me that > the bug that prevents its full use in the "monoid problem" is not a > fundamental design problem but rather something much more technical. I > would greatly appreciate any suggestions you have about how to > approach debugging this problem. My immediate question is how do you use it in practice? A monoid operation comes with a neutral element. How do you use it? Something I found very effective at testing proposals I've seen so far is to construct all the usual algebraic structures up to Lie algebras and use them in usual algorithms. That is a good test. Can you test that? ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
