A bit of background, since you don't know. I worked on SymPy for GSoC last summer on the ODE solving module. I decided to continue as a developer afterwords, and I hope to apply again this year (though I need to come up with a project idea first. If I can't, I might try to be a mentor). I am an undergrad at New Mexico Tech double majoring in Mathematics and Computer Science.
It sounds to me like any of these would make a good project. As far as stepping on Ronan's/Fabian's toes, we will have to wait to hear back from them, but I don't think it will be an issue. Fabian's GSoC project last summer was to implement the new assumptions, but he didn't get to merge it in. Since then, we have been trying to do some work on that, but not much has been done. This is partly because people are busier this time of year, because Fabian is the only one who really understands the new system, and because of some of the reasons outlined in Fabian's original email here. We would all like to see it get merged in, so I don't think there would be much objection to a project to do that. As for 2to3, this also concerns me. All students wishing to work on SymPy should apply to both PSF and PSU. So with any luck, if PSF doesn't like your idea because it doesn't relate to Python3, then PSU will be more forgiving :). If you see any other organizations that might be interested in working as an umbrella, be sure to let us know. I don't think much else could be done in a 2to3 project, though I haven't looked into it very deeply. There are some non-trivial changes that need to be done (e.g., remove all cmp-based function in favor of key-based functions), and we also need to develop a strategy for developing for both python2 and python3 in parallel (e.g., some kind of automated use of 2to3, improved buildbots). By the way, I am +1 on taking advantage of unused python symbols such as >> to make syntax simpler. Things are actually not too bad if you use Q in conjunction with IPython's tab completion. Aaron Meurer On Mar 23, 2010, at 1:37 PM, 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? > > (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) > > 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. > > - 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)) > > 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> 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 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. -- 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.
