On Tuesday, October 5, 2021 at 2:57:41 p.m. UTC+2 [email protected] wrote: > Although the matchpy gives of AC1-matching capability as far as I'm aware, > I just have a question that if is it really general enough. > I'm aware that general equational matching could be an undecidable > problem, > and hence there are lots of matchers or unifiers that handles some > domain-specific E-matching problems > (for other cases like boolean algebra, distributivity, or some other > combinations of equational identities) > and that have to be implemented separately (even there can be some > distinguish for one-to-one and many matching because of efficiency)
I'm not familiar with the decidability of pattern matchers. MatchPy is simply creating a lookup data structure (I refer to the *many-to-one* matcher, they also have *one-to-one *and *discrimintation nets*), recurring through the target expression and lazily walk through all partitions (for associativity) or subsets (for commutativity) until a matching subexpression is found. Their paper is here: https://arxiv.org/abs/1710.06915 -- 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 view this discussion on the web visit https://groups.google.com/d/msgid/sympy/0b36fd8b-c12b-41f0-9838-ec2c5195074cn%40googlegroups.com.
