HomePage RecentChanges

mmj2Feedback20080113

Back to: mmj2

note about the wiki

NOTE: To update the wiki your "username" must be whitelisted. Send an email to the wikilord if you are not already a user – and, if you don't care to do that, I authorize you to post as "ocat" for the purposes of mmj2 feedback and problem reports, etc. (Just put some initials on your edits so I know who is doing what…)

ALSO, you may get the "Cannot acquire main lock" error message when attempting to post to the wiki. In this case, hit the Back button on your browser, open a new window and go to RecentChanges then click on Administration, then Unlock Wiki. Wait, and then return to your original post and click on "submit" again.

other links

Dedicated page for feedback about the mmj2 Proof Assistant GUI: mmj2ProofAssistantFeedback

Previous version of mmj2Feedback: mmj2FeedbackV20070716

mmj2 -- ruminations about It (and how It got this way :-)

1. The mmj2 Proof Assistant GUI is written using the Java "Swing" classes, but it makes as little use as possible of standard GUI features. It is a bare-bones GUI, a Volkswagon, not a BMW or a Winnebago.

2. mmj2 is written in Java, which is surprisingly a very good language for something like mmj2 which involves a lot of complicated computations.

3. One weird and experimental thing about mmj2 is that it stores formulas and statements as sequences of references to objects, not as sequences of characters. Literally! For example, when set.mm is loaded into memory, there is only one ")" symbol (and one "(" symbol.) So, in a manner that is sure to flummox, annoy or boggle the average reader, the mmj2 code is studded with comparisons to MObj's like this: "if (mSym == nSym)", instead of "if (mSym.equals(nSym))".

4. A couple of people have asked, "Why is it so big?" That is an interesting, though relative question.

5. I asked myself, "Why did it take so long to reach this level of functionality? Nearly two years have gone by since the first release of mmj2!"

The first release of mmj2 on Aug-29-2005 contained just syntactic parsing and bootstrap creation of a Grammar from an input .mm file. In theory the requirements of all subsequent versions could have been determined by pure analysis at that point. The Proof Assistant GUI, the GUI "Derive" feature, Text-Mode Formula Formatting (TMFF), "soft" $ d error handling with generation of  $d statements, and Work Variables – perhaps this could all have been invented and coded in one shot. But part of that functionality was implemented as a result of user suggestions based on trying a working version of mmj2. For example, Raph suggested the "Derive" feature after trying the GUI, and the Work Variables enhancement finished what the Derive feature enhancement failed to adequately cover (that was an actual analysis error!)

In large, complicated systems choices must be made about which features are most useful and necessary. Given perfect analysis and superior intelligence all of these choices can be made correctly without experimentation. Unfortunately, I could not see the final end result before programming; so mmj2 shows my limitations. In my defense (self-justificatory pats on back), discoveries were required… Looking at this another way, a valid computer program is a proof that one's ideas and thoughts about the subject matter are correct; perhaps, then, a phased development approach is best when the subject matter requires discovery!

6. One of the most elegant and beautiful aspects of Metamath is that the Metamath .mm language uses the same syntax to define Syntax Axioms and Logic Axioms. This not only allows a user to define her own meta-language, and makes a .mm file self-defining, but it means that syntax and logic have parallel structures: parse trees and proof trees have the same structure! In fact, set.mm contains an instance of a "syntax proof" – a $p statement whose first formula symbol is "wff", in effect, "proving" that a formula can be generated using the previous syntax axioms…

What the parallel structure of syntax and logic also means is that given an unambiguous grammar (i.e. each formula has at most one syntactic parse tree), because we know that two identical parse trees have identical corresponding formulas, we also know that successful unification of a proof step showing that the step's conclusion and hypotheses are an instance of the justifying assertion (Ref) means that the proof step is valid.

Yes! the unification algorithms are logically equivalent to the Metamath stack-based, RPN Proof Verification algorithm, except for $d checking. This was not self-evident at the beginning of the project :-)

7. A very interesting feature of the Metamath language is the $d statement – the "Disjoint-variable Restriction" statement. The $d statement is used by Metamath to obviate the need for consideration of free vs. bound variables when performing substitutions (as in "replacing all free occurrences of 'x' with 'y').

The definition of $d's is simple yet precise, and can be traced back theoretically to Alfred Tarski's paper, "A Simplified Formulation of Predicate Calculus With Identity".

From the Metamath.pdf, page 96:

"The full meaning is that if any substitution is made to its two variables (during the course of a proof that references a $ a or  $p statement associated with the $d), the two expressions that result from the substitution must have no variables in common. In addition, each possible pair of variables, one from each expression, must be in a $d statement associated with the statement being proved. (This requirement forces the statement being proved to “inherit” the original disjoint variable restriction.)"

The beauty and elegance of the $d idea in the context of Metamath goes beyond the free vs. bound topic because the Metamath language enables the user define his/her own syntax and grammar. Whereas the "free vs. bound" distinction is intimately tied to syntax, the $ d statement is completely orthogonal to syntax;  $d's are layered on top of the user defined syntax (and $d's should not be supplied on Syntax Axioms!), and need not be restricted to the familiar index or range variable usages that are familiar to us from other languages. Thus, incorporation of the $d concept in the Metamath language makes Metamath more open-ended – or, conversely (looking at this another way), it eliminates the need for the Metamath language to have a mechanism for specifying whether or not or how a variable in a syntax construction is bound (or free.)

And, as with other great inventors, the Metamath inventor, Norm, strived to define the language with the most economical set of rules possible. But, as we see on page 105, complications to the $d definition arise when the concept of "Frame" and "Extended Frame" is introduced:

