On Tue, Apr 8, 2008 at 7:03 PM, Waldek Hebisch wrote: > > > > > Bill Page wrote: > > ... > > > The bug I think, is that MappingEqual does not attempt to > > > resolve the 'newGoGet' indirection. > > > > No, 'newGoGet' is not a problem for _this_ definition. EQ compares > addressess of cons cells, while 'newGoGet' changes content -- so > result of the comparison does not change after calling 'newGoGet'.
Please see the examples here: http://axiom-wiki.newsynthesis.org/SandBoxMyReduceInFriCAS The debugging output from: print(coerceMap2E(f)$Lisp::OutputForm) print(coerceMap2E(g)$Lisp::OutputForm) shows: theMap(INT;+;3$;37,688) theMap(newGoGet) and the comparison fails. > BTW: For some reason I get fully resolved mappings, so ATM I am > not sure if 'newGoGet' poses any problem. Rather, I mean different > problems. One is with caches -- I am affraid I can not give > you example, but I am pretty sure the problem is real. Another > is with recompilation: > > (1) -> f1 := _+$Integer @ Mapping(Integer, Integer, Integer) > > (1) theMap(INT;+;3$;37,996) > Type: ((Integer,Integer) -> Integer) > (2) -> f2 := _+$Integer @ Mapping(Integer, Integer, Integer) > > (2) theMap(INT;+;3$;37,996) > Type: ((Integer,Integer) -> Integer) > (3) -> (f1 = f2) :: Boolean > > (3) true > Type: Boolean > (4) -> )compile FOO.spad > (4) -> g := _+$Integer @ Mapping(Integer, Integer, Integer) > > (4) theMap(INT;+;3$;37,4) > Type: ((Integer,Integer) -> Integer) > (5) -> (f1 = g) :: Boolean > > (5) false > Type: Boolean > FOO.spad have nothing to do with Integer: > > )abbrev category FOO FOO > FOO(): Category == with nil > > but mere fact that I compiled FOO invalidates all domain vectors... > Wow, that's pretty neat! From your statement: "invalidates all domain vectors" I would have been afraid that f1 and f2 were no longer valid functions, but this is not the case. Here I see that although their names are not equal both f1 and g still refer to effectively the same function since they have the same definition and still compute the same value. > ... > > > > Of course equality of mappings is in general undecidable but I do > > not agree that therefore equality should be undefined. In many > > (most) practical circumstances simple syntactic equality of the > > Lisp names should be sufficient. Instead of true equality we have > > a more fine grained equivalence relation on the function space > > that sometimes says two functions are not equivalent when in > > fact they are the same function. But this does not prevent us > > from writing correct code - such as the 'reduce' example referred > > to earlier in this thread. > > > > Here you speak like a practical programmer -- from programmer > point of view it makes sense to have equality, even if it is > imperfect. Perhaps we should not think of it as "perfect" or "imperfect" but rather a better or worse approximation for equality. One thing that I know about this approximation is that if it is 'true' then the equality holds but if it is 'false' I do not know anything about the actual equality. The approximation is formally compatible (consistent) with the equality in this sense. > But IMHO "fundamental semantics" is not about practicalty -- > I would say that "fundamental semantics" is about clean and > consistent definition. Practicality typically means that you > compromise and sacrifice cleanliness and consistency... > In this case I do not agree that the definition of syntact equality of functions sacrifices cleanliness and consistency. > ... > > I agree that they are different. This is properly represented by the > > function names: > > > > (1) -> _+$(Polynomial Integer) > > > > (1) theMap(SMP;+;3$;27,628) > ^^^ > > > Type: ((Polynomial Integer,Polynomial Integer) -> Polynomial Integer) > > > > (2) -> _+$(Polynomial Fraction Integer) > > > > (2) theMap(SMP;+;3$;27,196) > ^^^ > > If you mean that the numbers in printed form "properly" show the > difference, then this is not really proper: the number is part of > hash of domain vector. Since the hash is truncated to three digits > you may easily get collisions. Hmmm... how are such collisions currently resolved in SPAD? > And you have other problems with "the same" functions looking > unequal. So, this is just a hack, you need to work harder to > compare domains. > I presume you mean: "to compare *functions*"? I am listening :-) Do you have any ideas? > > ... > > Maybe, however in order to do inlining in the first place it seems to > > me that the compiler must somewhere have already fully resolved the > > function. Or do you imagine that fully inlined functions will have no > > separate implementation somewhere in the system? > > > > Compiler resolve name at compile time. This does not imply that > the name will be resolved at runtime. Actually, since compilation > can redefine functions after compilation all functions will be > unresolved. > I admit that the problem of function definitions after re-compilation within a session is interesting. > ... > > > > In such a case would these optimizations be reflected in the mangled > > function name? If so, then I guess the proposed definition based on > > syntactic equality would fail. But doesn't this depend on the specific > > mechanism for the name resolution? Maybe one could write > > MappingEqual in such a manner that the same (unoptimized) > > name resolution is always applied for the purposes of functional > > comparison. > > > > You assume that you have name -- there is no fundamental reason > that compiler generating machine code associate names with given > piece of code. So, reiterating -- if you want equality for functions, > the whole system starting from relatively high level down to the > metal must make some effort. > You have convinced me. I do want a "better" equality for functions than what is currently implemented in Axiom and SPAD. I think this is quite important. > > ... I understand that the same function might sometimes end up > > having two (or more) different names and therefore appear to be > > unequal (syntactically) but I do not think that this is a problem in > > the type of use case I need in order to write the extended reduce > > function. > > > > One problem is that programmers want to write programs, for > them it is enough that their program "works". But if you design > language you need to look at all possible programs -- minimally > you need clear definition of programs which are not supposed > to work. My point is that it is tricky to give strong warranty > about function equality. Without such warranty it is easy to > write programs which "almost always" work -- that is programs > which exhibit hard to reproduce bugs. > I agree. Part of the purpose of this discussion for me is to learn when the current definition "works" and when it does not. You have helped me a lot with this. Thank you. :-) 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
