Logic

[Daishi]

Hi,

I'm interested in expressing and solving the following kinds
of questions in something like Sympy/Core. I've taken a quick
look at some of the code and it looks like the primary use-case
is more numeric rather than logic, but I'm wondering if it would
be appropriate to try to solve these kind of questions within
the Sympy framework:

1. Take a propositional statement and convert it into the
equivalent CNF.
2. Express a statement like "forall x in X: x%2 == 0" and then
apply it as a function to different domains X so that e.g.,
X = [1,2,3] => False and X = [2,4,6] => True.

I see that the logic.py module contains some basic code
which expresses n-ary predicates, but it wasn't clear to
me whether there was already support for expressing
conjunctions/disjunctions.

Thanks,
d

[Pearu Peterson]

Hi,

The logic subpackage currently implements only relational operations
but according to its design, one can express any predicate
using the Logic class. For example, conjuction and disjuntion
expression are represented as follows:

>>> from sympycore import *
>>> from sympycore.utils import AND, OR
>>> x,y,z,v,w=map(Logic.Symbol,'xyzvw')
>>> Logic(AND, (x,y))
Logic('x and y')
>>> Logic(OR, (x,y,z))
Logic('x or y or z')

sympycore used to use Quine-McCluskey algorithm to simplify
propositional expressions but we haven't had a chance to
reimplement it again after the major rewrite of sympycore in January.
But logic support is certainly in a top of sympycore todo list.

Regards,
Pearu

[Daishi]

Hi Pearu,

Thanks for your response!
I have a followup question regarding
substitution via .subs().

What I would like to have something
like the following:

