Hi Glauco, Please learn how to work with version control, so I can help, or at least cheer from the sidelines if you don't want help. They have nice YouTube videos from that too and I'm sure it's much easier to understand than the Martinelli Montanari mgu algorithm. The basic usage is probably easier than learning how to do unit testing with Jest.
I've just started writing a prettier plugin for mm files ( https://github.com/Antony74/prettier-plugin-mm), and fully half the task is tied up and neatly tucked away if I can get my hands on a serviceable parse tree. And surely there's no point in us both writing unifiers in TypeScript when we could both just work on yours? My other option is to focus on the third pillar - html generation - while you carry on writing your unifier. Mario writes: > 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. Fantastic, I wasn't looking forward to having to implement a fallback on manual unification like how metamath-exe does. So I'm never likely to see a unifier failure as long as I don't try to copy the metamath-exe algorithm or play with non-grammatical databases. Great :-) Best regards, Antony On Tue, Aug 23, 2022 at 7:12 PM Glauco <[email protected]> wrote: > Hi Antony, > > in the tool I'm working on, I definitely went for the Martinelli Montanari > mgu algorithm (you will find a lot of clear descriptions of the algorithm > and even a nice youtube video with a "concrete" example). > > Please, be aware that the unifier associates 'parse trees' (not formula > tokens) to working vars (the &Wnn and &Cmm stuff). > > The hard part is not to implement the (nice) algorithm, you first need to > parse your statements and build parse trees (the algorithm works with > 'terms' but 'parse trees' play the same role, thanks to set.mm > non-ambiguity). > > And before building parse trees, you have to build the grammar :-) > And this is done "on the fly" (it depends on the specific theory, i.e. .mm > file). > And, of course, you need to write a parser to feed with the (generated) > grammar and each statement (I used nearly.js, thus I did not needed to > write a new one). > > And once you've got parse trees, you'll need to build "substitutions" to > feed the mgu algorithm with the 'starting pairs' of parse trees to unify. > > Just for fun, this is a Jest test of what you can do with Diagnostic(s) > (in a language server) for a failing unification (mp2parse is not defined > here: it is an object of the class MmParser that parses .mm format and has > been fed with a supersmall subset of set.mm) > > test('Expect Working Var unification error', () => { > const mmpSource = > 'd1:: |- &W2\n' + > 'd2:: |- &W2\n' + > 'qed:d1,d2:ax-mp |- ph'; > const mmpParser: MmpParser = new MmpParser(mmpSource, > mp2Parser.labelToStatementMap, mp2Parser.outermostBlock, mp2Parser.grammar, > new WorkingVars()); > mmpParser.parse(); > expect(doesDiagnosticsContain(mmpParser.diagnostics, > MmpParserErrorCode.workingVarUnificationError)).toBeTruthy(); > expect(mmpParser.diagnostics.length).toBe(4); > mmpParser.diagnostics.forEach((diagnostic: Diagnostic) => { > if (diagnostic.code == > MmpParserErrorCode.workingVarUnificationError) { > const errMsg = 'Working Var unification error: the working > var &W2 should be ' + > 'replaced with the following subformula, containing itself > ( &W2 -> ph )'; > expect(diagnostic.message).toEqual(errMsg); > expect(diagnostic.range.start.line == 0 || > diagnostic.range.start.line == 1).toBeTruthy(); > expect(diagnostic.range.start.character).toBe(8); > expect(diagnostic.range.end.character).toBe(11); > } > }); > }); > > HTH > Glauco > > Il giorno martedì 23 agosto 2022 alle 14:33:50 UTC+2 [email protected] ha > scritto: > >> >> Are there any more implementations anyone wants to offer, please? >> >> 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. >> >> Or maybe it does matter because it's important to know whether it's the >> proof or the unification that was wrong. >> >> Best regards, >> >> Antony >> >> roups.google.com/d/msgid/metamath/CAFXXJSshZ3X-s8%2Be%3D%3D0CpV-6NB2Az66Q_iQx3tsM0iX-_0Pupg%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CAFXXJSshZ3X-s8%2Be%3D%3D0CpV-6NB2Az66Q_iQx3tsM0iX-_0Pupg%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- > 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/9471eb0d-3807-4446-a191-a99b5a92b2c8n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/9471eb0d-3807-4446-a191-a99b5a92b2c8n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAJ48g%2BCgBY8LgPBRtRopAmdJf9SE16wyxkv%2B-9Ja7O%3DXG%2Ba9SQ%40mail.gmail.com.
