Proof Assistant -- Unification and Metamath
Database Lookup Strategy -- An Outline.
=A Few Preliminaries=
My adventures with parsing showed me that the
"naive" approach to a subject that is complicated
and already well researched is unlikely to yield
satisfactory results. However, Metamath is
logically "agnostic", and conventional approaches
such as rewriting expressions into "normal" forms
may be unsuitable. The objective here is to add
to mmj2, creating facilities that can be accessed
in server-mode, and which are not dependent upon
the logic or grammar of the input Metamath
database -- except to say that the grammar must
be verified by mmj2 and that every statement is
parseable. Then...after I fail two or three times
I will know enough to access the literature
intelligently :)
Numero Dos: By "proof assistant" I am referring
to a utility that fills in missing statement
label "Ref" values, as on this proof page:
http://us.metamath.org/mpegif/isset.html
Or, in the format I use for in-stream .mm proofs
written as comments:
$( ======================================================== $)
$( *** Deduction combining antecedents and consequents. *** $)
${
syl34d.1 $e |- ( ph -> ( ps -> ch ) ) $.
syl34d.2 $e |- ( ph -> ( th -> ta ) ) $.
syl34d $p |- ( ph -> ( ( ch -> th ) -> ( ps -> ta ) ) )
$=
wph wch wth wi wch wta wi wps wta wi wph wth wta wch
syl34d.2 syl3d wph wps wch wta syl34d.1 syl4d syld
$.
$(
#/HYP REF EXPRESSION
===== ======== ==========================================
1: syl34d.1 |- ( ph -> ( ps -> ch ) ) $.
2: syl34d.2 |- ( ph -> ( th -> ta ) ) $.
3:2 syl3d |- ( ph ->
( ( ch -> th ) -> ( ch -> ta ) ) $.
4:1 syl4d |- ( ph ->
( ( ch -> ta ) -> ( ps -> ta ) ) $.
5:3,4 syld |- ( ph ->
( ( ch -> th ) -> ( ps -> ta ) ) ) $.
QED
$)
$}
The user will be required to complete a table or
rows containing the Step, Hyp and Expression
columns, then the Proof Assistant will complete
the Ref column. To speed things up, we might ask
the user to put an "H" in the Hyp column if the
Expression is one of the theorem's hypotheses --
or incorporate the theorem's hypotheses
automatically as steps 1, 2, etc.
While this may not seem ambitious, the difficulty
level of an industrial strength solution is
higher than might be imagined. Right now set.mm
has more than 6000 theorems and axioms. A key
challenge lies in efficient search because the
search must be repeated for each step of every
proof! And, a realistic solution must be capable
of handling an even larger database of theorems,
perhaps as many as 100,000 theorems, or more.
(Yes, $/cpu cycle is decreasing faster than the
size of set.mm is increasing -- right now -- but
the objective is a system that works well
interactively, and if the search time grows, even
linearly with the number of theorems in the
database, there might not be enough CPU power on
the planet to keep the customers happy.)
( OFF TOPIC NOTE concerning above Metamath link:
(fyi, Ponder theorem "isset" above, and its
friend "visset". visset is saying: "Every set
variable is a set" and isset is a way of
asserting that a given class, A is a set. The
*syntax axiom* (!?) "cv" converts a set variable
to a class grammatical type (every set is a
class), so it is interesting to discover visset.
mmj2 treats cv purely as a "Type Conversion
Syntax Axiom", but I am annoyed with this
perspective as it feels as if cv is more than a
grammatical device. In due time enlightenment
will come :)
=Sketch of Unification Process=
A) Each justified step in a proof table *is* a
separate proof. Justification for a step is
either that the step reiterates an hypothesis or
assertion, *or* that the step Expression is
derivable from previously given assertions
(axioms or theorems) and/or hypotheses, using the
rules of the Metamath Proof Verification Engine
regarding substitutions and distinct variables.
B) What is elsewhere referred to as "unification"
is used here to mean a process for determining
valid substitutions from a proof step Expression
into a given assertion's variables -- and *if*
these substitutions exist.
[ Ref: "Unification is a procedure for searching
for a consistent set of substitutions of
elements."
http://www.rci.rutgers.edu/~cfs/472_html/Logic_KR/resolution.html ]
In the case of an unambiguous grammar, assuming
successful grammatical parsing of every statement
in the .mm database, unification can be regarded
as, first, overlaying an assertion's parse tree
with a proof step Expression's parse tree and
making sure that none of the assertion's syntax
axiom nodes are visible. Then, the nodes where
the proof step's parse tree graft onto the
assertion's parse tree provide the substitutions,
which must be unique (only one substitution per
variable). The substitutions are then applied to
the Candidate assertion, which is then compared
to the original Expression -- they must now be
equal.
For example, unify:
ax-1 = ( ph -> ( ps -> ph ) )
with a proof step Expression "E":
E = ( ( ph -> ph ) -> ( ps -> ( ph -> ph ) ) )
"ax-1" "E"
**** ****
*wi* *wi*
**** ****
. . . .
. . . .
---- **** **** ****
-ph- *wi* *wi* *wi*
---- **** **** ****
. . . . . .
. . . . . .
---- ---- ---- ---- ---- ****
-ps- -ph- -ph- -ph- -ps- *wi*
---- ---- ---- ---- ---- ****
. .
. .
---- ----
-ph- -ph-
---- ----
From the diagram it is obvious that E can be
unified with ax-1 because each "****" box in ax-1
is overlayed by an *identical* box from E. This
is a necessary condition for unification because
the grammar was stipulated to be unambiguous, and
so, each expression has only one parse tree.
And, from the diagram, we see the correct, unique
variable substitutions to make. The "----" boxes
in ax-1 are the graft points on the ax-1 parse
tree: graft the corresponding subtree from E over
each "----" box in the ax-1 parse tree -- and if
the variable in the "----" box occurs more than
once in ax-1, then the same substitution takes
place for each occurrence (i.e. if E were defined
as follows then unification would be impossible:
E' = ( ( ph -> ph ) -> ( ps -> ( ch -> th ) ) ).
Note: the example above does not portray the full
complexity of unifying expressions containing
Type Conversion(1) and Nulls Permitted(2) Syntax
Axioms (as opposed to just Notation Syntax
Axioms, as we call them in mmj2). Nor does it
cover the scenario of Logical Hypotheses(3).
1. If a Type Conversion occurs *above* a "****"
box in the assertion's parse tree, then there must
be an identical overlaying node in the Expression's
parse tree. This is, again, because the grammar
is unambiguous and unique parse trees have been
stipulated to have been obtained prior to unification.
2. A "----" box containing a Nulls Permitted
Syntax Axiom must also be overlayed by an
identical node in the Expression's parse tree.
This is because "null" is a constant, and cannot
there can be no substitution for a constant
according to the rules of the Metamath Proof
Verification engine. (So...this consideration
also applies to Constant Syntax Axioms such as
"c0"!)
3. Each Logical Hypothesis of the assertion must
*also* be Unified (!) with an hypothesis from the
proof step -- and vice-versa. If the proof step
Hyp field specifies "1,2,4" then that means that
the proof step can only be matched to an
assertion with exactly 3 Logical Hypotheses --
each of which must undergo unification with one
of the Hyp Expressions specified by the user (we
will allow for the case where the user does not
provide the correct sequence of hypotheses,
compared to the assertion's .mm file ordering in
spite of the fact that extra work will be
required to rearrange the proof step's Hyp's.)
C) The problem of finding a Proof Step Ref using
the step's Expression and Hyp values requires a
search to identify "Candidates" for unification.
There may be many assertions satisfying the parse
tree overlay process described above! And, the
"degenerate" case of an assertion expression such
as "|- ph" must be considered (this obtains from
modus ponens as well as the trivial proof that a
hypothesis yields itself.)
Once a set of Candidate assertions is available,
secondary tests must be applied to determine
which, if any of the Candidates satisfy the
requirements of Unification (such as unique
substitution for "ph" in the example above) and
any disjoint variable restrictions used in the
Metamath Proof Verification Engine.
And, there may be more than one Candidate
assertion that passes every test, including any
distinct variable restrictions. In this
situation, assuming that the Candidate is not the
same Theorem we are trying to prove (!), perhaps
the user should be happy that we found even one
and will be grateful if we return the first
Candidate we find? (Additional restrictions on
the Candidates will be needed, for example
specification of the position of the theorem to
be proved in the .mm database -- meaning that no
subsequent assertions can be used in its proof --
i.e. no recursion!)
=Searching a Metamath Database: Context=
We wish to avoid sequential search of a .mm
database for each step of a proof. Ergo, a direct
lookup method is desired, but without having to
rewrite each proof step's Expression into a
"normal form"; the algorithm should be as general
as possible, knowing nothing about propositional
or any other form of logic or notation.
The problem with direct access is that,
essentially, building the set of "Candidate"
assertions for Unification involves a sort of
geometric matching -- the selected Candiates'
parse trees must be congruent to the proof step's
parse tree. And, unfortunately, we don't know in
advance how much of each Candidate's tree to
overlay. Just the root, or the root plus a
subtree? Remember that ax-mp may be the chosen
Candidate even for a very complex and lengthy
Expression (the Candidate's root node may be a
"Degenerate" Expression of the form "ph" -- a
generic wff.)
Here are some items that can be matched or used
to winnow a .mm database into a set of Candidates
for Unification:
1. Number of Logical Hypotheses: must match proof
step's number of Hyp's exactly. If the proof
step's Hyp column specifies 4 hypotheses, then
only axioms and theorems with 4 Logical
Hypotheses need apply.
2. It is stipulated that Proof Assistant is not
used for "syntax proofs". That means that each
proof step's Expression's Type Code is "|-" or
the user-designated Provable Logic Statement Type
Code (in mmj2 terminology). Thus, only axioms and
theorems with Type Code "|-" are to be considered
-- syntax axioms are excluded, and that means
that our Candidates will be of type "wff", or the
user-designated Logical Statement Type Code
equivalent that corresponds to "|-".
3. The Candidate's assertion's parse tree root
node always exists (duh), and is either
Degenerate (Variable Hypothesis or Nulls
Permitted Syntax Axiom -- the latter being
included as a technicality, for completeness), or
Not Degenerate (Notation or Type Conversion
Syntax Axiom):
- If Degenerate, the Type Code of the
Var Hyp or Nulls Axiom must match the
Type Code of the proof step's Expression;
- If Not Degenerate, the root node's (Syntax
Axiom) Label must equal the Label of the
root node of the proof step's Expression's
parse tree.
In other words, if the parse tree root node for
the proof step's Expression = "wi", then a
suitable Candidate for Unification must also have
a "wi" root node, or be Degenerate and have a
"wff" type Variable Hypothesis in the root. (A
proof step Null root could unify with a Null or a
"ph" root node, but not in set.mm of course.)
4. Similar considerations to #3 apply for each
Logical Hypothesis of a Candidate assertion for
Unification with a proof step's Logical
Hypothesis. Each Logical Hypothesis also has a
parse tree, and the root nodes on corresponding
Candidate assertion and proof step Logical
Hypotheses must match.
For example, consider ax-mp
${
maj $e |- ( ph -> ps ) $.
min $e |- ph $.
ax-mp $p |- ps $.
$}
ax-mp would be a satisfactory Candidate for
Unification with a proof step having one
hypothesis root node = "wi", a Degenerate second
hypothesis of type "wff", and a Degenerate
assertion of type "wff". (Subsequent checks of
unique variable substitutions would then be
needed to confirm the match.)
5. Sequence Number of a Candidate for
Unification: must be less than the Sequence
number of the Theorem being proved. (The Proof
Assistant may provide an entry field allowing
input of either a maximum Sequence Number, or a
Label which would specify the last Axiom or
Theorem that could possibly be used.)
6. Other metrics might be considered, such as
length or height of the portion of the
Candidate's parse tree to be overlayed. These
seem to be of dubious utility. If the portion of
the Candidate's parse tree to be overlayed is
longer -- written in RPN format -- than the proof
step's Expression, excluding Variable Hypotheses,
then the Candidate can be rejected out of hand.
Likewise with height.
7. Many assertions have parse trees that are
completely filled out with non-Degenerate nodes
below the root down to level 2 or 3.
For example, ax-2 has a "syntax depth" of 3, with
levels 1 and 2 "syntactically completed":
ax-2 $a |- ( ( ph -> ( ps -> ch ) ) ->
( ( ph -> ps ) -> ( ph -> ch ) ) ) $.
ax-2
****
*wi*
.****.
. .
. .
**** ****
*wi* *wi*
**** ****
. . . .
. . . .
---- **** **** ****
-ph- *wi* *wi* *wi*
---- **** **** ****
. . . . . .
. . . . . .
---- ---- ---- ---- ---- ----
-ps- -ch- -ph- -ps- -ph- -ch-
---- ---- ---- ---- ---- ----
=Searching a Metamath Database: Alternatives=
Variation 1:
In theory, a lookup key or a hash-code could be
constructed using the "syntactically completed"
levels, along with -- perhaps -- the number of
Logical Hypotheses. For ax-2 such a key string
might look like this:
"*wi*wi wi*0"
Then, to locate suitable Candidate assertions for
an Expression, E which is syntactically complete
to level 2, the lookup could proceed as follows:
1) Search Level 2 hash table
2) Search Level 1 hash table
3) Search Level 0 (degenerate) hash table
This approach still does not solve the problem of
correctly ordering the Logical Hypotheses. Since
we will not (absolutely) require (but request)
that the correct sequence of Logical Hypotheses
be provided to the Proof Assistant, building a
key using the syntactic structure of the Logical
Hypotheses is not straight-forward -- especially
since one of more of the hypotheses may be of the
degenerate form "ph".
Fortunately, "degenerate" form Logical Hypotheses
are in the minority, and a multi-step lookup
could be performed a key built with sorted top
level nodes from the hypotheses. For example, if
the Logical Hypotheses of an assertion have top
level parse nodes = "wi", "wn", then a key =
"wi*wn" could be constructed -- and in the event
of an unsuccessful search, a secondary lookup for
degenerate top level nodes could be performed.
Variation 2:
A preferred approach for the mmj2 system will
likely take into account the fact that every
symbol, assertion, theorem, hypothesis, etc. is
accessed by (object) reference instead of by
name. This means that "wi" is only referred to
during input and output. Thus, the top level "wi"
node of an Expression's parse tree contains a
reference to *the* "wi" object. There is no need
to perform a hash or tree lookup, the address is
already at hand. To facilitate this alternative,
a reference to a Proof Assistant lookup object
would be added to mmj.lang.Assrt, and another
refernence would be added to mmj.lang.Cnst to
handle the degenerate form of assertion (i.e. for
set.mm Cnst "wff" would contain a reference to a
separate lookup table holding ax-mp, etc.)
Considering set.mm as a typical database, though
still on the small side ( :), there are
approximately 41 wff type syntax axioms (class
syntax axioms will not appear in the root node of
a theorem or logical axiom parse tree in set.mm).
Given equal distribution of the 6,000 theorems
and axioms among the wff syntax constructors
yields an average of 150 Candidates for a proof
step expression. These are reduced somewhat by
the degenerate assertions such as ax-mp, which
would be searched separately.
To further reduce the number of Candidates that
would need to be painstakingly examined with in-
depth Unification, a secondary set of tables can
be added based on number of Logical Hypotheses. A
guesstimate is that 75% of Theorems and Logical
axioms have 0, 1, or 2 or 3 Logical Hypotheses.
These secondary tables could be constructed if
and when the primary table for a syntax
constructor's size exceeds a certain number, such
as 10 or 20.
A tertiary level of lookup tables might be
deployed for exceedingly common constructors such
as "wi" that may well be in the root nodes of
thousands of theorems -- and after splitting
these up according to the number of Logical
Hypotheses, several hundred might be present in a
secondary table. Techniques mentioned in
Variation 1 might be adapted for use here in the
tertiary lookups. For example, a hash key could
be built for syntactially complete level 2 parse
trees. Or, hash keys based on the root nodes of
the Logical Hypotheses might be created. And, a
combination might be tried for special cases such
as assertions with exactly 1 Logical Hypothesis
-- in this case the sequence of hypotheses is
moot, and a compound key could be constructed.
Note: it is further envisioned that within any
lookup table containing a list or array of
assertions to be examined that the assertions
will be sequenced by their order within the
Metamath database -- i.e. their Sequence Number.
This will enable a lookup to be terminated once
the input Max Sequence Number for the theorem in
the Proof Assistant is exceeded (i.e. if we are
proving theorem 100 we do not need to examine
101, 102 -- they are disallowed by definition in
the Metamath Proof Verification Engine!)
Examination and review of set.mm and perhaps
ql.mm will be needed before making any final
decisions about how to proceed with these
lookups. At the very least, set.mm and ql.mm will
provide instruction as to the *wrong* lookup
strategies. Ideally, the lookup process would
yield no more than 10 or 20 assertions for which
Unification would be attempted.
The costliness of Unification is not entirely
clear either, but it is envisioned that rejection
of Candidates will be performed as expediently as
possible. Resequencing proof step hypotheses is
likely to add expense to the Unification process,
as well as complexity. Detective work will be
needed to figure out which variables need to be
Unified -- and this will require Unification of
Logical Hypotheses! A process of elimination will
be needed to work through the impossible
sequences of hypotheses.
=Other real-life proof examples to ponder=
http://us2.metamath.org:8888/mpegif/sylan9.html
http://us2.metamath.org:8888/mpegif/rcla42v.html
Or, take for example, Theorem #5187 of set.mm, "climadd",
which has 9 logical hypotheses and a deceptively
short Expression but requires 193 proof steps!
http://us2.metamath.org:8888/mpegif/climadd.html
=set.mm wff-type Syntax Constructors=
FREQ (in theorem parse tree root nodes
as of 6/26/2005)
====
3587 # 2 label=wi formula=wff ( ph -> ps )
968 # 3 label=wb formula=wff ( ph <-> ps )
814 # 17 label=wceq formula=wff A = B
206 # 18 label=wcel formula=wff A e. B
152 # 44 label=wbr formula=wff A R B
110 # 30 label=wss formula=wff A (_ B
79 # 1 label=wn formula=wff -. ph
55 # 9 label=wex formula=wff E. x ph
40 --(degen)- wff formula=wff ph
22 # 67 label=wfn formula=wff A Fn B
20 # 4 label=wo formula=wff ( ph \/ ps )
20 # 22 label=wrex formula=wff E. x e. A ph
16 # 65 label=wrel formula=wff Rel A
15 # 68 label=wf formula=wff F : A --> B
11 # 5 label=wa formula=wff ( ph /\ ps )
10 # 14 label=wmo formula=wff E* x ph
10 # 19 label=wne formula=wff A =/= B
10 # 21 label=wral formula=wff A. x e. A ph
8 # 66 label=wfun formula=wff Fun A
8 # 49 label=wor formula=wff R Or A
7 # 71 label=wf1o formula=wff F : A -1-1-onto-> B
6 # 7 label=w3a formula=wff ( ph /\ ps /\ ch )
6 # 82 label=wer formula=wff Er R
5 # 53 label=word formula=wff Ord A
4 # 8 label=wal formula=wff A. x ph
4 # 43 label=wtr formula=wff Tr A
3 # 13 label=weu formula=wff E! x ph
3 # 70 label=wfo formula=wff F : A -onto-> B
3 # 51 label=wfr formula=wff R Fr A
3 # 23 label=wreu formula=wff E! x e. A ph
3 # 12 label=wsb formula=wff [ y / x ] ph
2 # 10 label=weq formula=wff x = y
2 # 73 label=wiso formula=wff H Isom R , S ( A , B )
2 # 55 label=wlim formula=wff Lim A
2 # 20 label=wnel formula=wff A e/ B
2 # 52 label=wwe formula=wff R We A
1 # 69 label=wf1 formula=wff F : A -1-1-> B
1 # 48 label=wpo formula=wff R Po A
0 # 6 label=w3o formula=wff ( ph \/ ps \/ ch )
0 # 11 label=wel formula=wff x e. y
0 # 31 label=wpss formula=wff A (. B
0 # 26 label=wsbc formula=wff [ A / x ] ph