"A frame with a $p (provable) statement requires a proof as part of the $p statement. Sometimes in a proof we want to make use of temporary or dummy variables that do not occur in the $p statement or its mandatory hypotheses. To accommodate this we define an extended frame as a frame together with zero or more $ d and  $f statements that reference variables not among the mandatory variables of the frame. Any new variables referenced are called the optional variables of the extended frame. If a $f statement references an optional variable it is called an optional hypothesis, and if one or both of the variables in a $d statement are optional variables it is called an optional disjoint-variable restriction. Properties 2, 3, and 4 for a frame also apply to an extended frame."

The Metamath.pdf attempts to reassure the reader on Page 100, and this excerpt provides important information about the original intent for $d's and users:

"Since Metamath will always detect when $d statements are needed for a proof, you don’t have to worry too much about forgetting to put one in; it can always be added if you see the error message above. If you put in unnecessary $d statements, the worse that will happen is that your theorem might not be as general as it could be, and this may limit its use later on."

Now, finally, on the basis of the work done in mmj2 in the 01-Jun-2007 and 01-Aug-2007 releases, I can state this well-founded opinion: optional disjoint-variable restrictions should be eliminated from Metamath. Here is why:

As a practical matter, elimination of optional disjoint-variable restrictions could be done in a phased basis. Announce that, say, on January 1, 2008 optional disjoint-variable restrictions will be "deprecated" – that ("soft") error messages will no longer be generated as a result of their omission. Then, make the change to Metamath.exe on that date, and require that mmverify.py and mmj2 follow suit at their convenience. Over time new theorems and their proofs would not contain optional $d's, and if desired, code could be written to eliminate them from existing .mm databases. Simple :-)

That is all I feel like talking about today… but there are many other things that interest me about mmj2 (and "mmj3"). --ocat 21-Jul-2007

mmj2 appears to work ok on the Mac OS X

(subject to "Issues" below).

It is necessary to manually download and install the Apple "J2SE 5.0 Release 4" because even OS X 10.4.10 arrives with only Java 1.4.2 installed.

Curiously, it seems that J2SE 5.0 Release 4 must be installed (first) even though J2SE 5.0 Release 5 is available. The Apple Update instructions are not entirely clear on this point, IMO. My guess is that Release 4 contains something that changes the default Java version in use. After Release 4 is installed the obvious next step is to download the +80MB Release 5 and install it – that takes you from Java 1.5.06 to Java 1.5.07 and eliminates some bugs, etc.

Issues:


1. OS X uses path separator "/" instead of "\", so RunParms? .txt files need a few updates. For example:

In mmj2jar\RunParmsPATutorial?.txt change

     ProofAsstStartupProofWorksheet,PATutorial\Page101.mmp
     

to

     ProofAsstStartupProofWorksheet,PATutorial/Page101.mmp

2. OS X does not use absolute paths (drive letters) so any file name references using drive letters must be changed.

In mmj2jar\RunParms?.txt change

     LoadFile,c:\metamath\set.mm 
     

to

     LoadFile,set.mm 

(assuming that you copy the Metamath set.mm file to the current directory, "mmj2jar".)


3. There is a "bug" which amounts to a difference in the way the "ProofAsstProofFolder?" RunParm? builds its (internal) path name. This RunParm? sets the default directory where user Proof Worksheets are stored. The first time a "Save" or "SaveAs?" is attempted with the following RunParm? in effect, the Save Dialog is initiated at the top level directory of the hard drive instead of the given directory:

    ProofAsstProofFolder,myproofs
     

Fortunately, after the first Save the (internal) path is set correctly and the user does not need to (re)navigate to the correct location. So this bug amounts to a minor annoyance…and so it goes…


4. I have not yet studied up on the Mac OS X system and I have no idea what is the equivalent to the Windows ".bat" file for storing commands (batch). For now, to initiate mmj2 in OS X, fire up the Applications/Utilities/Terminal application and then "cd" to the "mmj2jar" directory (wherever you installed it). Then … using the TextEdit? application manually copy the "java …" command line from the mmj2jar/mmj2.bat file and paste it into the Terminal window. Then press Enter. Here is the command:

    java -Xincgc -Xms64M -Xmx128M -jar mmj2.jar RunParms.txt
     

I don't believe the "-Xincgc" option is operative in the OS X version of Java – whether it uses Incremental Garbage Collection by default, or not, I do not know… this may not be a problem because the reason I added the "-Xincgc" option was to avoid buggy parts of the Sun Java environment (apparently Garbage Collection is the hardest thing in the world to code properly.) By doing garbage collection continuously instead of waiting for a memory shortage, not only do we avoid problematic execution paths (IMO), but the added overhead is not discernable – while eliminating the chance of a noticable delay for a (non-incremental) full sweep of the garbage.


So, the bottom line based on a quick test and none of the regression tests, is that mmj2 works "ok" in the Max OS X environment, but it is a Rude Dog that needs to be sent to obedience school… --ocat 9-Aug-2007


Hello, I just compiled mmj2 on Eclipse running on my linux machine. It runs, but I have not had time to play around with it to test the functionality.

I have made a few changes on my local version, to get rid of many warnings Eclipse complained about when loading the source. There are still some warnings. The stuff I fixed is related to typing the generics (List, Collection, etc.) used. If you are interested, I can send a patch somewhere.

Dan Getz. – 9-Nov-2007

The Sun compiler generates warnings too, demanding that the new "generics" are used. If you think it is important to eliminate these warnings, then I can add the fixes to the next version. I already have a couple of little enhancements slated for inclusion, and with your contribution we may have enough change to justify doing a Release. Do you have an email address I can commo to? (Ghestalt seems to be dead but I recall "alamedanet.net" something?)

--ocat

One of my addresses is getzdan, hosted on Yahoo mail.

Getz Dan


Questions/Comments About mmj2?