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 <https://launchpad.net/~hvr/+archive/ubuntu/ghc> 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 On Tue, Jun 18, 2019 at 3:06 PM Mario Carneiro <[email protected]> wrote: > > > On Tue, Jun 18, 2019 at 6:01 PM Mario Carneiro <[email protected]> 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. > > -- > 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/CAFXXJSs9yPXUUBTGgGbUFETYr9d94mibpjk-kzK2z%3DM_LoA0VA%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJSs9yPXUUBTGgGbUFETYr9d94mibpjk-kzK2z%3DM_LoA0VA%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/CAOoe%3DWJQ%3DPnZhYWRKP%3DjJsiEH7atLk7sEDQj8%3DfDbbn2ojnRjQ%40mail.gmail.com.
