prodigy.distribution.equality

Three-valued equality of SymPy expressions: proven equal, proven different, or unknown.

An engine’s == must never claim equality without proof (#117), so for non-rational expressions it answers False when it merely cannot prove equality. Checks such as the EVT fixed-point equation need to tell “provably different” from “not proven” apart (#123); decide_equal() gives that answer.

is_rational_over_q(expr)[source]

Whether expr is built from symbols and rational numbers with +, * and integer powers only, i.e. it is a rational function with rational coefficients. Constants such as sqrt(2) or pi and floating-point numbers are excluded: for them, exact cancellation is not a decision procedure.

Parameters:

expr (Expr)

Return type:

bool

decide_equal(lhs, rhs, use_simplify=True)[source]

Decides lhs == rhs as an identity in all symbols.

Return type:

bool | None

Returns:

True if equality is proven, False if inequality is proven, None if neither.

  • Floating-point numbers make arithmetic inexact (1e20 + 1 - 1e20 is 0), so expressions containing them are only equal if they are identical; otherwise the answer is None.

  • The difference is put over a common denominator and cancelled. This is exact polynomial arithmetic over the rationals in which every non-rational subterm (e.g. exp(p*x)) is an indeterminate, so a zero result proves the difference zero. If the difference is a rational function over the rationals (is_rational_over_q()), a nonzero result proves it nonzero.

  • Otherwise (only if use_simplify) SymPy’s Expr.equals may prove equality: it returns True only if simplify turns the difference into 0 or, for constant differences, by an algebraic proof (minimal polynomials). Its False comes from evaluation at random points and is no proof, so it counts as None.

Parameters:
decide_equal_strings(lhs, rhs, names)[source]

Like decide_equal() (without simplify) for the string forms of two engine expressions, e.g. of SymEngine or GiNaC. names are the variables and parameters; they are parsed as plain symbols, so names such as E or S keep their meaning. Decimal literals stay floating-point numbers, so expressions containing them are never decided different. Unparsable strings give None.

The strings must come from an engine, not from the user: SymPy’s parser evaluates Python code.

Parameters:
Return type:

bool | None