最大值事实如何运作？为什么负数减去正数也不是负数？

Question

我是maxima的新手。我对 maxima 中的基本事实感到困惑。

% maxima
Maxima 5.46.0 https://maxima.sourceforge.io
using Lisp SBCL 2.3.3
...
(%i1) assume( S >= 0, IS < S );
(%o1)                          [S >= 0, S > IS]
(%i2) asksign( IS - S );
(%o2)                                 neg
(%i3) asksign( IS - S - 1 );
Is S - IS + 1 positive, negative or zero?

如果我从一个负数中减去 1，结果不应该也是负数吗？

有人可以向我解释一下 maxima 的想法以及我如何说服它相信正确的事情吗？ （这在我想要执行的某些集成中很重要，集成会问我同样的愚蠢问题。）

Answer 1

Maxima 从声明的不等式推论的系统不是太强大。据我所知，声明的集合（在讨论这个东西时统称为“假设数据库”）被构造为一棵树，并且确定正在考虑的表达式的符号与遍历树有关，也许应用一些启发式方法。

我说“据我所知”是因为 assume 数据库被广泛认为是代码库中比较晦涩的部分之一——这可不是一件容易的事。它对于简单的案例工作得很好，而且速度非常快，但很容易遇到处理不好的案例。

报告的行为可能是也可能不是错误，因为假设的行为没有很好地指定，但无论如何它是一个明确的缺陷；我将发布有关它的错误报告。

至于现在如何解决它，也许可以说

assume(c < 0)

然后在整个过程中用

c

代替

IS - S

。一种方法是说

subst(IS = c + S, <expr>)

——这对文字

IS - S

以外的表达式有预期的效果。