-
Notifications
You must be signed in to change notification settings - Fork 17
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unification function #19
Comments
Unbound itself does not have a unification function. It is of course possible to write one over terms built up with unbound. I suspect that a complete first-order unification algorithm probably doesn't belong within I wrote a fairly generic first-order unification algorithm for a project that I worked on a couple of years ago (https://github.com/ppaml-op3/insomnia/blob/master/src/Insomnia/Unify.hs) and maybe that's a useful starting point for you? (Note that I represented unification variables distinctly from unbound's |
Thanks for the helpful answer! I can get by with a simple solution for the moment, but those references will certainly be useful. |
Does unbound have a unification function? If not, does that seem like a good addition? To be precise, I'm looking for a function such that, given two terms
t0
,t1
, finds a substitutions
such thatsubsts s t0 `aeq` t1
, if it exists.The text was updated successfully, but these errors were encountered: