Bill Page wrote:
>
> 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.
>
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'.
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...
> >
> > > >
> > > > 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.
>
Here you speak like a practical programmer -- from programmer point
of view it makes sense to have equality, even if it is imperfect.
But IMHO "fundamental semantics" is not about practicalty --
I would say that "fundamental semantics" is about clean and
consistent definition. Practicalty typically means that you
compromise and sacrifice cleanliness and consistency...
> >
> > > > 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)
^^^
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. 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.
> > ...
> > > >
> > > > 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?
>
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.
> > 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.
>
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 relativly high level down to the
metal must make some effort.
> >
> > > > 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.
>
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.
--
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
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
