Thank you for the answer. The implementation of lambda calcuus can be related with logic under the ideas behind Curry-Howard isomorphism [1]. You can take a logic formula and relate it to a type which can be related to a term in a variation of lambda-calculus. But i guess that there are other things in logic module to start working on before that.I will take a few days to finish some work (I am in my exams period right now) and read the code. I will write again as soon as I can to refine my proposal. Ezequiel [1] http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
> From: [email protected] > Date: Fri, 21 Feb 2014 19:33:00 -0600 > Subject: Re: [sympy] Logic Module, computarional theory and GSoC > To: [email protected] > > On Thu, Feb 20, 2014 at 9:08 PM, Ezequiel Postan > <[email protected]> wrote: > > Hi, my name is Ezequiel, I'm from Argentina, so first of all excuse my > > English. > > I am an advanced CS student and also a TA at Universidad Nacional de Rosario > > [0], I hope not bothering you too much asking a couple of questions about > > sympy. > > > > I would like to participate in GSoC this year and I am very interested in > > the logic module. I have some ideas, but I don't know if they are on the > > sympy project interest or scope. Some examples that I thought and some I > > read on your wiki are: > > - It would be nice to generate proof trees for propositional logic formulas. > > - also to extend the module so it can work with first orden logic and to > > manage some operations like normalization to Skolem, Prenex, among others. > > To add the generation and test of unifiers of two expressions, to ask for > > sets of free and bound variables, alpha-convert expressions, substitutions, > > and other kind of manipulations > > > > I would like to get more information about the observation you make in the > > wiki "This task is heavily tied to the assumptions system." [4] > > Yes, the assumptions system is currently the biggest user of the logic > module, and I anticipate it to stay that way. Any GSoC project to work > on the logic module will need to take the assumptions system into > account. > > Unfortunately, the assumptions system in SymPy is a bit of a mess. > There are two systems, the old (x.is_real and Symbol('x', real=True)), > and the new (ask(Q.real(x)) and assume(Q.real(x))`. The two systems > use completely different logic deduction systems as well. The old one > computes all deductions on symbols when they are instantiated using a > RETE algorithm, which is in sympy/core/facts.py. The new system uses > the SAT solver (which uses the DPLL algorithm), and some manual logic > in the handlers code. At https://github.com/sympy/sympy/pull/2508 I am > working on making them use only the SAT solver, but it is a long > process, and it has revealed a few deficiencies in the logic module > already. > > Issues aside, the very expressiveness of the logic module is essential > to the assumptions system. The more kinds of things we can express > with the logic module, and the ease with which we can express them, > the easier the assumptions system will be to use. The sets module is > also pretty heavily tied to this idea. > > In general with SymPy, our philosophy is that users should be able to > just express what they want in a way that makes sense to them, and > then it's our job to translate this into something that we can compute > with. > > > > > Also I don't know if the project is interested in computational theory, like > > implementing lambda calculus for example and the basic operations like > > alpha, beta and eta convertions/reductions/expantion, some related topics in > > type theory and intuitionistic logic could be extended in the future of the > > project. > > Perhaps. How heavily is this tied to the logic module? > > > > > As an example of experience (on these subjects) I wrote (with one friend) an > > implementation of Robinson's resolution method for First Order Logic [1] in > > Haskell. We implemented all stages from parsing, normalization to generation > > of a refutation tree. Also wrote a simple interactive text interface. > > > > I must confess that I don't have too much experience in Python, I know it's > > basics (syntax, flow control, exception handling), I know OOP theory but I > > am more like a functional programer (Haskell mainly). I have knowledge of > > quite many languages like Haskell, ML, C, Prolog and have used Scilab, > > Pascal, C++, Coq and R. I believe I can get all I need for the begining of > > the coding stage. I worked in "fairly big" projects like NachOS (in C/C++ > > learning C++ on the fly) [2] and I am working in the Tiger compiler project > > in ML [3] (learned ML on the fly again) now. > > Learning Python shouldn't be difficult then. You don't need to know > everything to get started. It can't hurt to have a little Haskell > influence in SymPy too :) > > > I never worked in an open source project, and I am trying github for the > > first time now. Reading your documentation I couldn't find a guide on how to > > read the code of sympy, maybe I am bad at searching but I would like to ask > > for a little help on that (I would like to get familiar with the code, > > structure, style...) > > The best way is to find some issue to fix (you'll need to do this > anyway, as it's required for GSoC), and to look into fixing it. That's > really the best way to learn any codebase, in my opinion. > > We are currently migrating issue trackers, so you'll want to search > for issues at both https://github.com/sympy/sympy/issues?state=open > and https://code.google.com/p/sympy/issues/list. Both have "easy to > fix" labels if you want to start with something easy. > > Aaron Meurer > > > > > I know (suppose) you can't guarantee you will take me for GSoC in this > > project, but if anything I proposed is usefull for sympy I would like to get > > familiar with it. > > > > Thank you for your time and excuse my English again > > > > Regards > > > > Ezequiel > > > > [0] UNR Computer Science Licenciatura web page (in Spanish): > > http://www.fceia.unr.edu.ar/lcc/ > > [1] http://en.wikipedia.org/wiki/Resolution_(logic) > > [2] > > http://en.wikipedia.org/wiki/Not_Another_Completely_Heuristic_Operating_System > > [3] https://www.cs.princeton.edu/~appel/modern/ml/ > > [4] https://github.com/sympy/sympy/wiki/GSoC-2014-Ideas > > > > -- > > You received this message because you are subscribed to the Google Groups > > "sympy" group. > > To unsubscribe from this group and stop receiving emails from it, send an > > email to [email protected]. > > To post to this group, send email to [email protected]. > > Visit this group at http://groups.google.com/group/sympy. > > For more options, visit https://groups.google.com/groups/opt_out. > > -- > You received this message because you are subscribed to the Google Groups > "sympy" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To post to this group, send email to [email protected]. > Visit this group at http://groups.google.com/group/sympy. > For more options, visit https://groups.google.com/groups/opt_out. -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/sympy. To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/BAY174-W20CA1ABDE5A30E483A6D5899860%40phx.gbl. For more options, visit https://groups.google.com/groups/opt_out.
