On Tue, Aug 23, 2022 at 8:33 AM Antony Bartlett <[email protected]> wrote:
> Are there any more implementations anyone wants to offer, please? > Another implementation you might want to look at is mm0-rs: https://github.com/digama0/mm0/blob/master/mm0-rs/src/elab/refine.rs#L692-L772 It's MM0 not metamath, but it basically represents what I would do for a metamath unification algorithm, with the slight extension that it supports unfolding definitions as well. You can just ignore the cases that call self.unfold (and the returned conversion proof) for mmj2-style unification. > I think it's quite possible that anything goes when it comes to writing a > unification algorithm? Maybe it doesn't matter in the slightest how you > come by a unification, because the very next thing you're going to do is > run a validator to ensure the proof is correct anyway, and because a > perfect algorithm does not currently exist so you're always going to have > to be able to fall back on the option of manual unification. Heuristics, > AI, quantum superposition of all potential unifications, whatever. I'll > almost certainly stick to the standard algorithm anyway, but it might > become tempting to massage away some difficulties (if any) encountered > while attempting to re-unifying theorems in set.mm. > Kind of. It's true that the result of a unification algorithm is checked, but it is possible to get the wrong answer, for example if you unify ?a =?= ?b with ?a := 1 and ?b := 2 that's obviously wrong and will cause issues in the proof assistant and confusion for the user, and if you resolve it with ?a := 1 and ?b := 1 that's also wrong because it's too specific and may cause the user to not be able to complete the proof. It's not true that there is no perfect algorithm though - for first order unification the "most general unifier" (mgu) is the unique best answer and it is decidable by exactly the algorithm I described. You will see that all extant verifiers are implementing something like that algorithm. There is a caveat regarding the metamath-exe algorithm though, which is that it doesn't actually have a complete and correct math parser so the classical algorithm doesn't exactly apply (since it goes by recursion on the structure of the term), and moreover it will sometimes give syntactically incorrect outputs and/or require user input to determine how to parse the expression. This is a metamath peculiarity which only exists for non-grammatical databases, but most other proof assistants do some kind of parsing to handle this step correctly. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" 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/metamath/CAFXXJSvnUc1smBsOz80xLCD16nAwbC2%2B%2BN3fs6Lr0i6aqfH%2B3A%40mail.gmail.com.
