search

jozefg / higher-order-unification

A small implementation of higher-order unification
MIT License
182 stars 5 forks source link

Strange problem #1

Open liamoc opened 4 years ago

liamoc commented 4 years ago

Hi Daniel

Not sure if you're interested in helping me debug something, but I made use of this implementation as part of a proof assistant I am implementing.

Firstly, I think line 48 (where you check if you should raise a variable) is incorrect. Should it not read:

 LocalVar j -> if j >= lower then LocalVar (i + j) else LocalVar j

?

Secondly, I am now encountering a problem where it fails to make progress on this constraint:

(Lam (Ap (FreeVar 0) (LocalVar 0)),Ap (MetaVar 4) (FreeVar 0))

Pretty-printing this:

(\x. P x)  ~ ?4 P

For some reason, it spins around on this and doesn't find the obvious solution ?4 := (\y.\x. y x). I'd appreciate any help you can give. It's also possible I somehow introduced a bug that wasn't present in your original implementation. If that's the case, I'm sorry to have bothered you!

jozefg commented 4 years ago

Ack, I'm sorry, I just saw this now! Are you still stuck on this issue?

liamoc commented 4 years ago

I'm not stuck anymore, as I switched to pattern unification instead (works for what I'm doing). Still would be interested to figure out what was going wrong, but no urgency!

jozefg commented 4 years ago

I think pattern unification is probably sufficient for a proof assistant yeah, I would like to figure it out as well. I'll have to spend some time looking at code my longtime nemesis (past me) wrote.

fizruk commented 3 years ago

Hello there! I am now also looking at this code as a source of inspiration, thanks for making it public :)

I think that the problem with non-termination is because of this line: https://github.com/jozefg/higher-order-unification/blob/21382f44205aa3d8b115fe2b2eba47489da4b492/src/Unification.hs#L199

I believe this line exists to avoid identifying meta-variables with local (bound) variables. This is a bit confusing (why do we need an isClosed check here if we're concerned about bound variables). But what we are trying to check here is that we did not capture any of the bound variables which we previously converted into fresh free variables upon entering the scopes here:

https://github.com/jozefg/higher-order-unification/blob/21382f44205aa3d8b115fe2b2eba47489da4b492/src/Unification.hs#L164-L173

So if you remove isClosed check then the example of @liamoc works well. However, it is not correct to remove it entirely. Instead one could introduce another constructor (e.g. FreeLocalVar or FreshVar or something like that) and check for absence of those.