Hi Cris,
Translating MM to HOL requires two stages, MM -> MM0 and then MM0 -> HOL. I
have a HOL intermediate representation which you can test using the command
"mm0-hs to-hol" on the MM0 repo (https://github.com/digama0/mm0), which is
then translated into OpenTheory and Lean (I hope to get other exporters
working but I am limited by my expertise in the target system).
MM0 differs from MM in that variables are separated into bound variables
and regular variables. In set.mm "setvar" is a bound variable type and
"class" and "wff" are regular variables. Bound variables are always
distinct, which means that some work is required to eliminate bundling by
duplicating statements and proofs. Additionally, every term constructor and
theorem is annotated with the set of bound variable dependencies of each
regular variable. That is, we say things like "ph is an open term depending
on x" which is opposite to the MM practice of declaring the variables that
a regular variable does *not* depend on. These are mostly derivable from $d
statements in MM, but the dependency annotations in MM0 terms is new and
requires a bit of additional annotation in the input MM file. But on the
whole this translation is not too traumatic and the result is still
recognizably the same as the input MM theorem.
Now suppose we have an MM0 statement translated from MM. For example ax-gen:
${
ax-gen.1 $e |- ph $.
ax-gen $a |- A. x ph $.
$}
translates to the MM0 statement:
axiom ax_gen {x: setvar} (ph: wff x): $ ph $ > $ A. x ph $;
Note that x is in braces, indicating it is a bound variable, and ph is
declared to depend on x. Now, let's write this in HOL. First, we remove all
bound variables from the context (like x); they influence the types of
other things but don't directly appear in the statement. For regular
variables, they are turned into a function arrow with one argument for each
bound variable dependency. In this case, that means that ph gets type
setvar -> wff, and all occurrences of ph in the hypotheses are replaced
with "ph x".
As I mentioned, MM0 has a new concept not (explicitly) in MM, namely
binding term constructors. For instance, "A. x ph" in the MM0 statement is
actually notation for "wal x ph", where wal is defined as:
term wal {x: setvar} (ph: wff x): wff;
This says that the input ph is allowed to depend on x, and it binds these
occurrences; since the result type is "wff" instead of "wff x", x is bound
in the result. Like with statements, this is translated to HOL by removing
the bound variable arguments and changing the type of ph to setvar -> wff,
so that the overall type of wal is (setvar -> wff) -> wff. In statements,
this means that an application "wff x ph" is translated to "wff (\x. ph x)"
where "\x." is a lambda over x.
Coming back to ax_gen, the hypothesis becomes "ph x" and the conclusion
becomes "wal (\x. ph x)". Now we universally close each statement by
gathering all the free variables. So the hypothesis becomes "!x. ph x" and
the conclusion stays as "wal (\x. ph x)" because x is already bound in the
conclusion. The "!x." here is a meta-quantification over variable x of type
setvar, i.e. whatever the native HOL system thinks a forall quantifier is.
Finally, we string all the hypotheses together with meta-implication, and
bind all the regular variables at the top level. The result is:
ax_gen : !(ph : setvar -> wff). (!x:setvar. ph x) -> wal (\x:setvar. ph x)
In addition to theorem applications, MM0 adds a conversion rule to support
definitions (which are not in MM), and it requires a "forget" rule of the
type
forget (P: wff) : (!x:setvar. P) -> P
that is equivalent to "the type setvar is nonempty", in order to accomodate
proofs that use dummy variables. In the target HOL system this is generally
provable by using a concrete element of set, e.g. the empty set.
Mario
On Tue, Jun 18, 2019 at 5:07 PM Cris Perdue <[email protected]> wrote:
> Hi Mario,
>
> I am intrigued by your work toward translating from MM0 to HOL or a subset
> thereof, as you discuss in your post of May 19: (
> https://groups.google.com/d/msg/metamath/raGj9fO6U2I/8gKq_KFuBQA),
> and I would like to understand better how the incoming MM/MM0 statements
> correspond to their HOL counterparts. The question that always comes to my
> mind is what statements in Metamath (normally theorems) translate into.
>
> You mention OpenTheory as a target, so I imagine the language of
> statements to be a pretty generic language of the HOL variety.
>
> Can you offer some combination of description and examples of how the
> translation of a Metamath statement relates to the original (or MM0)
> version of the statement?
>
> This would be very much appreciated. I have some notions of how this might
> go, and will be very interested to learn of your actual practice.
>
> -Cris
>
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/CAOoe%3DWLnpy%3D1wF1Sh8hOrpjOBcDzj5Ssty7hfwWJLWVwhfPuXA%40mail.gmail.com
> <https://groups.google.com/d/msgid/metamath/CAOoe%3DWLnpy%3D1wF1Sh8hOrpjOBcDzj5Ssty7hfwWJLWVwhfPuXA%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSuD3mVVwt7uUO-k_CSbgNPDewqfHgEjBsoGKonZq6sozQ%40mail.gmail.com.
