Martin Rubey wrote:
> Ralf Hemmecke <[email protected]> writes:
>
> 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?
>
I believe to "normal" domains should be computable and our definition
of computable should include equality. In more detail: power of
matchematical reasoning comes from ability to compose results
in arbitrary ways. Once not all operations are computable
reasoning about correctness and code gets _much_ more complicated.
Since not all things are computable we have to provide some
"uncomputable" operations (approximations, probabilistic routines
etc.). But we should prefer computable equivalents if possible.
To illustrate possible pitfals let us do a little thought
experiment. Suppose that we have a function from integers
to integers such that we can compute the difference
Delta(n) = f(n+1) - f(n) cheaply. By computing Delta(n) at
many random points if we get zero from each evaluation
we can conclude that Delta(n) "almost surely" is 0.
This is quite different from beeing zero: if Delta(n)
is zero then using induction we prove that f is constant.
But if f has single jump at some very large point then we
still have Delta(n) 0 unless we hit jump point which has
very low probability.
Normal methods proving program correctness work recursively,
assuming correctness of components. And highly recursive
nature of FriCAS code means that proof are inductive.
Of course, some resonings works using only one-sideded
or probablistic assumptions, but methods are more
complicated and results are weaker than for full correctness.
There is one weakening of full correctness that works well
in practice: partial correctness. In case of partial
correctness we do not require that computation always
finishes sucessfully, but if it finishes then result
should be correct. Computation may not finish because
of infinte loop (or infinite recursion), but also may
finish unsuccesfuly due to detected error (exception).
While program that always finish are preferable, in reality
we have to accept programs which cause errors. Namely,
the simplest possible error is running out of memory.
Several algorithms "typically" works well, but have
very bad worst case complexity -- rejecting such algorithms
would make FriCAS inpractical. Once we accept one class
or error I think it is reasonable to accept other possiblities
for error. Of course, if is easy to perform computations
without error we should do this. But in case of hard
problems getting either correct result or "can not do this"
error is better than nothing (and fits well into reasonings
proving correctness of result).
In other words I find operations which throw errors in
problematic cases as acceptable. On the other hand
I conside as anacceptable operations which pretend to do right
thing, but produce possibly wrong results.
Coming back to start of this thread: it is possible to compute
determinant in power series domains, but it has to be done
differently than in other domains. More precisely, expanding
determinat into products is inpractical for large matrices
(it seems that already 15 by 15 is inpractical). I did
not check other methods which avoid zero test (it is easy to
find methods which are slightly better than full expansion,
I am not sure if there is something much better). But
in power series domains we really work with finite approximatins
to true infinite value. If column of matrix is zero up to
given order (this is computable condition) then determinant
is zero up to corresponding order. OTOH if we have nonzero
element we can use it as pivot and reduce problem to smaller
matices. So the catch is that we can not use generic method,
but must use method which makes good use of specific context.
Now, if sombody wants to create a set of domains and operations
that works well with weaker information than equality test
I encourage then to experiment (our power series framwork
can be treated as such an experiment). However, I would
prefer to keep such experiments somewhat isolated, to
avoid things like our current determinat algorithm
applied to power series.
Releated, I would prefer clearly specified "precision",
so for example instead of "additive?" which uses some global
variable I would prefer version which takes explict precision
parameter.
--
Waldek Hebisch
[email protected]
--
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.
