search

pythological / unification

Straightforward unification in Python that's extensible via generic functions.
Other
43 stars 7 forks source link

Recover "irreducible unsatisfiable set" of equations #37

Closed frabert closed 2 years ago

frabert commented 2 years ago

Is it possible for the algorithm to report an irreducible set of equations that render unification impossible? I.e. removing any one equation from the set renders unification possible

brandonwillard commented 2 years ago

Is it possible for the algorithm to report an irreducible set of equations that render unification impossible? I.e. removing any one equation from the set renders unification possible

No, there's no explicit functionality for something like that. Since it involves equational reasoning, it sounds like something that could possibly be facilitated by this library, but would otherwise fall outside of its scope.

brandonwillard commented 2 years ago

For simple cases, you could encode equations as relational goals in miniKanren (e.g. see this kanren example) and, if an evaluation of those goals yields answers/matches, then you can confirm that unification is possible for that system of equations. While that doesn't answer the irreducibility aspect, or the more general notion of unification being impossible, it's one flexible way to determine whether or not unification of a form is possible under a set of equations.

The irreducibility aspect sounds like something in the vein of rewrite completion and reduction (e.g. Knuth-Bendix and the like).

frabert commented 2 years ago

Wow, thanks for the additional notes!

In the end, I'm going to exploit some properties of the specific problem at hand to avoid having to find an actual irreducible set