On Thu, 26 Sep 2019 16:56:26 -0400, Mario Carneiro <[email protected]> wrote:
> Benoit's description is a good explanation of how mmj2's definition checker
> works today.
I used Benoit's description as a starting point. I tweaked the last definition
rule text
to be (hopefully) clearer & to map more cleanly to the error messages
if a user sees them.
> The main worry I have about a pure reimplementation is the
> automated theorem prover part.
I added a hypertext link from the conventions text to the JavaScript code.
That way, someone who wants to know more will be able to quickly
see more information. That's not the best way to define things,
but I think the current problem is that it's not obvious that this situation
even exists or how to get *any* information about it.
If someone wants to rewrite that to be clearer/better later, I'd be delighted.
> If you aren't worried about dependence on set.mm metatheory, or on actually
> producing proofs, the easiest algorithm to implement is to keep track of
> all binding operators, and ensure that all dummies are not free in the true
> sense (while also calculating the binding structure of the new definition).
Is that algorithm adequate?
The code seems to all depend on proveBoundVar (copied below), but
I've never written an mmj2 JavaScript plugin so I wasn't sure how
to interpret that code (and it'd take me some time to drill in).
--- David A. Wheeler
=========================
function proveBoundVar(w, boundVars, v, dummy, root, fast)
{
var bound = new boolArr(root.child.length);
var bound2 = new boolArr(bound.length);
var allBound = true;
for (var i = 0; i < root.child.length; i++)
allBound &= bound[i] = bound2[i] = proveBoundVar(w, boundVars,
v, dummy, root.child[i], fast);
if (allBound)
return v.stmt != root.stmt;
var val = boundVars.get(root.stmt);
if (val == null) {
if (!fast)
return isBound(w, v, dummy, root);
var proto = root.stmt.getExprParseTree().getRoot();
val = new boolArrArr(proto.child.length);
for (var i = 0; i < val.length; i++) {
if (!proto.child[i].stmt.getTyp().getId().equals("setvar"))
continue;
val[i] = new boolArr(val.length);
var assignments = new HashMap();
for (var j = 0; j < val.length; j++)
if (proto.child[j].stmt instanceof VarHyp) {
assignments.clear();
assignments.put(
proto.child[j].stmt,
boxToType(proto.child[i],
boxToType(proto.child[i], null, "class"),
proto.child[j].stmt.getTyp().getId()));
val[i][j] = proveBoundVar(w, boundVars, proto.child[i],
dummy, reassignVariables(assignments, proto), false);
}
}
boundVars.put(root.stmt, val);
}
for (var i = 0; i < val.length; i++)
if (val[i] != null && !bound[i])
for (var j = 0; j < val.length; j++)
bound2[j] |= val[i][j];
for (var i = 0; i < val.length; i++)
if (!bound2[i])
return !fast && isBound(w, v, dummy, root);
return true;
}
--
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/E1iDbou-0003gu-4H%40rmmprod07.runbox.
