Ralf Hemmecke <[email protected]> writes:
>>> For example one could have that
>>>
>>> TaylorSeries(Integer) has RingOperations
>>>
>>> meaning that all the usual ring operations are available, but you
>>> don't assert anything about axioms these operations fulfill.
>>
>> I guess it's only a difference in naming, but I'd call
>> TaylorSeries(Integer) a Ring, but I wouldn't require Ring to have
>> equality -- thus I'd make it the same as your RingOperations.
>
> http://en.wikipedia.org/wiki/Ring_%28mathematics%29#Formal_definition
>
> If you want this, then you basically violate any axiom that involves
> =.
Sorry, I was unclear again. I meant: I wouldn't require Ring to have
computable equality.
>> What I mean with "such a scheme" is a *useful* set of categories that
>> assert various meanings for equality. (it seems to me that
>> computability problems occur most frequently for equality)
>
> We probably are in favour of the same thing, so we shouldn't argue too
> much.
Yes :-)
> Having the same =: (%, %) -> % with a different definition might not
> be a big problem, but can become one. For example, one cannot have
> equality in Stream(Integer), but if one imposes additionaly
> properties, namely finite-stream, then of course that = would be
> computable. Now what ++ documentation applies? So it seems, having
> the same name is not a good idea. I would like to reserve = for a
> computable total function.
I agree.
>> There is some thinking required, however: should some of these
>> operations have the same signature, but different meaning?
>
> Look into the Aldor library. The most basic type is PrimitiveType. It
> implements equality, but look at the documentation that Bronstein has
> specified for =.
>
> #if ALDOC
> \alpage{$=$}
> \Usage{a = b\\ a $\sim=$ b}
> \Signatures{
> $=$: & (\%,\%) $\to$ \altype{Boolean}\\
> $\sim=$: & (\%,\%) $\to$ \altype{Boolean}\\
> }
> \Params{ {\em a, b} & \% & elements of the type\\ }
> \Retval{ If $a = b$ returns \true, then $a$ and $b$ are guaranteed to
> represent the same element of the type. The behavior if $a = b$ returns
> \false~depends on the type, since a full equality test might not be
> available. At least, it is guaranteed that $a$ and $b$ do not share the
> same memory location in that case. The semantics of $a~\sim= b$ is
> the boolean negation of $a = b$.}
> #endif
Yes, that's precisely the question of above. It seems both of us rather
had a = b mean just that, and then have additionally
| true | false
------------------------------------------------------------------
a = b | a and b are equal | otherwise
provablyEqual | a and b are equal | a and b might be equal
provablyDifferent | a and b are different | a and b might be different
right? Ring could then export provablyEqual and provablyDifferent (with
silly default false) but equality would be reserved for domains with
computable equality like Integer, IntegerMod, AlgebraicNumber,
Polynomial R, Fraction R, Matrix R, List R, ... (whenever R has
ComputableEquality).
Are we on the same track?
Martin
Martin
--
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.