Logic('x and y').subs('y', 'not x') => False
Logic('x%2==0 or x<10).subs('x', 3) => True

to parallel the existing:

Calculus('x+1').subs('x', 2) => Calculus('3')

Is this a reasonable and intended usage
of .subs() in the logic context?

Having investigated somewhat in this
direction, it appears that Logic and Verbatim
do not have _subs() defined. If I understand
things correctly, it would seem like _subs()
could be defined for Verbatim based on
simple replacement. The reason I ask this
is because a possible naive implementation
of _subs() for Logic seems to be to ask Verbatim
to do blind substitution, and to do an eval/simplify
pass on the result. Does this seem reasonable?

Thanks again,
d

[Pearu Peterson]

Hi,

I have now implemented subs support for Logic. Both of
your examples work now:

>>> Logic('x and y').subs('y', 'not x')

Logic('False')
>>> Logic('x%2==0 or x<10').subs('x', 3)
Logic('True')

and even this one:

>>> Logic('x>y and x<=y')
Logic('False')
>>> Logic('x>y or x<=y')
Logic('True')

Let us know if you need more basic functionality in Logic.

Regards,
Pearu

[Daishi]

On Apr 1, 4:53 am, Pearu Peterson <pearu.peter...@gmail.com> wrote:
> I have now implemented subs support for Logic.

Hi Pearu;

Thanks! I noticed two simple things:

1. Logic(True) != Logic('True')
(The LHS is a number, while the RHS is a symbol).
Given how generally sympycore seems to parse
string arguments it seems like this would be a nice
property to have.

2. >>> print Logic('True and False').as_tree()
Verbatim:
AND[
SYMBOL[True]
SYMBOL[False]
]

I expected this to simply be Logic(False).
I originally thought that perhaps this was due to the
issue in 1., but even if I explicitly do:

>>> print Logic(AND, (Logic(True), Logic(False))).as_tree()
Verbatim:
AND[
NUMBER[True]
NUMBER[False]
]

On the other hand, I'm not entirely sure that in general
logical sentences should be "simplified" unless explicitly
requested by the user, so perhaps this is the right behavior.

On a slightly separate note, it appears that .subs() currently
does an implicit 'eval' in addition to substitution, but that
sometimes this is short-circuited. Hence one observes
what seems like slightly odd behavior:

>>> print Logic(AND, (Logic(True), Logic(False))).subs([]).as_tree()
Verbatim:
AND[
NUMBER[True]
NUMBER[False]
]
>>> print Logic(AND, (Logic(True), Logic(False))).subs({'a':1}).as_tree()
Verbatim:
NUMBER[False]

Perhaps there should be a distinct .eval() separate from .subs()?
(Or have I missed it somewhere?)

Finally, my goal here to express some basic quantification.
It seems to add an operator within an Algebra what you do
is create an interned symbol for the head in utils.py and then
implement the operation within the Algebra, is that about right?

Thanks,
d

[Daishi]

On Apr 1, 6:48 pm, Daishi <dai...@gmail.com> wrote:
> 1. Logic(True) != Logic('True')
> (The LHS is a number, while the RHS is a symbol).
> Given how generally sympycore seems to parse
> string arguments it seems like this would be a nice
> property to have.

perhaps naively, i tried the following
patch to try to remedy this, but it appears
to only partially do the right thing.

>>> print Logic(True).as_tree()
Verbatim:
NUMBER[True]
>>> print Logic('True').as_tree()
Verbatim:
NUMBER[True]

>>> print Logic('True and False').as_tree()
Verbatim:
AND[
SYMBOL[True]
SYMBOL[False]
]

i.e., it works for the simplest case, but
not when actual parsing on the string
argument is done.

i did look and see that ultimately you are
using the compiler/ast modules to do the
string parsing. i'm not very familiar with
these modules, but my impression from
somewhat following python-dev and
python-3000 gossip is that the compiler
module is to be deprecated. i believe
the parser module is meant to substitute,
but it's quite possible that i don't fully
appreciate your use-case and the parser
module would not be suitable.

d


--- a/sympycore/logic/algebra.py
+++ b/sympycore/logic/algebra.py
@@ -40,6 +40,16 @@ class Logic(Algebra):

def as_verbatim(self):
return Verbatim(self.head, self.data)
+
+ @classmethod
+ def convert(cls, obj, typeerror=True):
+ if isinstance(obj, (str, unicode)):
+ obj_l = obj.lower()
+ if obj_l == 'true':
+ return cls.true
+ elif obj_l == 'false':
+ return cls.false
+ return super(Logic, cls).convert(obj, typeerror=typeerror)

def convert_operand(self, obj, typeerror=True):
head = self.head

[Pearu Peterson]

On Apr 2, 1:48 am, Daishi <dai...@gmail.com> wrote:
> Hi Pearu;
>
> Thanks! I noticed two simple things:
>
> 1. Logic(True) != Logic('True')
> (The LHS is a number, while the RHS is a symbol).
> Given how generally sympycore seems to parse
> string arguments it seems like this would be a nice
> property to have.

This is fixed in svn yesterday. The fix was to define
get_predefined_symbols() method for Logic.

> 2. >>> print Logic('True and False').as_tree()
> Verbatim:
> AND[
> SYMBOL[True]
> SYMBOL[False]
> ]
>
> I expected this to simply be Logic(False).

It should work now.

> I originally thought that perhaps this was due to the
> issue in 1., but even if I explicitly do:
>
> >>> print Logic(AND, (Logic(True), Logic(False))).as_tree()
>
> Verbatim:
> AND[
> NUMBER[True]
> NUMBER[False]
> ]
>
> On the other hand, I'm not entirely sure that in general
> logical sentences should be "simplified" unless explicitly
> requested by the user, so perhaps this is the right behavior.

The above is expected behavior.
In general, sympycore supports three ways of creating
symbolic expressions. I'll describe them below using Logic but
the idea applies also to other Algebra classes:

1) Logic(AND, frozenset([x,y])) - returns Logic instance representing
`x and y` without
performing any canonization. Either the canonization is done by the
caller algorithm
or an user needs an uncanonized representation. So,
Logic(AND, frozenset([True,False])) -> `True and False`
This way of creating Logic instances is used by 2)

