Waldek Hebisch <[email protected]> writes: | Gabriel Dos Reis wrote: | > | > Waldek Hebisch <[email protected]> writes: | > | > | Gabriel Dos Reis wrote: | > | > | > | > Bill Page <[email protected]> writes: | > | > | > | > | Maybe it is a bit late to ask this question but why not just define a | > | > | default hash function for FriCAS directly in terms of the hash | > | > | function in the underlying Lisp? E.g. | > | > | | > | > | hash(x) == SXHASH(x)$Lisp pretend SingleInteger | > | > | > | > This is essentially what OpenAxiom does. I do not know of any problem | > | > with it. | > | | > | AFAICS there are two problems: | > | | > | 1) Correctness: FriCAS objects may be equal from FriCAS point | > | of view, but have different enough representations so that | > | SXHASH produces different values. | > | > This problem is far more general than that and is not specific to using | > SXHASH or failure to use it. Until AXIOM systems integrate full | > evidence/proof requirements of certain relations or axioms, this is not | > going to magically go away. | | Consider D := Fraction(S) where S is not a GcdDomain. No fancy | proof theory is needed to see that equality in D is mathematical, | while representation is expected to be nonunique.
You may not need a proof theory to understand a representation may not be unique, but you would need a proof theory to mechanically check that an implementation of hash() for such domains indeed follows the right invariant, e.g. x = y => hash x = hash y. | Admitedly, | ATM I can not give you a way to build such IntegralDomain S using | only existing constructors, but there is a lot of such S in | mathematics and it should be possible to represent them. That isn't the issue. Whatever you ended up with you need to provide machine checkable evidence that x = y => hash x = hash y. | And adding appropriate constructor at Spad level is trivial. | | > In OpenAxiom, SXHASH implements the default hash() operation and is in | > agreement (as far as I can determine) with the default implementation of | > =$SetCategory. | > | > | > | > | > | 2) Preformance: IME SXHASH for arrays ignored most of differences | > | leading to large number of conflicts. | > | > I haven't had these problems with OpenAxiom/SBCL; maybe other Lisp systems | > have different behaviour. | | With Debian sbcl 1.40: | (1) -> )lisp (lisp-implementation-version) | Value = "1.0.40.0.debian" | (2) -> v2 := vector([0, 0, 0]) | | (2) [0,0,0] | Type: Vector(NonNegativeInteger) | (3) -> v1 := vector([1, 2, 0]) | | (3) [1,2,0] | Type: Vector(NonNegativeInteger) | (4) -> SXHASH(v1)$Lisp | | (4) 518591303 | Type: SExpression | (5) -> SXHASH(v2)$Lisp | | (5) 518591303 | | As you see vectors produce the same value. I have seen this behaviour | for ages and while ATM I can not check newer sbcl I doubt that it | is better. That is correct. What I am saying is that I haven't had the performance issue. -- Gaby -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
