> In trying some apparently-equivalent
> expressions, I find that the handling of equality and
> inequality is complicated, and incompletely described
> by the available documentation.
Robert,
I agree this is confusing. Let me start with the *explanation* (not a
defense) of the current behavior. (Your sinc_FOO_nois test shows this
all pretty clearly, but I'll be a bit more explicit.)
You are seeing the semantics of evaluation of boolean expressions here.
Since the semantics of Maxima evaluation in general are nowhere defined,
it's not surprising that the semantics of relations and conditions are
nowhere defined....
Relations (=, <, EQUAL, ...) are normally treated as declarative, so
that it is possible to write and manipulate equations and inequations.
Just as you can write the equation x^2+a=y, you can write the inequation
x^2+a>y. Both can then be manipulated with Subst, Part, etc. (but
unfortunately not Solve).
To ask Maxima to evaluate a condition against its mathematical knowledge
and its inequality database, you write IS(...). So:
x^2 > -1 => x^2 > -1 (a declarative statement)
is(x^2 > -1) => true (evaluation giving a boolean)
x > y => x > y (a declarative statement)
is(x>y) => ...error... (cannot resolve to a boolean value)
Since conditionals (if, while, ...) are control structures, not
declaratives, Maxima requires their protasis to evaluate to a specific
boolean, and thus implicitly calls "is" on the protasis.
Maxima does not support unevaluated boolean connectives (and, or, not),
and similarly implicitly calls "is" on their arguments. If you change
your definition A to
A(x,y):=true and EQUAL(x,y)$
or
A(x,y):=is(EQUAL(x,y))$
or
A(x,y):=not not EQUAL(x,y)$
you will see that it now behaves consistently with the others.
--------------
Now for the discussion. There are lots of things you could do with
simplifying (rather than evaluating) IF, AND, etc. It would be nice to
be able to say:
cond: x>0 and y>0 => x>0 and y>0
subst([y=x],cond) => x>0
subst([x=x^2+1,y=x],cond) => true
or (assuming nothing is known about x)
cond: if x>0 then a else b => if x>0 then a else b
subst([x=x^2+1],cond) => a
But there are some interesting questions here. Normally, simplification
and evaluation are orthogonal. Even if something is a noun form, it
evaluates its arguments. So we have
a: 3
expr: sin(a+b) => sin(3+b)
expr, b=-2 => sin(1)
Now what do you do with a simplifying IF? In simple cases, there's no
problem:
myabs(x):= if x>=0 then x else -x$
Then
myabs(a) => if a>=0 then a else -a$
And you'd hope to get some nice simplifications:
myabs(-a^2) => if (-a^2)>=0 then -a^2 else -(-a^2)
=> if (-a^2)>=0 then -a^2 else a^2
But since sign(-a^2)=NZ, this can simplify to:
=> if equal(a,0) then -a^2 else a^2
and since you can assume(equal(a,0)) in the then-clause, this can
simplify to:
=> if equal(a,0) then 0 else a^2
and since a^2=0 when a=0, the two clauses are equal and can be collapse:
=> a^2
Isn't that nice? Of course, it's all a fantasy, since none of these
simplifications is currently implemented. But they could be.
Now let's look more closely at the evaluation here. All three clauses,
the if-clause, the then-clause, and the else-clause must be evaluated so
that x takes on the value a.
But in the normal semantics of if-statements, either the then-clause or
the else-clause is evaluated, never both. After all, when we write
if equal(x,0) then 1 else 1/x
we don't expect the 1/x to be evaluated (and cause an error) when x is
equal to zero.
Even when we are *not* evaluating, but only simplifying, we have a
problem. Let's quote the above expression to block evaluation:
expr: '(if equal(x,0) then 1 else 1/x)
Now, we expect to be able to manipulate this expression in the usual
ways. For example, subst([x=0],expr). But wait! That will produce
if equal(0,0) then 1 else 1/0
which will cause a divide-by-zero error in the simplifier. That's not
what we wanted, is it?
Or consider a recursion:
fact(n):= if equal(n,0) then 1 else
n*fact(n-1)$
This works fine for fact(2). But what happens when you try fact(a)?
There is no problem in evaluating the if-clause and the then-clause, but
what about the else-clause? Evaluating that will result in a recursion,
giving (if it ever returned):
if a=0 then 1 else
a*(if (a-1)=0 then 1 else
(a-1)*(if (a-2)=0 then 1 else ...
There is no good reason to stop the recursion at any particular point.
After all, if we'd declared assume(equal(a,2)) then it would in fact
nicely terminate, returning 2! = 2*1 = 2.
The And and Or operations in Maxima have similar problems since they
have short-circuit semantics -- that is, (equal(x,0) or 1/x > 1) does
not cause an error when x=0.
I am not saying all these things are not soluble with some appropriate
design. What I am saying is that it *does* require non-trivial design
and implementation, and that the current (interim?) solution is not as
simple-minded as you might think. I do agree, though, that it is hard
to explain. Probably the best explanation is to say that if-clauses,
while-clauses, and AND, OR, and NOT have an implicit IS(...). I would
also simply recommend that users avoid AND, OR, and NOT except in if-
and while-clauses.
-s