2) Logic.And(x, y) - returns Logic instance representing `x and y` but
also performs
basic canonization. An important note is that `x` and `y` must be
boolean expressions.
So,
Logic.And(True, False) leads to an exception.
This way of creating Logic instances is used by algorithms and by 3)

3) And(x, y) - returns Logic instances representing `x and y`. It
converts `x` and `y`
to Logic instances and performs basic canonization (by calling
Logic.And).
This is what users should use to create boolean expressions. So,
And(True, False) -> `False`

Note that Logic defines two number-like instances representing the
True and False values.
They are available via Logic.true and Logic.false, and are actually
equal to Logic(NUMBER, True)
and Logic(NUMBER, False), respectively.

> On a slightly separate note, it appears that .subs() currently
> does an implicit 'eval' in addition to substitution, but that
> sometimes this is short-circuited. Hence one observes
> what seems like slightly odd behavior:
>
> >>> print Logic(AND, (Logic(True), Logic(False))).subs([]).as_tree()
>
> Verbatim:
> AND[
> NUMBER[True]
> NUMBER[False]

This is expected because of 1) above.

> ]>>> print Logic(AND, (Logic(True), Logic(False))).subs({'a':1}).as_tree()
>
> Verbatim:
> NUMBER[False]

This is also expected because subs actually uses 2) above.

> Perhaps there should be a distinct .eval() separate from .subs()?
> (Or have I missed it somewhere?)

Yes, I think the descriptions of ways to create Logic instances should
cover this.

> Finally, my goal here to express some basic quantification.
> It seems to add an operator within an Algebra what you do
> is create an interned symbol for the head in utils.py and then
> implement the operation within the Algebra, is that about right?

Yes. I think that the head symbols defined in utils.py cover already
all needed cases that the parser can handle.

To create a new symbolic operator, say, Implies, one should define a
callable object `Implies` that is used as a head. For example,

class Implies(object):

def __new__(cls, x, y):
# perform basic evaluation and return simplified result
return Logic(cls, (x, y))

See also how, say, `sin(x)` is defined. There is a special hook
(defined in sympycore/calculus/function.py) for how to parse
Calculus('sin(x)') correctly.
The same should be implemented also for Logic functions so that
Logic('Implies(x, y)') would work as expected.

Regards,
Pearu

[Pearu Peterson]

On Apr 2, 6:08 am, Daishi <dai...@gmail.com> wrote:
> On Apr 1, 6:48 pm, Daishi <dai...@gmail.com> wrote:
>
> > 1. Logic(True) != Logic('True')
> > (The LHS is a number, while the RHS is a symbol).
> > Given how generally sympycore seems to parse
> > string arguments it seems like this would be a nice
> > property to have.
>
> perhaps naively, i tried the following
> patch to try to remedy this, but it appears
> to only partially do the right thing.
>
> >>> print Logic(True).as_tree()
>
> Verbatim:
> NUMBER[True]>>> print Logic('True').as_tree()
>
> Verbatim:
> NUMBER[True]>>> print Logic('True and False').as_tree()
>
> Verbatim:
> AND[
> SYMBOL[True]
> SYMBOL[False]
> ]
>
> i.e., it works for the simplest case, but
> not when actual parsing on the string
> argument is done.

I think I have covered the above in my last mail.

> i did look and see that ultimately you are
> using the compiler/ast modules to do the
> string parsing. i'm not very familiar with
> these modules, but my impression from
> somewhat following python-dev and
> python-3000 gossip is that the compiler
> module is to be deprecated. i believe
> the parser module is meant to substitute,
> but it's quite possible that i don't fully
> appreciate your use-case and the parser
> module would not be suitable.

