Martin Rubey wrote:
> > 3) Re-organize expression domains to allow finite fields, but
> > still warranty that operations can be done.
> >
> > If we want faithfully follow Axiom paradigm than only 2) or 3) would
> > be acceptable. 3) would be ideal, but I am affraid that the best
> > we can get in this direction would be some combination of
> > 2) and 3). I must say that I consider 2) as very ugly. So 1)
> > looks like best alternative...
>
> why do you think that 3) is difficult?
>
Consider:
P := PrimeField 1000003
T := UnivariateTaylorSeries(P, t, 0)
t: T := monomial(1,1)
polynomial(sin(t), 30)
This make sense, is useful and works now. How you want to allow
something like this, but disallow 'polynomial(sin(t), 1000004)'?
Note:
- I want general functions here
- I want more operations (integration, solutions of differential
equations, etc...)
- I want to reuse code doing actual computations
More generally, complexity theory shows in several places
that if you require "warranted" success than you can solve less
problems than if you allow failure (or infinite loops).
In particular, unsolvability of haltiong problems means that
the most efficient method to find out if program (on given input)
will stop in after at most n steps is to run the program and interrupt
it in case it does not stop in n steps. To put this in different
words: the only general method to find out that program (on given input)
will run without raising errors is to run the program and see if
it raises error.
Note, that in general to know that our code is correct we need
some proof. To avoid runtime errors we would have to encode
that proof in the type system. More precisely we have some
background theory like
'F is a field' implies 'F is an integral domain'
There is no need to encode proof of rule above. But we need
a set of rules like above and typesystem that is rich enough to
exclude runtime errors. Given that in mathematical computations
'no erorrs' may be an interesting mathematical problem I would
say that this is beyond current technology.
Note: in the long run I would like to improve "proving power" of
out typesystem to handle much more problems. But we should not
get too frustrated that we have no solution now -- the problem is
provably hard and the best we can get is partial solution (assuming
that we solve current problems we certainly will want to expand
into new domains and we will find out new problems).
--
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.
