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.