I think when the compiler package will be depreciated then
we can reimplement the parser code easily
using the recommended tools. In fact, if I recall correctly,
sympycore used to use parser package last year but
then compiler package turned out to be more convinient
for sympycore case. We can review this when there will
be depreciation issues. For now sympycore
assumes Python 2.5 and up, so the current approach
should be stable for some time.

Regards,
Pearu

[Daishi]

On Apr 2, 1:39 am, Pearu Peterson <pearu.peter...@gmail.com> wrote:
> See also how, say, `sin(x)` is defined. There is a special hook
> (defined in sympycore/calculus/function.py) for how to parse
> Calculus('sin(x)') correctly.
> The same should be implemented also for Logic functions so that
> Logic('Implies(x, y)') would work as expected.

hi pearu,

thanks again for your continued help!

i looked over some of your latest doc updates,
so it seems the recommendation is to subclass
core.Function when defining new functions?

something that is still unclear to me when
one might prefer the approach taken in
logic.functions, where e.g., Eq, Lt, etc.
are defined as plain python 'def's,
and basically delegate to Logic.<op>
once conversion has been done.

is there a reason why these would not
also be core.Functions? It seems like
one difference is that for core.Functions
the head ends up being the class itself,
while for Eq, Lt, etc, you have interned
strings, but it's not clear to me that that's
a big deal.

i am currently in the process of starting
to write some basic code. my goal is
to be able to write something like:

Logic('any(x in X, x%2==0)').subs('X', [1,2,3]) => Logic('True')
Logic('all(x in X, x%2==0)').subs('X', [1,2,3]) => Logic('False')

although i should probably get the above
working first, i'm wondering if you have
any opinions as to whether it would be useful
for logical quantifiers to "collect" possibly in
a manner similar to CollectingField, so
that instead of:

Logic('any(x in X, any(y in Y, x%y==0))')

we could have something like:

Logic('any(x in X, y in Y, x%y==0)')


on a separate note, one small thing that
i noticed is that i believe that EQ is
missing from head_to_string in utils.py:

--- a/sympycore/utils.py
+++ b/sympycore/utils.py
@@ -72,7 +72,7 @@ DENSE_POLY = intern('DP')

