Equality in Computer Algebra and Beyond James H. Davenport, JSC Volume 34 Issue 4, October 2002
Equality is such a fundamental concept in mathematics that, in fact, we seldom explore it in detail, and tend to regard it as trivial. When it is shown to be non-trivial, we are often surprised. As is often the case, the computerization of mathematical computation in computer algebra systems on the one hand, and mathematical reasoning in theorem provers on the other hand, forces us to explore the issue of equality in greater detail. http://dl.acm.org/citation.cfm?id=636429 http://www.calculemus.net/meetings/siena01/Papers/Davenport.pdf On 24 March 2015 at 09:35, Waldek Hebisch <[email protected]> wrote: > Bill Page wrote: >> >> The following patches provide hashUpdate! and as a result hash >> functions to the Expression, Kernel, Float and Complex domains. >> ... >> wspage@opensuse:~/fricas-ker> svn diff > ../exprhash.patch >> wspage@opensuse:~/fricas-ker> cat ../exprhash.patch >> Index: src/algebra/expr.spad >> =================================================================== >> --- src/algebra/expr.spad (revision 1893) >> +++ src/algebra/expr.spad (working copy) >> @@ -147,7 +147,10 @@ >> x : % = y : % == (x - y) =Rep >> numer x == numer(x)$Rep >> denom x == denom(x)$Rep >> - >> + hashUpdate!(s : HashState, x : %) : HashState == >> + s := hashUpdate!(s, numer x) >> + s := hashUpdate!(s, denom x) >> + >> EREP := Record(num : MP, den : MP) >> >> coerce(p : MP) : % == [p, 1]$EREP pretend % > > There is a serious problem with this patch. Namely, your > 'hashUpdate!' only depends on representation. This means if > we have two expressions 'e1' and 'e2' such that 'e1 = e2' > (according to equality in Expression), but 'rep(e1) ~= rep(e2)' > then it may happen that 'hash(e1) ~= hash(e2)'. Yes, certainly I (mostly) agree with you, although my definition of 'hashUpdate!' does not depend on the representation as such since it uses only exported operations. The representation could change without changing this definition. That is why I wrote: >> Also >> included is a patch to XHashTable to optionally pass a user specified >> function representing equality in the key domain. This is important >> for the use of XHashTable in domains like Expression where equality >> is not canonical." >> ... > However, correct > implementation of 'hash' must satisfy 'hash(e1) = hash(e2)' if > 'e1 = e2'. Due to this requirement finding correct hash function > for domains with noncanonical representation is quite tricky. > Expression adds additional difficulties due to dynamic nature. > Sure, but Davenport 2002 advises that I should ask: "equal as what?" To satisfy this that we need to be able to pass an additional parameter to XHashTable. > I admit that current situation where at category level we claim > there here is hash function, but a lot of domains lack implementaion > is unsatisfactry. But it is not clear what to do. We could > introduce new category, say 'Hashable' and make sure that > domains which export 'Hashable' also implement 'hash'. Or we > could weaken requirement on 'hash' and say that equality > of representations is enough to have equality of hashes. > However, weaker requirement on 'hash' would seriously limit > its usefulness, basicaly to cases when one works with > representaion. Since we want to hide representation, this > is serious limitation. > I think a better way to solve this is to realize that the "unsoundness" is in the specification not the implementation. It seems to me that 'hash' and 'hashUpdate!' should be exported by the category 'Comparable' without presuming any relationship with the "mathematical" equality = that should actually be exported by SetCategory rather than BasicType. Then we only need that 'hash(e1) = hash(e2)' if 'not (smaller?(e1,e2) or smaller?(e2,e1)' Even better perhaps would be if Comparable also exported an operation named 'equal' that had this relationship to 'smaller?'. The name 'equal' should remind one of EQUAL in Lisp (in particular IBM Lisp/VM, ref. Davenport). > We could easily add 'hashUpdate!' to canonical domains, like Polynomial > or SAE. Also we could add 'hashUpdate!' to Set (but implementation > is tricky). But Expression and Float pose serious difficulties. The fact that there are "serious difficulties" should be an indication that the specification is wrong. In fact as you know according to Richardson's theorem it is impossible even in princple in Expression since we have rational functions plus 'abs', and 'sin'. But the concept of hashing is so important that we should not make it to extraordinary things in order to use it in domains like Expression. > Similarly, power series and streams are problematic (they are > supposed to be lazy but hash function has to access elements). > For lazy infinite objects it is important to compare the algorithms/functions that generate them rather than values. Since two or more algorithms may generate the same sequence we have the same situation as in Expression but that should not mean we cannot hash them. > Extra comment: current handling of kernels is unsound so why > I oppose adding code which is "no worse" than existing one? > The point is that I would like to eventually remove > unsoundness. If we allow new unsoundness to get in then > there is almost no chance of removing unsoundness: new > one is likely to get in faster than old is removed. > So I keep old unsoundness for pragmatic reasons: replacing > it by sound code is a lot of work and takes time and > without unsound parts we would lose important functionality. > In principle I agree and as you know I am also concerned about the current handling of kernels. But I think the problem here not unsoundness but rather the assumption that hash should necessarily be related to *mathematical* equality. Bill. -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
