On Feb 12, 2008 1:35 PM, Robert Dodier <robert.dodier at gmail.com> wrote:
> db.lisp is an incomprehensible mess. I don't think it is doing
> anything very complicated (to judge by the weakness of the
> assume system). Let's start thinking about how to replace it.
>
The weaknesses of assume/is have fairly little to do with the DB, which is
simply a representation of a partial order. Any additional algebraic,
logical, or mathematical intelligence comes from outside DB. I am not sure
whether you're proposing to change this interface.
One of the reasons it's hard to understand is that the obvious
representation of linked structures in Lisp gives you circular lists, which
(even with nice pretty-printing) are hard to understand. So debugging and
tracing are a mess. Perhaps the first step is writing a special-purpose
printer for these structures....)
Let's think about the desired functionality, which should probably be a
superset (strict or not) of the current functionality:
-- represent <, <=, =, and # relations between expressions
-- make partial order inferences using those relations, a<=b and b<=c and
a#b implies a<c
-- given an assumption X, it must be possible to remove it without modifying
other assumptions, regardless of the order in which they were added and
whether they overlap logically
-- (new functionality) it would be nice to be able to add/remove *redundant*
assumptions -- perhaps identified by some sort of unique ID, so that you
could do assume(x>0) => %rel_x1, assume(x>0) => %rel_x2, forget(%rel_x2)
(is(x>0) would remain true); forget(%rel_x1) (is(x>0) would no longer be
true)
-- (new functionality) it would be nice to handle logical combinations of
assumptions, e.g. assume(a<0 or b<0); but this is perhaps outside the scope
of DB
-- it must be possible to group assumptions into contexts which can be
activated or deactivated relatively efficiently
--checking for a relation in the DB should be pretty efficient.
What am I forgetting?
-s