Translation from MM0 / MM to HOL

[Cris Perdue]

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

[Mario Carneiro]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAOoe%3DWLnpy%3D1wF1Sh8hOrpjOBcDzj5Ssty7hfwWJLWVwhfPuXA%40mail.gmail.com.

[Mario Carneiro]

On Tue, Jun 18, 2019 at 6:01 PM Mario Carneiro <di....@gmail.com> wrote:

In statements, this means that an application "wff x ph" is translated to "wff (\x. ph x)" where "\x." is a lambda over x.

Oops, typo. That should read:

In statements, this means that an application "wal x ph" is translated to "wal (\x. ph x)" where "\x." is a lambda over x.

[Cris Perdue]

Thanks Mario for your diligent efforts to explain your work on translations from MM / MM0 to other logical languages, HOL in particular. I can't say at this point that I properly understand everything you have said, but it does look like the results of translation may indeed match what I would hope for in a translation to HOL. I would like to explore this further. Having Metamath theorems and proofs available for consumers of HOL looks promising and interesting from my point of view.

You refer to using the command mm0-hs to-hol in your repository. I am not a Haskell user and am not exactly set up to run Haskell on the Mac computers I use. On the other hand I do have Docker set up, and have downloaded an official Haskell image from Docker Hub, which I expect I can use to run scripts such as this one. The description at https://hub.docker.com/_/haskell/ states that:

This image ships a minimal Haskell toolchain (ghc and cabal-install) from the upstream downloads.haskell.org Debian repository as well as the Stack tool (https://www.haskellstack.org/).

Can you give ghc command(s) to build the translator?  I think I can figure out how to run ghc commands within the Docker image, and work with files on the host filesystem. And then, would I run the compiled Haskell in a specific directory, e.g. one containing set.mm or an MM0 counterpart?

Frankly, right now I would find translations of statements in Metamath (or MM0) to statements in HOL more interesting than translations of the proofs. OpenTheory claims to be low-level and surely not the only option for translation of the proofs.

You may already have files with the results of the translation(s). If some of these might be available, perhaps that would be a good next step for me rather than recreating the translations. What do you see as reasonable options?

Thanks much,

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSs9yPXUUBTGgGbUFETYr9d94mibpjk-kzK2z%3DM_LoA0VA%40mail.gmail.com.

[Mario Carneiro]

One place where you can look for results of the translations is https://github.com/digama0/mm0/blob/build/mm0-lean/mm0/set/set.lean#L7625 , which is the output of the MM0 -> Lean translation. The variable names are currently kind of garbage because they aren't preserved through the translation process, and there are no notations so it's all direct references to the metamath internal names for the syntax constructors, but you should be able to see the general shape I outlined in the previous post and you can probably infer a lot more by looking around and comparing the theorems there to the original theorems from set.mm (note that hyphens become underscores in the translation).

The Haskell project is designed to be run using Stack, which ensures a consistent build environment. I believe it is possible to use ghc directly, but only if you give it a mountain of command line options. If your docker build supports stack, then the following should work:

stack build mm0-hs

stack exec mm0-hs

which should produce a short error/help message detailing mm0-hs's command line options (of which to-hol is the most useful one for the present purpose).

By the way, check out https://github.com/digama0/mm0/blob/build/mm0-lean/mm0/set/post.lean#L539 , which is a *complete* translation of dirith. It's a proof of Dirichlet's theorem in lean, in fully lean-native syntax, by modeling ZFC inside lean and translating the statement (including natural numbers, gcd, divisibility and infinitude) from the metamath notions to the analogous lean notions.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAOoe%3DWJQ%3DPnZhYWRKP%3DjJsiEH7atLk7sEDQj8%3DfDbbn2ojnRjQ%40mail.gmail.com.