oldk1331 wrote:
>
> Another angle to see this problem:
>
> In theory, every Euclidean domain is a unique factorization
> domain, but in FriCAS, it's not.
>
> In an email one year ago, there's discussion about it:
> https://groups.google.com/forum/#!topic/fricas-devel/mMmm9zmC7io
>
> > There are principal ideal domains where all functions
> > exported by PrincipalIdealDomain are computable, but
> > factorization is not computable. In other words,
> > factorization in such domain is not constructive.
> >
> > Currently FriCAS contains no such domain, and it is
> > not clear if it ever will. But the logical distinction
> > makes sense.
>
> I want to clarify it a bit more:
>
> Are there Euclidean domains which have non-computable
> factorization?
>
> The proof that every PID (thus EUCDOM) is a UFD is not
> constructive, but for every constructive PID (EUCDOM),
> can people write a factorization algorithm for them?
> (That's different from "build a factorization algorithm from
> the exports of PID/EUCDOM".)
Define constructive. One possiblity is ring where ring
operations are computable. In such case we can give example
of a field (hence EUCDOM) such that polynomial factorization
in non computable. Namely, K = Q(S, x_1^2, x_^2,...)
where S is a subset of {x_1, x_2, ...}. In a field
polynomial y - a is reducible if and only if a is a square.
So, polynomial factorization implies computability of
square roots. However, in K above a = x_i^2 has square
root if and only if x_i \in S. So computable polynomial
factorization implies that S is recursive. Now, take
recursively enumarable S. Such S is relevant for
compoutations: in principle any element of S can appear
in computation. But factorization is non-computable in K.
Note that above K is subset of F = Q(x_1, x_2, ...) so field
operations are computable, but using F as representation
given x \in F it is not computable if a \in K. But one
can easily correct this: take as representation pairs
(a, c) where a in F and c is proof that c \in K. Since
S is recursively enumerable for each a in K there exists
a proof that it belongs to K and checking proofs is
computable.
--
Waldek Hebisch
--
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 fricas-devel+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
