Remplacement simultané de la fonction logique SymPy

Question

Je suis tombé sur un problème de substitution de variables dans des formules logiques dans Sympy. Voici un exemple minimal -

from sympy import *
x, y = symbols('x y')
Nand(x, y).subs({x: Nand(x, y)}, simultaneous=True)

Cela échoue à la fois dans mon inter-opérateur local et dans le shell live sur Docs SymPy avec le message d'erreur

Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/base/data/home/apps/s~sympy-live-hrd/49.400254913747479351/sympy/sympy/core/basic.py", line 889, in subs
    d = Dummy(commutative=new.is_commutative)
  File "/base/data/home/apps/s~sympy-live-hrd/49.400254913747479351/sympy/sympy/core/symbol.py", line 205, in __new__
    cls._sanitize(assumptions, cls)
  File "/base/data/home/apps/s~sympy-live-hrd/49.400254913747479351/sympy/sympy/core/symbol.py", line 65, in _sanitize
    '%scommutativity must be True or False.' % whose)
ValueError: Dummy commutativity must be True or False.

D'autres formulations que j'ai essayées, comme remplacer les "Nand" par des "And", n'ont pas échoué. Le fait de définir simultaneous=False n'échoue pas non plus, mais ne donnera pas le résultat souhaité si je veux remplacer y en même temps (cf. cette question pour en savoir plus).

S'agit-il d'un bogue dans SymPy, ou est-ce que je comprends mal quelque chose ?

Answer 1

C'est un bogue dans SymPy. Classe Not n'a pas is_commutative et n'en hérite pas non plus. En conséquence, Nand(x, y) (qui est Not(And(x, y)) a "None" pour l'hypothèse de "commutativité", ce qui n'est pas acceptable pour la méthode de création de symboles fictifs, qui tente de créer un symbole fictif avec les mêmes hypothèses. Ce problème ne se pose pas pour And parce que And hérite de is_commutative=True de LatticeOp classe.

La façon de corriger cela dans SymPy semble être d'ajouter is_commutative=True à la classe Not .

Les solutions de contournement du côté de l'utilisateur comprennent : l'utilisation de Or(Not(x), Not(y)) au lieu de Nand(x, y)

Nand(x, y).subs({x: Or(Not(x), Not(y))}, simultaneous=True)

(ce qui renvoie ~(y & (~x | ~y)) )

et de réparer les classes par toi-même :

class Not(Not):
    is_commutative = True

class Nand(Nand):
    @classmethod
    def eval(cls, *args):
        return Not(And(*args))      

Nand(x, y).subs({x: Nand(x, y)}, simultaneous=True)

(retours ~(y & ~(x & y)) .)