| MMJ Name (Abbreviation Usage) |
MetaMath.pdf Name/Standard Usage |
| MObj |
Math Object, parent class of Sym and Stmt. Created only because in a few places unrelated to the "core" lang processing, it is convenient to be able to hold an array or collection containing a mixture of Sym's and Stmt's. The database sequence numbe, "seq" is now stored in MObj. In theory, new objects that might be added later to enable persistent storage of the LogicalSystem object might be added as sub-classes of MObj (example, Scope, for one.) |
| Sym |
Math Symbol |
| Cnst |
Constant (aka $c) (Note: "const" is a Java keyword and "con" is a device name.) |
| Var |
Variable (aka $v) |
| varHypArray |
Internally
computed, provides
the unique variable hypotheses referenced in an assertion's
expression (it is a processing byproduct that is saved for later use.)
The variable hypotheses are stored in the array in order of their
appearance in the database -- i.e., by seq. Example: ax-1 expression "( ph -> ( ps -> ph ) )" has 2 unique variable hypotheses, named, "wph" and "wps" in set.mm. |
| Expr |
Expression. Refers to the 2nd through "n"th Sym's in a Formula. May be of zero length itself. |
| ExprRPN |
Reverse Polish Notation version
of expression, if it exists (it is assumed in MMJ that identification
of "syntax constructors" such as "wi" and "wn" axiomatic assertions
will enable automatic conversion of Expr's to ExprRPN's.) These RPN
versions are further differentiated by content: they refer only to
labels! For example, theorem "id" would be expressed in RPN as "wph wph
wi"; this embeds variable type information in the expression and avoids
namespace ambiguity (Cnst/Var's are not guaranteed to be different than
labels.) |
| Formula |
The Metamath "statement"
consisting of 1 Cnst Sym followed by 0 to m Cnst or Var Sym's. Defined
as an array of 0 to n Sym's, the Cnst at the beginning is referred to
as the Typ (type) of the statement. This class is outside of the
MObj->Sym/Stmt hierarchy and is stored as an attribute of Stmt. The
intent in separating the Formula into its own class was to facilitate
processing of formulas and expressions that are not part of a Stmt (for
example in proof verification -- see mmj.verify.) |
| LogicFormula |
LogicFormula is an attribute of
both LogHyp (Logical Hypothesis) and Assrt (Assertion). It is differentiated
from VarHypFormula because, although every Metamath statement can be
treated as a "Formula", VarHyp formulas consist of exact 1 Cnst Sym
followed by 1 Var Sym, and thus, the handling is different in a few
places; the other problem faced was that LogHyp is a sub-class of Hyp but
contains a LogicFormula, and Assrt also contains a LogHyp. |
| VarHypFormula |
Variable Hypothesis Formula. See LogicFormula. |
| Syn |
Syntax, normally used in reference to Syntax Axioms and/or VerifySyntax. |
| Vhe |
Variable-Hypothesized
Expression. This is a quirky, experimental thing derived from an
Expression: each Var in the Sym[] array is replaced by the
corresponding VarHyp for the Var in that specific Expression; the
VarHyp is *then* expanded into its component Type (a Cnst) and Var. The
Vhe and variations are used in Syntax Verification processing for
pattern matching. There are several variations for printing, sorting
and verifying. The quirkiest one of all is the MObjVhe[] which contains
a mixture of Cnst's and VarHyp's (the VarHyp's are not expanded.) Also
very quirky is the SynVhe, which stands for Syntax Axiom Vhe --
in this variation the Var is
replaced with null (the reason being that for insertion into the
SynTree the variable name is irrelevant -- as it is in all Syntax
Axioms, except to establish sequence of the hypothesis in
VerifyProof. All in all, an ugly business... |
| Typ |
= 1st Constant in Metamath $e, $f, $a and $p statements (i.e. statement "type code"). The first entry in the Formula Sym array. |
| Opt |
Optional (note that names of
sets/lists of variables and/or disjoint variable hypotheses,
unless the name is prefixed with "Opt" it refers to Mandatory
Variables, as in Mandatory Variable Type Hypotheses.) |
| Stmt |
Statement |
| DjVars |
Disjoint Variable Restriction
(aka $d, note that in Frames, unless prefixed with "Opt", refers to a
Mandatory Variable Disjoint Variable Restriction) |
| Hyp |
Hypothesis |
| VarHyp |
Variable Type Hypothesis (aka
$f, note that in Frames, unless prefixed with "Opt", refers to
Mandatory Variable Variable Type Hypothesis) |
| LogHyp |
Essential (aka $e aka "Logical") Hypothesis |
| Assrt |
Assertion |
| Axiom |
Axiomatic Assertion (aka $a) |
| Theorem |
Provable Assertion (aka $p) |
| MandFrame |
Mandatory
Frame -- attribute of every Assrt, both Axiom and Theorem. Contains the
"mandatory" hypotheses and disjoint variable restrictions of the
assertion. "Mandatory" refers to variables and hypotheses used in the
assertion's own statement and logical hypotheses' statements (see
OptFrame). |
| OptFrame |
Optional Frame -- only Theorems
have OptFrames. Whereas Axioms have only a MandFrame, Theorems have
both MandFrame and OptFrame. OptFrame contains variable hypotheses and
disjoint variable restrictions needed for assertions referenced in the
Theorem's proof. |
1. In the 3rd column, "Abstract/NA", "NA"
means the item is not actually coded as a separate Java class but is
provided in the table as a logical entity; "Y" means that the
Class is an abstract "super" class that cannot be instantiated (turned
into a
real "object" by itself), but its properties and attributes are
inherited by its sub-classes.
For example, "Assrt" is Abstract Class whose non-abstract
sub-classes are AxiomaticAssrt and ProvableAssrt; an assertion must be
either an axiomatic assertion or a provable assertion, but both types
of assertion share common properties and attributes.
2. The
4th column, "Unique Key Attributes" identifies which, if any,
components of the Class comprise a unique key, whether for sorting or
for duplicate checking.
For lack of a better name, "Id" is used in several places as a key;
it is the character string that was used in the MetaMath.mm file to
define the entry. For example, the value of Id for the so-called
"turnstile" symbol is "|-".
| MMJ Entity:Java Name (note: the *list names may not be coded as actual classes) | Relationships: "ISA" means Sub-Class Of "HAS" means contains "0-n" means Zero to "n" occurrences. |
A b s t r a c t / NA |
Unique Key A t t r i b ______________ |
Nonkey A t t r i b _______________________ |
| MObj |
Y |
int seq |
||
| Sym | ISA MObj |
Y |
String id |
|
| Cnst | ISA Sym |
boolean isVarTyp etc. (lots of stuff, including items created by and used by mmj.verify.Grammar.java) |
||
| Var | ISA Sym |
boolean active VarHyp activeVarHyp |
||
| Label | NA |
String label |
||
| Expr |
HAS 0-M Sym |
NA |
sym[1]->[n] of Formula |
|
| ExprRPN | HAS 0-M Stmt (references) |
NA |
Stmt[] exprRPN | |
| UnknownLabel (= "?") |
ISA Label |
NA |
(converted to null in proof table) | |
| Typ | HAS 1 Cnst |
NA |
sym[0] |
sym[0] of Formula |
| Formula |
HAS 1 Typ HAS 1 Expr |
int cnt Sym[] sym |
||
| VarTyp | ISA Typ |
NA |
||
| ExprTyp | ISA Typ |
NA |
||
| ProofStep |
HAS 0-1 Label HAS 0-1 UnknownLabel |
NA |
||
| Proof | HAS 1-M ProofStep |
NA |
Stmt[] | |
| DjVars | HAS 2 Var |
Var varLo Var varHi |
||
| Stmt | ISA MObj HAS 1 Label HAS 1 Formula HAS 1 ExprRPN | Y | String label | Formula formula Stmt[] exprRPN |
| Hyp | ISA Stmt | Y | boolean isActive | |
| VarHyp | ISA Hyp HAS 1 Var | Var var | ||
| LogHyp | ISA Hyp HAS 1 Expr HAS 1 ExprRPN | Sym[] expr Stmt[] exprRPN VarHyp[] varHypArray | ||
| Assrt | ISA Stmt HAS 1 Expr HAS 1 ExprRPN HAS 1 MandFrame | Y | Sym[] expr Stmt[] exprRPN VarHyp[] varHypArray MandFrame mandFrame | |
| Axiom | ISA Assrt | |||
| Theorem | ISA Assrt HAS 1 Proof HAS 1 OptFrame | Stmt[] proof OptFrame optFrame | ||
| DjVarsArray | HAS 0-M DjVars |
NA |
DjVars[] djVars |
|
| OptDjVarsArray | HAS 0-M DjVars |
NA |
DjVars[] optDjVars | |
| HypArray | HAS 0-M Hyp |
NA |
Hyp[] hypArray |
|
| OptHypList | HAS 0-M Hyp | NA | Hyp[] optHypArray | |
| MandFrame | HAS 1 HypArray HAS 1 DjVarsArray |
Hyp[] hypArray DjVars[] djVarsArray | ||
| OptFrame | HAS 1 OptHypArray HAS 1 OptDjVarsArray | Hyp[] optHypArray DjVars[] optDjVarsArray | ||
| =================== (OTHER) CONTENTS OF "LogicalSystem.java" follow: =================== |
====================== ====================== |
=== === |
=========== =========== |
======================== Notes? ======================== |
| ScopeDef |
HAS ArrayList Var HAS ArrayList VarHyp HAS ArrayList LogHyp HAS ArrayList DjVars |
"active" statements in current scope |
||
| scopeDefList |
HAS ArrayList ScopeDef |
NA |
ScopeDef definitions at a scope level (global scope = 0, followed by 1, 2, ...) |
|
| symTbl |
HAS Map |
NA |
String Sym.id |
Map symTbl (mandatory table: keep unused symbols from garbage coll.) |
| stmtTbl |
HAS Map |
NA |
String Stmt.label |
Map stmtTbl |