On Tue, Apr 8, 2008 at 12:52 PM, Waldek Hebisch wrote: > > Bill Page wrote: > ... > > For inspiration I was looking at > > > > MappingEqual(x, y, dom) == EQ(x,y) > > > > in 'buildom.boot'. Do you think this is a bug? > > > > IMHO think that this definition is not simply a bug -- it is > a conscious decision to give wrong definition when type > rules require something and correct thing can not be > implemented >
By "type rules" do you mean the function signature? Isn't that properly reflected in the function name when the name is fully resolved? The bug I think, is that MappingEqual does not attempt to resolve the 'newGoGet' indirection. > > > > > > > Concerning exporting equality: 'Mapping' has 'SetCategory' and > > > exports equality. It is likely that this equality is not visible > > > in some places where formally it should be available. One > > > reason may be that nobody treats seriously equality for > > > functions (as I wrote above current definition (as EQ) does > > > not guarantee that "the same" functions are equal). > > > > > > > Yes! I think this is a serious problem - at least from the point of > > view of the fundamental semantics of SPAD and Axiom. > > > > Remember that mathematical equality on mappings represented by > programs is undecidable. So, from the point of view of "fundamental > semantics" equality on mappings should be undefined. > 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. > > > > Also, as I wrote, it is not enough to compare code, you need > > > also compare constructor. > > > > > > > I don't think I understand this yet. Could you give an example? > > > > Do you consider +$(Polynomial Integer) to be the same as > +$(Polynomial Fraction Integer)? IIRC both use the same code, > so checking just code part would make you belive that they are > the same. However, they belong to different domains, so I do > not consider them "the same". > 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) Type: ((Polynomial Fraction Integer,Polynomial Fraction Integer) -> Polynomial Fraction Integer) (3) -> > ... > > > > > > Have you noticed that in another thread we are trying to expand > > > functions inline? Spad compiler may use inline version for the > > > first comparision and defeat your attempt... > > > > > > > Yes. I found the discussion in the other thread very informative. But > > I do not see how inlining functions could cause any problem with > > properly defining functional equality. > > > > 1) Inlining invalidates your trick of using function [application] to force > resolving positions in the domain vector. 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? In any case, I expect that the MappingEqual function should do this resolution of positions (and therefore the function name) itself when necessary before calling EQ. > 2) Suppose that A(X) defines generic operation foo. If B uses > foo and the compiler knows that X is in fact Integer, than it is > reasonable to produce specialised version of foo which can only > operate on Integer, but is more efficient. Now, if C also uses foo > with Integer arguments, but compiler does not see this than C > will use generic version. In principle, you may have several copies > of foo and you can not discover that they are equal just comparing > code. > 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. > > > > 2) Making "the same" functions unequal > > > > > I think solving the general problem of making "the same" functions > > equal is too hard. It is better to have an efficiently computable > > definition of equality that is sufficient for most purposes - > > essentially a syntactical one. > > > > Above by "the same" I meant syntactic equality. > Hmmm... how can something that is "syntactically equal" actually be unequal? 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. Regards, Bill Page. ------------------------------------------------------------------------- This SF.net email is sponsored by the 2008 JavaOne(SM) Conference Register now and save $200. Hurry, offer ends at 11:59 p.m., Monday, April 7! Use priority code J8TLD2. 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
