``update()`` producing wrong results

[LKlinke]

Currently Subtraction just use the linear_transformation() function for sympy generating functions. There is a sanity check that gives a warning if the operation might lead to incorrect results. One should check this and then compute the correct result using the monus variant.

[Legotier]

Fixed by 9ac4bec867ac1b92a345b9cec055b1634ae9064f, I think. I'm not sure if it's 100% correct, the tests seem to work though.

[Legotier]

It is possible that the solution right now only works for finite functions. I don't know how to make it work for everything though.

[Legotier]

(This is mainly just a reminder for myself, and I think I already know how to solve this problem. Still, it may be interesting to some people)

I noticed a problem while implementing monus: Addition (and by extension subtraction) with the monus operation is not commutative and/or associative.

For example, consider the following code:

result = prodigy.analysis.compute_discrete_distribution(
    pgcl.parse_pgcl("""
nat n;
n := n-6+1;
"""), GF("n^5"), prodigy.analysis.ForwardAnalysisConfig())
assert result == GF("n", "n")

This should pass, because we first subtract 6 from n, which means it is 0, and then add 1, meaning n is 1 with probability 1. However, sympy simplifies this expression to n-5, meaning the result we actually compute is the GF 1.

However, even if we can somehow tell sympy not to simplify this expression, it still persists because there seemingly is no easy way to get the operations of a sympy expression in order. For example, the following code should pass as well:

result = prodigy.analysis.compute_discrete_distribution(
    pgcl.parse_pgcl("""
nat n;
nat m;
m := 3
n := 1;
n := n-m+1;
    """), GF("n^5"), prodigy.analysis.ForwardAnalysisConfig())
    assert result == GF("m^3*n", "n", "m")

But this doesn't pass, because sympy doesn't tell us that m is subtracted before 1 is added.

[LKlinke]

I See the issue and very well seen! That is a very good observation the have to take care of.

[Legotier]

The problem with associativity / commutativity is fixed by a025d4b46148e65268e6a739381f3c908a33c605. However, this leads to other problems, since we don't use sympy's simplification anymore (see c91890101fd6b3d41f81b78cc2eae89fec865015). I don't know how to implement a solution that solves all conceivable problems.

[LKlinke]

The problem with associativity / commutativity is fixed by a025d4b. However, this leads to other problems, since we don't use sympy's simplification anymore (see c918901). I don't know how to implement a solution that solves all conceivable problems.

The problem with associativity / commutativity is fixed by a025d4b. However, this leads to other problems, since we don't use sympy's simplification anymore (see c918901). I don't know how to implement a solution that solves all conceivable problems.

I think we should not do it that way as it introduces the error test cases described in (see c918901). Better document pretty well that subtraction is not associative. And one carefully has to describe subtraction by using parentheses.

One Question: Is subtraction associative if we do a proper minus and not the monus operation? So, basically the user should take care that program variables cannot get negative values (as we describe prodigy as a tool for discrete non-negative integer probabilistic analysis tool).

[Legotier]

Better document pretty well that subtraction is not associative.

That's the problem, sympy doesn't know this. So even if the user knows that subtraction is not associative (and, in the monus case, also not commutative), if we parse the expression n-6+1 for example using sympy, this is automatically simplified to n-5. I know that we can tell sympy not to do this, but even then, there doesn't seem to be a way to actually get the operations in the correct order, i.e., to know that we actually want to compute n-6+1 and not 1-6+n for example. So we have to somehow get the operations in the correct order to even be able to compute the correct result. I don't think using parentheses is sufficient for this.

Is subtraction associative if we do a proper minus and not the monus operation?

Unless I'm misunderstanding, isn't this obviously false? For example, $a - (b - c) = a - b + c \neq (a - b) - c$.

[Legotier]

The associativity / commutativity problem does not only exist in the linear_transformation function. The following code fails as well:

gf = GeneratingFunction("n^5")
assert gf.get_expected_value_of("n - 6 + 1") == "1"

[Legotier]

This has been fixed for a while now, if there are still errors they are unrelated to this thread