Christian Muise wrote:
Hey Fabian (et al),
Thanks for the summary here on the assumption system -- I was going to
ask for exactly this later tonight ;).
I'm definitely interested in working on this for SoC. My long-term
goal is to be a regular contributer to sympy.logic, and until just
recently I had no idea how deep the logical system actually ties sympy
together with this assumption system. It's basically set up to be a
general existential theorem prover, right?
exactly. If you look closely at the code in ask.py, you see that at the
end it just checks the satisfiability or (!premise ^ known_facts) or
(premise ^ known_facts).
(1) ask(x*y, Q.even, Assume(x, Q.even) & Assume(y, Q.integer))
...looks like...
(2) (\exists x,y). [even(x) && integer(y)] \implies even(x*y)
yes, but there is no notion of quantification. If is all translated into
a problem of propositional logic.
This is all quite exciting to me since it's so related to the field
I'm currently in (working on a PhD in Knowledge Representation &
Reasoning and spent the last two weeks formalizing stuff in 2nd order
logic :p). To specifically address some points and ask some pointed
questions:
- Performance:
The known_facts_compiled a list of conjuncts or disjuncts? Either way,
you're compiling initial information that you'll be querying about into
some sort of normal form, and I've done quite a bit of work in theory
compiling for just that sort of thing. We may be able to speed things up
substantially by computing prime implicants or implicates or even
something more exotic such as d-DNNF. It all depends on the type of
queries the assumption system will face, but there's definitely lots
that can be done here.
Indeed. Unfortunately I'm not an expert in the field, so I don't know
what direction would be best.
- Scalability:
I've done some work in SAT encodings for planning problems...one huge
improvement there (since incremental SAT problems are produced) is to
keep around clauses that are learned previously in a clause learning
setting (good clauses can be good as gold for SAT-solving). If / when
the DPLL solver in sympy gets clause learning (something I can do as
well), then this would play a role for repeated queries.
- API:
If you want a more natural way to express things, maybe something
based on the above form (2) would work:
(ask(x, Q.integer,Assume(x, Q.rational)))
...becomes...
exists(x, rational(x) >> integer(x))
I do not have a clear opinion on this.
The function rational, integer, etc (or whatever they would be named)
would return True or False based on the value of x. It reads nicer to
me, but maybe not so much for those outside logic ;).
- Assumption Status:
I didn't realize that there was a new assumptions fork. Would the
scope of the SoC project be picking up from that point? Where should the
proposal target? (eg. proposing a new way to integrate, proposing to
continue the integration, etc) Would working on this take work away from
someone else already dealing with assumptions? (ie. Fabian or Ronan)
- py2to3:
There seems to be an emphasis for the PSF on this. I would hate to
fail at getting a spot just because I didn't put forward a 2->3
proposal. Anything that helps out the project (and I'm capable of doing)
would be great for me, but is there any way to merge the two projects?
Will the 2->3 conversion be an extensive process or just a little elbow
grease? If the latter, then is a multi-tiered application acceptable or
should separate applications be put forward?
---------
Again, thanks for putting this summary out. It helps clear things up
quite a bit.
Cheers,
Christian Muise
On Tue, Mar 23, 2010 at 1:10 PM, Fabian Pedregosa <fab...@fseoane.net
<mailto:fab...@fseoane.net>> wrote:
Hi all.
Since some of you are willing to improve the logic and assumption
system, I'll just say my opinion on the current state of these modules.
The logic framework (sympy.logic) in my opinion is ok. Sure, it could be
improved with quantifiers (first-order logic) and other niceties, but
overall it fulfills its purposes, and after 6 months I believe it is
considered API stable.
On the other hand, I am not at all happy with the assumption system that
I coded. It works, but there are some places that surely could be
improved:
- Performance. I have to restore to ugly hacks to have an acceptable
performance. See known_facts_compiled in assumptions.ask
- Scalability. When the size of the known_facts database grows, the
performance grows exponentially. Plus, each time there is a query, a
Satisfiability solver is run over *all* variables. There are algorithms
that use previous knowledge to run faster.
- API. The API is cumbersome and far too verbose (ask(x, Q.integer,
Assume(x, Q.rational) just to query if a rational is an integer).
Unfortunately, I do not know a better one.
The old assumption system
-------------------------
Having the old assumption still around is a pain, but the core is
extremely fragile and removing the old assumption and plugging the new
one is not a trivial task.
The HOWTO is rather simple: you remove the inheritance of Basic from
AssumeMeths, that is where all the old assumption framework is
encapsulated, and you start fixing tests.
See this commit for an example on how this could be done.[1]
Now you have two kinds of bugs. One type is derived from the fact that
the new assumption system supports less keys than the old one. This is
done because in the new system I removed all keys that where redundant
or could be derived from others. See also [1] for an example on how this
could be done. Note that you will have to re-generate
known_facts_compiled each time you add new keys.
The other type of bugs are bugs that come from the fragility of the core
and are bugs that give strange (or simply different) results for things
that apparently have nothing to do with the core nor with the assumption
system. These bugs are really painful to solve and will likely not be
solved unless there is a real interest in the community and someone who
understands the core (Ondrej?) is willing to work on this.
Note that also Ronan Lamy (search in this list) tried to remove the old
assumption system by splitting Basic into two subclasses, although I do
not know how far that effort went.
[1]
http://github.com/fseoane/SymPy/commit/2343cdac1023e0205a8db8c2a326312350268ae5
Cheers,
--
You received this message because you are subscribed to the Google
Groups "sympy" group.
To post to this group, send email to sympy@googlegroups.com
<mailto:sympy@googlegroups.com>.
To unsubscribe from this group, send email to
sympy+unsubscr...@googlegroups.com
<mailto:sympy%2bunsubscr...@googlegroups.com>.
For more options, visit this group at
http://groups.google.com/group/sympy?hl=en.
--
You received this message because you are subscribed to the Google
Groups "sympy" group.
To post to this group, send email to sy...@googlegroups.com.
To unsubscribe from this group, send email to
sympy+unsubscr...@googlegroups.com.
For more options, visit this group at
http://groups.google.com/group/sympy?hl=en.
--
You received this message because you are subscribed to the Google Groups
"sympy" group.
To post to this group, send email to sy...@googlegroups.com.
To unsubscribe from this group, send email to
sympy+unsubscr...@googlegroups.com.
For more options, visit this group at
http://groups.google.com/group/sympy?hl=en.
