On Tue, Apr 8, 2008 at 9:55 AM, Waldek Hebisch wrote: > > Bill Page wrote: > > Yes! That is the right idea but really what we need is for the SPAD > > compiler to choose a reasonable signature for the '=' operation. > > Probably everything would work-out (almost) ok if the built-in > > 'Mapping' domain exported an operation like this: > > > > (f:(S,S)->S) = (g:(S,S)->S)):Boolean == EQ(f,g)$Lisp > > > > Well, EQ is wrong, given our representation of functions. Namely, > Spad function is a pair. First coordinate (CAR) is a Lisp > function or symbol, the second is constructor where the function > is defined. The constructor is represented by a Lisp vector. This > vector is not unique: the runtime tries to reuse vectors and keeps > cache of recently created ones. But if you generate a lot of > vectors the old vector may be purged from the cache and you may > get a new vector even if domain are "equal". So, you need to > compare vectors for equality: currently this is done using > devaluate function and comparing (using Lisp EQUAL) the resulting > S-expressions.
Do you mean that this is done by the '=' operation exported by Mapping? For inspiration I was looking at MappingEqual(x, y, dom) == EQ(x,y) in 'buildom.boot'. Do you think this is a bug? > > Concerning exporting equality: 'Mapping' has 'SetCategory' and > exports equality. It is likely that this equalty 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. > > > Your suggested code only fails to compile because of the missing > > definition of equality for functions. > > > > > OTOH I am not sure if it is supposed to actually work -- > > > equality of functions is a tricky business. One can > > > define reasonable equality for functions, but this > > > basically disables some optimizations. > > > > I think that in principle one can simply compare the names of the > > operations. > > You assume that you can determine name given a function. This is > a non-trivial assumption -- in C program compiled without debugging > information all you have is address of machine code. All Lisp > implementations I checked keep function names, but there is no > requirement to do this -- in principle implementation can throw > out names to save space. > I do not think there is a need to solve problems that do not exist. But certainly we should document this as a requirement of the underlying abstract machine for Axiom. > 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? > > > But the complication is that the "names" of some > > operations in SPAD are not fully determined until their first > > application during run-time. There is a need to resolve calls to > > 'newGoGet' before comparing the names. One way to do this is simply to > > apply the functions to some arguments at least once before doing the > > comparison. E.g. > > > > f(0,0)=(0+0)$S and (f = _+$S) => return 0$S > > > > Here both 'f' and '+' are applied to a member of S before testing the > equality. > > > > 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. > > > If the function equality operation were actually exported by Mapping, > > then there would need to be some more "magical" way to do this inside > > the operation itself. > > > > > And, when I write "one can define", this assumes > > > complete low-level control of the implementation -- > > > for example Lisp can defeat our efforts. > > > > > > > Could you explain further how you think Lisp might affect this? > > > > 1) Keeping or not names > 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. 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