head_to_string = {\
OR:'OR', AND:'AND', NOT:'NOT',
- LT:'LT', LE:'LE', GT:'GT', GE:'GE', NE:'NE',
+ LT:'LT', LE:'LE', GT:'GT', GE:'GE', EQ:'EQ', NE:'NE',
BAND:'BAND', BOR:'BOR', BXOR:'BXOR', INVERT:'INVERT',
POS:'POS', NEG:'NEG', ADD:'ADD', SUB:'SUB', MOD:'MOD', MUL:'MUL',
DIV:'DIV', POW:'POW',
NUMBER:'NUMBER', SYMBOL:'SYMBOL', APPLY:'APPLY', TUPLE:'TUPLE',
LAMBDA:'LAMBDA',


finally, not to be pedantic, but
i believe when you say 'canonization'/'canonized'
what you mean is 'canonicalization'/'canonicalize'.
see, e.g.:
http://en.wikipedia.org/wiki/Canonicalization
vs
http://en.wikipedia.org/wiki/Canonization

d

[Ondrej Certik]

> finally, not to be pedantic, but
> i believe when you say 'canonization'/'canonized'
> what you mean is 'canonicalization'/'canonicalize'.
> see, e.g.:
> http://en.wikipedia.org/wiki/Canonicalization
> vs
> http://en.wikipedia.org/wiki/Canonization

Oops, thanks for noticing, we really don't want the "canonize". :)

For SymPy, this is now:

http://code.google.com/p/sympy/issues/detail?id=777

Ondrej

[Pearu Peterson]

On Apr 3, 7:33 pm, Daishi <dai...@gmail.com> wrote:
> On Apr 2, 1:39 am, Pearu Peterson <pearu.peter...@gmail.com> wrote:
>
> > See also how, say, `sin(x)` is defined. There is a special hook
> > (defined in sympycore/calculus/function.py) for how to parse
> > Calculus('sin(x)') correctly.
> > The same should be implemented also for Logic functions so that
> > Logic('Implies(x, y)') would work as expected.
>
> hi pearu,
>
> thanks again for your continued help!
>
> i looked over some of your latest doc updates,
> so it seems the recommendation is to subclass
> core.Function when defining new functions?

Yes. Note that core.Function is named as core.DefinedFunction.
(Function is now defined for functions ring support).

> something that is still unclear to me when
> one might prefer the approach taken in
> logic.functions, where e.g., Eq, Lt, etc.
> are defined as plain python 'def's,
> and basically delegate to Logic.<op>
> once conversion has been done.
>
> is there a reason why these would not
> also be core.Functions? It seems like
> one difference is that for core.Functions
> the head ends up being the class itself,
> while for Eq, Lt, etc, you have interned
> strings, but it's not clear to me that that's
> a big deal.

First, the Logic.Lt classmethod and Lt function is kept
separated for performance reasons: Logic.Lt does not
have conversion support because in internal algorithms
all arguments are assumed to be of correct type.
The Lt function is provided for end-users where argument
conversion might be necessary.

Second, indeed it would be possible to replace all interned
strings with core.DefinedFunction subclasses. Currently
we are just following a convention that if python defines
an operation then the corresponding head in sympycore
is interned string of operation symbol. This convention
is assumed in Verbatim._compute_str method, for instance
(look at the last line in the method). Otherwise it is not a

big deal.

> i am currently in the process of starting
> to write some basic code. my goal is
> to be able to write something like:
>
> Logic('any(x in X, x%2==0)').subs('X', [1,2,3]) => Logic('True')
> Logic('all(x in X, x%2==0)').subs('X', [1,2,3]) => Logic('False')

I would use Capitalized names for `all` and `any` as
they are already taken by Python.

To get the above working, sympycore needs `in` support finished. I'll
take a look at that..

Meanwhile you can define Contains function and rewrite an expression
above as
Logic('Any(Contains(X, x), x%2==0)')
for instance.

> although i should probably get the above
> working first, i'm wondering if you have
> any opinions as to whether it would be useful
> for logical quantifiers to "collect" possibly in
> a manner similar to CollectingField, so
> that instead of:
>
> Logic('any(x in X, any(y in Y, x%y==0))')
>
> we could have something like:
>
> Logic('any(x in X, y in Y, x%y==0)')

Yes, that should be probably implemented in class methods Logic.Any,
similar to Logic.And, for instance.

Hmm, may be one should consider also other names for Any and All:
Any -> Exists
All -> ForAll
Look for how Mathematica or Maple names these functions. Also,
use the same argument order that these programs do. For example,
Exists(x%y=0, x in X, y in Y)
could be also an option (it could have advantage in implementing
collect feature).

> on a separate note, one small thing that
> i noticed is that i believe that EQ is
> missing from head_to_string in utils.py:

Thanks, it is fixed in svn,

> finally, not to be pedantic, but
> i believe when you say 'canonization'/'canonized'
> what you mean is 'canonicalization'/'canonicalize'.
> see, e.g.:
> http://en.wikipedia.org/wiki/Canonicalization
> vs
> http://en.wikipedia.org/wiki/Canonization

Right:) We should use correct terminology indeed.

Thanks for feedback and bug reports,
Pearu

[Pearu Peterson]

On Apr 3, 8:33 pm, Pearu Peterson <pearu.peter...@gmail.com> wrote:

> To get the above working, sympycore needs `in` support finished. I'll
> take a look at that..

Ok, I have implemented `in` and `not in` support in svn. It is not
complete
though as we don't have Set algebra yet. Anyway, now
Logic('x in X') is parsed to Logic.IsElement(x, X).

Regards,
Pearu