"Bill Page" <[EMAIL PROTECTED]> writes: | On Tue, Aug 5, 2008 at 8:42 PM, Gabriel Dos Reis wrote: | > ... | > Again, my problem is not that I do not understand what a partially | > ordered set is -- I guess you can give me credit for that [I know I'd | > assume that anybody contributing to this discuss understands | > those basic notions until proven otherwise :-)] | > | | Personally as you know, I do give you a lot of *credit*. This is an | email-based discussion - most normal cues from a face to face meeting | are missing. In my experience it is not safe to assume anything about | the people potentially contributing to the discussion - even it that | means maybe offending someone by making what to them might seem like | unnecessary definitions and references. By making such references it | is definitely not my intention to suggest any deficiency on anyone's | part.
Yes, I've done lot of technical work by email in larger forums; it has almost always worked well to assume a minimum of `domain knowledge' from the other end of the communication link -- until proven otherwise (and if the minimum domain knowledge is missing, that usually shows up very quickly). Unless, of course, we are in typical `teacher/student' setting (which is not the case here); but even there you get good results by assuming a minimum knowledge :-). That helps quikcly get to the meat of the problems, and possibly solutions; that also saves from many distractions :-) | > The problem is that even if you define a separate category named | > PartiallyOrderetSet that exports "<" and the likes, that still does not | > solve a fundamental problem: That many partial orderings may exist | > on the same domain, and if we stipulate that any partial ordering must | > be spelled "<", then we have an impossible situation: This is exactly | > an instance of the general monoid problem. This is why I view this | > solution as abstractly attractive but programmatically ineffective -- | > unless the monoid problem is solved. | > | | 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 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. 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 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 There is no export because associativity is essentially a logical axiom. 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. | --------- | | 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. | | 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 abandonned. 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. -- Gaby ------------------------------------------------------------------------- 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
