Crash on startup with custom .mm file

[ishanpm]

Hello,

I'm using mmj2 to create a database of linear logic theorems, and mmj2 crashes upon startup in the presence of two particular theorems.

Here is the database I am using, along with the RunParams file and start script: https://github.com/ishanpm/metamathlinear/tree/7f8b9e3d8e0ec36532d4b3d91079476354ad81dd

Here are the specific statements causing the crash; mmj2 starts fine when either one is commented out: https://github.com/ishanpm/metamathlinear/blob/7f8b9e3d8e0ec36532d4b3d91079476354ad81dd/linear.mm#L632-L642

${
  lbsymi.1 $e |- ( ph O-O ps ) $.
  $( Linear biconditional is symmetric. Inference for ~lbsym . ERROR this makes mmj2 freak out for some reason $)
  lbsymi $p |- ( ps O-O ph ) $= ? $.
$}
${
  lbtri.1 $e |- ( ph O-O ps ) $.
  lbtri.2 $e |- ( ps O-O ch ) $.
  $( Linear biconditional is transitive. Inference for ~lbtr . $)
  lbtri $p |- ( ph O-O ch ) $= ? $.
$}

This error message is produced when attempting to start mmj2:

I-UT-0015 **** Processing RunParmFile Command #8 = RunProofAsstGUI
null
java.lang.NullPointerException
        at mmj.transforms.EquivalenceInfo.fillDeductRules(EquivalenceInfo.java:91)
        at mmj.transforms.TransformationManager.<init>(TransformationManager.java:106)
        at mmj.pa.ProofAsst.initAutotransformations(ProofAsst.java:977)
        at mmj.pa.ProofAsst.initializeLookupTables(ProofAsst.java:259)
        at mmj.util.ProofAsstBoss.getProofAsst(ProofAsstBoss.java:319)
        at mmj.util.ProofAsstBoss.doRunProofAsstGUI(ProofAsstBoss.java:1020)
        at mmj.util.Boss.lambda$putCommand$0(Boss.java:107)
        at mmj.util.Boss.doRunParmCommand(Boss.java:121)
        at mmj.util.BatchFramework.executeRunParmCommand(BatchFramework.java:281)
        at mmj.util.BatchFramework.runIt(BatchFramework.java:223)
        at mmj.util.BatchMMJ2.main(BatchMMJ2.java:53)
null

I am running the latest precompiled version of mmj2 as of 12/20/2020, under HotSpot on Windows 10.

[ml-2]

I'm no expert on MMJ2, but since I already have a debugging environment for it set up I decided to take a stab at figuring this out. What's going on seems to be that the addition of ~ lbsymi makes MMJ2 recognize O-O as an equality on wffs, because it is reflexive, symmetric, and transitive. The issue is that it also expects such an equality operator to have a deduction version of these theorems, and as you've seen, it doesn't handle their absence gracefully.

So the easiest way to fix it right now would be to add the extra theorems it expects, assuming they are true in linear logic (unfortunately I don't know anything about linear logic so I'm not totally sure).

Add these theorems for -O:

${
   lbsymd.1 $e |- ( ph -O ( ps O-O ch ) ) $.
   $( Linear biconditional is symmetric. Deduction for ~lbsym . $)
   lbsymd $p |- ( ph -O ( ch O-O ps ) ) $= ? $.
 $}
 ${
   lbtrd.1 $e |- ( ph -O ( ps O-O ch ) ) $.
   lbtrd.2 $e |- ( ph -O ( ch O-O th ) ) $.
   $( Linear biconditional is transitive. Deduction for ~lbtr . $)
   lbtrd $p |- ( ph -O ( ps O-O th ) ) $= ? $.
 $}

And add these for ->:

 ${
   lbsymimd.1 $e |- ( ph -> ( ps O-O ch ) ) $.
   $( TODO $)
   lbsymimd $p |- ( ph -> ( ch O-O ps ) ) $= ? $.
 $}
 ${
   lbtrimd.1 $e |- ( ph -> ( ps O-O ch ) ) $.
   lbtrimd.2 $e |- ( ph -> ( ch O-O th ) ) $.
   $( TODO $)
   lbtrimd $p |- ( ph -> ( ps O-O th ) ) $= ? $.
 $}

Optionally, adding these should remove the warning message about the "trivial implication rule":

 ${
   lba1i.1 $e |- ph $.
   $( TODO $)
   lba1i $p |- ( ps -O ph ) $= ? $.
 $}

and

 ${
   a1i.1 $e |- ph $.
   $( TODO $)
   a1i $p |- ( ps -> ph ) $= ? $.
 $}

[ishanpm]

Thank you! Luckily, all of the equality deduction theorems are valid in linear logic. ph ==> ( ps -O ph ) isn't, though, so I'll just have to live with that warning message. This resolves my particular issue so I'll close this, even though this problem might still affect other theories that can't accommodate deduction-style theorems.

[digama0]

What I would have suggested, if the proposed fix didn't work, is to disable the autotransformations module, which does some classical logic specific reasoning. You can disable it using ProofAsstUseAutotransformations,no,no,no in the RunParms.

[ishanpm]

@digama0 Attempting to use ProofAsstUseAutotransformations,no,no,no still causes the errors (both the "trivial implication rule" warning for -O and the crash due to missing deduction theorems); in fact, the errors happen on the line with the ProofAsstUseAutotransformations command. The traceback is a little bit different for the crash:

I-UT-0015 **** Processing RunParmFile Command #4 = ProofAsstUseAutotransformations,no,no,no
null
java.lang.NullPointerException
        at mmj.transforms.EquivalenceInfo.fillDeductRules(EquivalenceInfo.java:92)
        at mmj.transforms.TransformationManager.<init>(TransformationManager.java:106)
        at mmj.pa.ProofAsst.initAutotransformations(ProofAsst.java:977)
        at mmj.pa.ProofAsst.initializeLookupTables(ProofAsst.java:259)
        at mmj.util.ProofAsstBoss.getProofAsst(ProofAsstBoss.java:319)
        at mmj.util.ProofAsstBoss.doProofAsstUseAutotransformations(ProofAsstBoss.java:755)
        at mmj.util.Boss.lambda$putCommand$0(Boss.java:107)
        at mmj.util.Boss.doRunParmCommand(Boss.java:121)
        at mmj.util.BatchFramework.executeRunParmCommand(BatchFramework.java:281)
        at mmj.util.BatchFramework.runIt(BatchFramework.java:223)
        at mmj.util.BatchMMJ2.main(BatchMMJ2.java:53)
null

Poking through the source, it seems that the ProofAsstUseAutotransformations command constructs a ProofAsst object, which creates a (broken) TransformationManager as part of its initialization. The silver lining of all this is that I now know how to compile mmj2 from source, so I'll make a pull request.