Should facts() show duplicate facts?

I found this while working on bug #5120, and it surprised me, so I suspect
it will surprise others too: The fact database can hold the same fact more
than once, and facts() does not tell you.

assume(notequal(a, 0))$
assume(notequal(a*b, 0))$
facts();
  [notequal(a, 0), notequal(b, 0)]

forget(notequal(a, 0))$
facts();
  [notequal(a, 0), notequal(b, 0)]

The fact notequal(a, 0) existed twice, but facts() shows it only once. One
must call forget() twice for the fact to actually disappear.

The reason is that some assumptions are filed as several facts.
notequal(a*b, 0) is stored as notequal(a, 0) together with notequal(b, 0),
because that is the form the database can actually answer questions from.
These internal facts are stored even if the database already contained
them. On the other hand, trying to establish the same fact twice using the
user-level function assume() will answer [redundant] from the second time
on.

That second copy of the fact is not a bug, and I want to be clear about
that, because my first instinct was to call it a bug. It works as a "count
of reasons", and it is what makes this case come out right:

assume(notequal(a*b, 0))$
assume(notequal(a*c, 0))$
forget(notequal(a*b, 0))$
facts();
  [notequal(a, 0), notequal(c, 0)]

notequal(a, 0) correctly survives, because notequal(a*c, 0) still says so.
If the two assumptions shared a single entry, that forget would have taken
it away.

The one thing that does seem wrong is facts() not showing the duplicate
facts, and because it is the only window users have, the whole thing looks
inconsistent: forget() says it removed something, but then facts() says it
is still there. And forget(facts()) doesn't work as one might reasonably
expect.

My proposal is simply that facts() should stop suppressing duplicates.
forget(facts()) then becomes exact, and facts() agrees with what forget was
already reporting.

Duplicates appear only where there genuinely are two independent reasons
for the same statement, which is exactly the situation a user needs to know
about.

This doesn't cause any test failures. But it is a user-visible change, so
it would want a line in the manual saying a statement can appear more than
once when more than one assumption supports it. It changes nothing about
what assume means or what the database stores, only about what you are
allowed to see.

Is anyone opposed, or relying on facts() returning each fact at most once?

There is a larger question behind this about whether the database should
record what the user said or what Maxima knows, and the counting above is
an approximation of the former. I would rather leave that for another
thread and just stop hiding the count.

Best regards
David Scherfgen

_______________________________________________
Maxima-discuss mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/maxima-discuss