Bill Page wrote:
>
> On Tue, Apr 8, 2008 at 9:55 AM, Waldek Hebisch wrote:
> >
> > 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?
>
Mapping uses EQ (below you quoted the definition). Above I wrote
how we compare constructors (which is done in other parts of the
compiler).
> 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 concious decision to give wrong definition when type rules
require something and correct thing can not be implemented
> >
> > 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.
>
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.
> > 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".
> >
> > > 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.
>
1) Inlining invalidates your trick of using function to force resolving
positions in the domain vector.
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.
> > 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.
--
Waldek Hebisch
[EMAIL PROTECTED]
-------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
