Proposal: add option for axiom usage minimization

[GinoGiotto]

As mentioned in the GitHub issue¹, with the /MAY_GROW option it's possible to utilize the minimizer as an axiom usage minimizer. Some of my pull requests²³⁴ show that this approach can lead to meaningful results.

However, the drawback of this method is that the minimizer often produces "garbage" modified proofs that are neither shorter nor eliminate any axiom dependency. Consequently, I find myself needing to tediously filter only the valuable edits, which consumes a lot of time.

To address this issue, I propose the addition of a new option for the minimizer. Its implementation would limit the edits to only when some dependencies at choice are eliminated as a result (so no garbage edits would occour). Below I present how this addition would combine with the other commands. I'm not attached to this formatting particularly, feel free to propose your alternative ideas (or different option names).

/IF_DROP

The /IF_DROP <label-match> option means: "Modify the proof only when at least one of the labels in <label-match> has been removed in the proof dependencies". In most cases we would be interested in removing axioms, so /IF_DROP ax-* would be the most common use. Regardless the user can use it against undesirable theorems and definitions as well.

Here is how this addition would behave with some option combinations:

• Edit proofs if replacements are both shorter and less dependent on axioms. This is a rare occurrence, so it's probably not very useful.

MM-PA> MINIMIZE_WITH * /IF_DROP ax-*

• Edit proofs when axiom dependencies are reduced, regardless of the length of new proofs. This would be the basic useful form.

MM-PA> MINIMIZE_WITH * /IF_DROP ax-* /MAY_GROW

• Edit proofs when axiom dependencies are reduced, regardless of the length of new proofs. Additionally, allow the introduction of new definitions within the proof, which provides a better fine-tuning compared to the previous combination.

MM-PA> MINIMIZE_WITH * /IF_DROP ax-* /MAY_GROW /ALLOW_NEW_AXIOMS * /NO_NEW_AXIOMS_FROM ax-*

• As mentioned by @benjub in the Metamath mailing list⁵, by proving a few statements in main with distinct variable conditions, then most other theorems can drop ax-13 without adding any new dv conditions. This is where the axiom minimizer becomes handy, as it could automatically axiom-reduce those non-dv proofs, thereby speeding up the process:

MM-PA> MINIMIZE_WITH * /IF_DROP ax-* /MAY_GROW /ALLOW_NEW_AXIOMS * /NO_NEW_AXIOMS_FROM ax-* /FORBID ax-13

The combination with /FORBID ensures that any replacement would never use ax-13, therefore providing the desired behaviour (in practice /FORBID makes it more likely to find a specific axiom reduction, because we are forcing it to choose our route in case of interchangeable possibilities, see #154 (comment) for a basic example).

/IF_DROP_OR_SHORTER

Minimization requires a significant amount of computing power, so we might aim to make the most of our time. In that case we could use a refined option /IF_DROP_OR_SHORTER <label-match>. This one would make an edit if either any of the written labels dropped (regardless of the proof length) or if the proof is shorter. This way we would maximize the outcome for the time spent for the process (note: in this case the /MAY_GROW option would have no effect).

Some side thoughts

As explained by Norman Megill⁶, /NO_NEW_AXIOMS_FROM ax-* (when accompanied by /ALLOW_NEW_AXIOMS *) does not introduce new axioms, but can utilize different ones if they are already part of the proof. In contrast, /FORBID avoids any dependency from <label-match>, regardless of their presence in the proof. The latter option effectively forces the minimizer to eliminate dependencies from a proof if enough allowed replacements exist.

Therefore I disagree with the first note of /FORBID when consulting MM> help minimize in metamath-exe⁷: I think /FORBID is useful and shouldn't be deprecated. If the minimizer will be used as an axiom reducer, I would propose revising or removing that note, as /FORBID would be exactly what is needed.

One could also add an option to create a log file of axiom reductions for the corresponding proof edits. This way the user would be facilitated when consulting the reasons behind those particular changes.

I'm aware that this whole proposal goes against the "don't add anything" rule for metamath-exe, but I believe this small addition would be useful to speed up some routine processes in the long term. If you think this is worth giving consideration, I'll already be very grateful for it.

Regards

Gino

Footnotes

1. GitHub issue about ax-13: https://github.com/metamath/set.mm/issues/3183 ↩

2. Pull request removing ax-11 and ax-13: https://github.com/metamath/set.mm/pull/3189 ↩

3. Pull request removing ax-pow: https://github.com/metamath/set.mm/pull/3222 ↩

4. Pull request removing ax-13: https://github.com/metamath/set.mm/pull/3274 ↩

5. Benjub Google Groups discussion: https://groups.google.com/g/metamath/c/1wi1s6qBYqY/m/FPkPsd5oAwAJ ↩

6. Norman Megill's explanation: https://groups.google.com/g/metamath/c/f-L91-1jI24/m/3KJnGa8qCgAJ ↩

7. Help section about /FORBID: https://github.com/metamath/metamath-exe/blob/16ca0310abff69ff9c3777cb336ea69213f01f79/src/mmhlpb.c#L1296C1-L1299 ↩

[digama0]

The option seems reasonable to me, although I'm not planning on working on it any time soon. I will review a PR which implements it. The design looks a bit ad-hoc / inextensible (I'm sure you can come up with more variations on this command and maybe we will be doing this again later), but I will leave rethinking / overhauling the system to one of the newer alternatives.