unevaluated boolean and conditional expressions (take 1)

Richard,

Thanks for your comments.

> Seems useful in some context, but...

I claim these changes are generally useful.

At present undecidable predicates yield an error or unknown
(depending on the prederror flag). The revised code makes
simplification and evaluation of predicates analogous to that
of arithmetic expressions: work towards a definite result,
but return a partially evaluated expression if you don't get there.

The weight of history aside, I don't see any reason to banish
unevaluated boolean and conditional expressions,
when we allow unevaluated arithmetic expressions.

> not(c<1)  does not mean  c>=1  for all c in Maxima.
> For example, c=3+4*%i.

At present, not c < 1 => "unable to evaluate the predicate"
when c is bound to itself. The point of the current proposal
is to get an interesting / useful result in that case,
and analogous cases involving and, or, and if.

not 3+4*%i < 1 yields an error at present, and also with the
revised code. Changing that is not within the scope of
the current proposal.

The examples are literal, not general; I didn't mean to
imply that they hold for all values of a, b, c, and d.
I guess prefacing the examples with kill (a, b, c, d)
would clarify that point.

> So there is an implicit assumption that a,b,c are from an ordered
> field, or perhaps from the real numbers.  Maybe this should be
> explicit. e.g. have your simplifications within a context of some sort..

The revised code isn't making any assumptions not already
implicit in the input. E.g. if you write c < 1, it is implied that
c would be comparable to 1, if ever it were assigned a value,
therefore not c < 1 => c >= 1 is not any less jusified than c < 1.

> How far are you going with geometric inequalities?

I'm not sure what you're getting at here.

Here are some more examples.

kill (a, b,c, d, e);
ev (a and b or c and d, a=true, c=false) => error or unknown
a > 1 and a > 1  => error or unknown
a > 1 and 2 > 1  => error or unknown
a > 1 or 2 > 1  => error or unknown
ev (if a then b elseif c then d else e, a=false) => error or if unknown ...

and / or don't commute in obvious cases at present:

a > 1 or 2 > 1 => error or unknown,
2 > 1 or a > 1 => true

Here are the results returned by the revised code
for the above examples. In each case, I claim
the result returned by the revised code is more generally
useful than the result returned at present.

ev (a and b or c and d, a=true, c=false) => b
a > 1 and a > 1  => a > 1 and a > 1 (yes, more simplification is
possible here ...)
a > 1 and 2 > 1  => a > 1
a > 1 or 2 > 1  => true
2 > 1 or a > 1 =>  true
ev (if a then b elseif c then d else e, a=false) => if c then d else e


Hope this helps,
Robert Dodier