[GSoc] Assumptions System

[Rigel Bezerra de Melo]

Hi,

First I quick introduction. My name is Rigel Bezerra de Melo, I am a senior Computer Science student at Federal University of Campina Grande, in Brazil. I am really into Algorithms and Data Structures. As a hobby, I like contests like TopCoder, Codeforces, etc. As previous professional experience, I have interned last year at Microsoft. Also, I have studied abroad at UC Berkeley.

I really really want to do a GSoC with you guys. I always thought the symbolic capabilities of Mathematica were awesome, but always looked for alternatives, as I am FOSS enthusiast. I came across sympy a few months ago, while doing stuff in graph theory (yeah, I know, sympy doesn't have graph theory capabilities). Soon I discovered the number theory features and was amazed.

By far, the project idea the really strike me as working in the Assumptions system. I know this system will be highly tied to the Set Theory system, as lots of people have already pointed out. But I think you guys are all thinking the inverse way of organizing it. It looked to me like you guys wants to do the Set Theory system dependent of the Assumptions system, but it should be the other way around! My idea of what would be a perfect organization of Assumptions, Set Theory an Formal Logic is:

1. Formal Logic system is the base for everything. It is totally independent. In its core, it will have Propositions, and will decide on them.

2. Set theory system depends on the Formal Logic one. I think the most useful feature of Sets in symbolic calculations is testing pertinence. I mean, I think that by far, that would be the most common ultimate goal of using it. Having it depending on the Formal Logic allow as to construct Sets from Propositions (the Set of all elements the satisfies the Proposition). The would make the code of deciding pertinence only a matter of calling the Formal Logic system to check satisfaction.

3. The assumptions system should depends on the Set Theory system. I think that, in the core, all assumptions should be of the type "x in S", where S is a Set. That would have 2 advantages. First, the code for assumptions is already done, because all we have to do now is convert Expressions to Set pertinence assumptions (things like "x > y" = "x-y in Z+", "x in A" and "x in B" = "x in A^B"). Asking would them be only a matter of evaluating pertinence, what would call the formal logic system to decide satisfaction over propositions, that is the guy that should know about this kind o thing. The second advantage is that, now that there is not much logic left in the assumptions system, we can spread the assumptions everywhere. I mean, all packages should add their our set of assumptions. There is a prime_number basic assumption, but prime numbers make only sense in the number theory context. Is number theory special? Is there other number theory assumptions that should be added? Is there other packages with "same importance" assumptions? To me, the answer is No, No and No. I think the right way to do it is, the number theory module have Prime Number Set, them a prime_number assumption based on this set. Now, with you care about prime numbers and stuff, you import the number theory package, and get it all.

I know those ideas may be a little bit of diverging from what you guys are building. That's why I would like to work on the assumptions system now (it seems like you guys need help removing the old system). That way I would get a deeper understanding of the assumptions system and re-work these ideas in my head.

Sorry for the long message.

Thanks.