On 2/11/23 07:39, David A. Wheeler wrote: > 1) I think one of the "key" missing things is ability to help a user > to understand why a statement doesn't unify.
I have only an approximate idea of whether this is easy or hard, but I will say that even modest improvements here would be helpful. For example, it may be easier to detect particular cases than every possible "way" a statement can't unify. One of the more time consuming things that happens to me when using mmj2 is that a unification which I expected to happen doesn't, and then I need to look at (sometimes long) expressions to figure out what parts don't match. Hi Igor, below I tell what I've come up with, in yamma. First, I'll write the short story, then I'll elaborate a bit about the theory and the challenges. The short story: yamma has two kinds of diagnostic messages for unification failure. The first kind of message, suggests how to fix the unification error. Two examples: "Unification error: referenced statement is '|- ph' but it was expected to be '|- ( ps -> ph )'" (see https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L329 for the full unit test) or "Unification error: statement is '|- ch' but it was expected to be '|- ( &W1 <-> &W2 )'" (see https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L498 for the full unit test) The first example is a diagnostic highlighted on the hyp label, referencing a formula that doesn't match what's expected. The second example is a diagnostic on the statement itself (the 'main' formula cannot be unified with what's expected by the step label) The second kind of messages, involves substitution of working vars. Example: 'Working Var unification error: the working var &W2 should be replaced with the following subformula, containing itself ( &W2 -> ph )' (see https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L420 for the full unit test) Now, a bit of 'theory' (as far as I understand it) There are two categories of unification: 1. single statement 2. multiple statements With single statement unification, you're trying to find the mgu for both the logical variables (the theory's variables) and the (possible) working variables. You could use a Martelli Montanari algorithm on the whole proof, and it will be clean and "secure", but you'll not get a super-informative error message. That's why, for the single statement unification, I've gone for a 'custom' approach, that allows for some better error message. With multiple statement unification, you're trying to find the mgu for all the working vars in the proof (because logical variables have already been 'substituted'). Here, I've gone with the 'pure' Martelli Montanari algorithm. It can fail either - with a 'clash fail' error (for metamath, it means two constants don't match; something like '->' was expected, but you have '<->' ) or - with an 'occur check fail' (a working var should be replaced with a formula strictly containing itself) Hope this can give you some ideas. -- 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/2c6f7855-3aea-4035-a0c6-2e16cf2f1aben%40googlegroups.com.
