Bill Page wrote:
>
> On 25 November 2014 at 14:05, Waldek Hebisch <hebi...@math.uni.wroc.pl> wrote:
> > Bill Page wrote:
> >> I propose the following patch:
> >> + if (F has conjugate : F -> F) then
> >> + localReal? x == x = conjugate(x)
> >> + else if (R has imaginary : () -> R) and (R has conjugate : R -> R)
> >> then
> >> localReal? x ==
> >> (u := retractIfCan(x)@Union(R, "failed")) case R
> >> and (u::R) = conjugate(u::R)
> >> -
> >> else localReal? x == true
> >
<snip>
> > However, I would rather move in direction
> > of removing unsoundness than adding more of it.
>
> That sounds obviously very sound to me ... so I wonder if you are
> suggesting my patch unsound?
Depends on definition of 'conjugate'. One resonable fefinition
of 'conjugate' on _functions_ is:
conjugate(f)(z) = conjugate(f(conjugate(z)))
Basicaly the definition means that we compute 'conjugate' on
real axis and continue analitically to complex plane. This
definition is useful if we want to use 'conjugate' on complex
valued functions of real variable, but also want to use
analytic continuation.
With such definition we have 'conjugate(z) = z' (here 'z' means
identity function!) and 'conjugate(sin(z)) = sin(z)'. But
this does not prevent the function to have complex values.
More naively:
(9) -> conjugate(z::Complex(Expression(Integer)))
(9) z
Type: Complex(Expression(Integer))
Note: Complex is not a FunctionSpace, so directly no
contradiction is possible, but I hope that this example
illustrates that your change introduces an assumption
which is undocumented and hard to verify.
> > To be more
> > precise: currently the assumption is made blindly regardless
> > of user wishes.
>
> If you are referring to the current default assumption of 'true', I
> agree that the long term goal should be to change this to 'false' so
> that 'localReal?' only returns 'true' when it can be determined that
> this is in fact the case.
Yes.
> > We should improve FriCAS to be able to do
> > more simplifications without extra assumptions
>
> Yes. I think my patch accomplishes this when used together with the
> introduction of 'conjugate'.
>
> > and to allow user specified assumptions
>
> In general I am against introducing a general mechanism for making
> assumptions such as "x is real", etc.
>
> > -- such changes should allow removing unsound assumptions without
> > loss of computing power.
> >
>
> I would prefer that any potential loss of computing power should be
> offset by enriching the algebra rather than depending on explicitly
> stated logical assumptions.
IMO "enriching the algebra" here must add ability to do
appropriate logical reasoning. Standard algebra rules
are equational, but such problems need condtional
rules and ability to simplify conditions. Some
conditions appear during computation, for example
integrate(1/x, x=1..2)
means that x is between 1 and 2. Some conditions
appear due to reasoning via cases: each case has
some conditions, together they cover the whole
space. But user may also want to specify that
for exaple in
limit(exp(-a*x), x = %plusInfinity)
a is positive. We need to handle that anyway, so
why to force user to write something like
limit(exp(-exp(a)*x), x = %plusInfinity)
In general, each computation should be done in context
containing known (or assumed) facts. Context should
change during computations, for example case splits
should introduce extra assumption, perform subcomputation
and then retract the assumption.
Challenges are:
- choose useful form of conditions. Very general one, like
full logical formuls cause computational problems. Simple,
like 'is_real', 'is_integer', etc. may be too weak.
- efficient implementation of contexts: we need to search them,
add and retract condtions. There is danger that context will
be big.
- reasoning on conditions: if we require that exact condition
is in the context, then we will miss many fact implied by
the context and the condition system will be of little use.
so we need some inference. At least we want to infer from
2 < x that 1 < x. But it would be nice to deduce from
1 < x < 2 that 0 < sin(x) and similar.
- scope of conditions. FriCAS treats different types as
independent entities, so at first one may think that
0 < x in Expression(Integer) does not mean that
0 < x in Expression(Fraction(Integer)). But expressions
get passed between types and conditons should travel
with expressions. So either we make conditions typeless,
or we need a method to convert conditions between types.
I must admit that ATM typeless conditions looks more atractive
to me: most computations does not affect conditions, so
with typeless conditions we can add condition handling
just to some selected places. With typed conditions I do
not see how to avoid propagating them explicitely (which
could double the size of algebra due to needed boilerplate).
--
Waldek Hebisch
hebi...@math.uni.wroc.pl
--
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 http://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
