Logic Module, computarional theory and GSoC

[Ezequiel Postan]

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]

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.

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.

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...)

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

[Aaron Meurer]

On Thu, Feb 20, 2014 at 9:08 PM, Ezequiel Postan
<ezequie...@hotmail.com> 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 sympy+un...@googlegroups.com.
> To post to this group, send email to sy...@googlegroups.com.
> Visit this group at http://groups.google.com/group/sympy.
> For more options, visit https://groups.google.com/groups/opt_out.

[Ezequiel Postan]

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