Hi All,
I'm thinking about finally writing the missing MM0 -> MM translator. The
MM0 language was always designed to be compatible with metamath, so there
is a mostly one to one mapping from MM0 theorems and proofs to MM. But MM0
has some features that do not easily lower, and some intelligence is needed
to select the right choice.
Part 1: General translation
First, I will look at translating an arbitrary MM0 database to an MM
database, with no particular relation to set.mm.
1. Variables. In MM0, every theorem declares its own variables and the
types of those variables. There is no notion of a global variable. This is
sometimes used (especially in the more CS applications) with descriptively
named variables like "addr" or "env". How should these be translated? One
option is to use MM local variables, i.e. variables in local scope. But
this still requires adding a lot of (global) $v declarations for every
variable name in every scope, and moreover I think this runs into
restrictions with a variable having two types (for example, "a" is used as
a wff in the logic part of the peano database and then as a nat variable
later on).
* Option 1: Disambiguate all variable names with their sort, i.e. "aW"
and "aN". This is simple to implement but not super nice to look at.
* Option 2: Same as 1 but only disambiguate when a conflict is observed.
This is better but still not great because common variables like "a" will
get disambiguated at all their uses.
* Option 3: Ignore variable names from the source entirely and select
from a predefined list of variables of each type, i.e. specify that wff
variables should be "ph,ps,ch,th,..." and nat variables should be
"a,b,c,..." This requires more configuration work, and it also ignores the
names in the source, which may be informative, for example variables named
"G" are often used for the context in deduction style theorems, and names
like "env" will clearly be clobbered. If we run out of given names we will
have to allocate names like "x1, x2, x3" which are even less pleasant.
2. Definitions. In MM0 you can make a definition and there is a primitive
step for unfolding them. This is not terribly hard to model in MM using
equality proofs, although it requires that every sort have an equality
relation on it. In MM0 not all sorts have an equality relation defined on
them, and even when there is an explicit equality relation the system does
not register this fact explicitly. For example, in peano.mm1 there is an
"eq" relation on nat, and enough axioms to prove that every term respects
equality (similar to equality in set.mm), but like metamath there is
nothing special about this term constructor and without one of the axioms
this theorem would not be true. By contrast the definitional equality
relation exists on all sorts, has its own rules separate from theorem
application, and every MM0 term respects definitional equality regardless
of any axioms that exist.
* Option 1: Represent the definitional equality relation as a new term
constructor, one for each sort. Every term constructor gets an axiom saying
it respects definitional equality, and then we have to prove automatically
for every new definition that it too respects definitional equality. A
downside of this is that for types with an equality already we get two
equality relations, and what's worse you can't even prove "defeq a b -> a =
b" although it is true at the metalevel.
* Option 2: Add configuration so that you can say that a specified
relation should be used in preference to adding a new defeq relation, when
one exists on the sort. (For a database like set.mm this is not a problem
since every sort has an equality relation except setvar, which is a pure
sort and so does not need a defeq relation.) This generally results in more
idiomatic MM statements, although it does require identifying all the
axioms that the defeq judgment needs, and the system will probably end up
reproving a lot of equality theorems that already exist, unless these are
also marked.
3. Sort modifiers. MM0 has a number of sort modifiers, which were
originally devised to make the translation to MM clearer, so hopefully this
should be easy. By default a MM0 sort corresponds to two MM sorts, one for
variables and one for terms of that sort. A pure sort is one without any
term constructors, so in this case we can skip the term version; and a
strict sort is one without any binders, and for this we can skip the
variable version. A free sort is one where you can't drop unbound
variables; this one is problematic for MM but we can just ignore it in
translation, provided the sort itself is nonempty.
4. Delimiters. MM0 has a tokenizer that is slightly more complicated than
split(' '). But adding more spaces for disambiguation is totally okay, so I
am inclined to solve this by simply adding spaces around token sequences
until it matches MM conventions.
5. Notations. MM0 has a precedence grammar that allows you to avoid a lot
of parentheses. MM only allows the encoding of pure CFGs.
* Option 1: MM0's grammar is also a CFG, so use that encoding. This is a
strawman because the grammar has thousands of nonterminals (one for each
precedence level), and to declare this in MM would need one sort for every
precedence level (or at least every precedence level in use, which for
peano is probably at least 15-20 levels). We would also need a coercion
from each lower precedence level to the next higher level, meaning that
terms would be bloated with towers of meaningless coercion functions. (I've
actually done this sort of thing in metamath before; dtt.mm contains a
precedence grammar so that lambdas and applications don't need unnecessary
parentheses. Even there you need at least three levels and it is not at all
fun to write manually.)
* Option 2: Live with the extra parentheses. This is idiomatic MM. But
still it leaves open the question of how to determine when to insert
parentheses. Every MM sort corresponds to one precedence level, so
functions like "+" with type nat -> nat -> nat are not precedence changing
and hence require parentheses, while functions like "=": nat -> nat -> wff
are potentially precedence changing and require parentheses only if the
prec(nat) <= prec(wff). It is not clear how to assign precedences to sorts
based on the available precedence information in MM0, though (which is
associated with term constructors, not sorts). Perhaps this also needs to
be provided as configuration. (In set.mm it's pretty simple: there are only
two expression sorts, and prec(wff) < prec(class). In peano.mm0 I'm not
really sure what would be appropriate, perhaps prec(wff) < prec(nat) =
prec(set).)
* Option 3: Forget about the analysis and just parenthesize everything.
This has the advantage of being easy to implement and also easy to prove
unambiguous, compared to option 2.
6. Tactics. This is more of an MM1 feature than MM0, but it will be a shame
to lose all the tactic scripts. In particular this information might be
useful for using MM1 as a MM IDE by means of continuous translation. I
already much prefer MM1 to mmj2 for writing metamath style proofs, and
especially if MM1 can work in a semi-translated mode where it is compatible
in a limited way with pure metamath theorems, you might be able to use MM1
for set.mm development.
* Option 1: Live with it, drop the tactics, metamath was never designed
for this. This is the more idiomatic option, but it may end up with
difficult to maintain MM proofs. I don't think this is a very big problem
for the existing peano.mm1 proofs, because they have been written with a
mind toward efficient MM output, with the exception that peano.mm1 uses
ax_mp a lot more than MM normally would, and the *i "inference form"
theorems are mostly absent. But a minimize pass should clean this up. In
the future, especially if people other than me start writing tactics, it is
likely that much more inefficient proofs will start popping up. (I
recognize that I care about proof length a bit more than is rational.)
* Option 2: Put the proof scripts in comments next to the metamath proof,
possibly with some sigils so that they can be automatically rediscovered by
tooling. This solves the problem of recovering the tactic that produced the
proof, although it is also likely to go out of date if it is a proof script
for a set.mm proof and people who don't use MM0 subsequently change the
proof without changing the comment. It could be checked in CI but this puts
another layer of complexity in MM checking that arguably shouldn't be
present if it's actually to be a translation.
* Option 3: Try to reconstruct a MM1 proof script from a MM proof object.
This sounds really hard to me, particularly when it comes to identifying
where tactics have been called, as they don't really leave any trace in the
term.
* Option 4: Add comments *inside* a translated MM proof saying where
tactics were called. The most advanced version of this might require a
change to the MM spec, but we can probably get away with adding comments
like "ABAZBABC $( tac1 $) DFAZAABZ" in the compressed proof block.
7. Do blocks. Similarly, the definition of tactics themselves could be
translated, although at this point there is really not much to say on the
MM side besides "here's some MM1 code, I hope it means something to you
because I sure don't know what it is". In MM1 do blocks can also create
theorems and this is sort of the pinnacle of automated proof generation; it
is very hard to represent the provenance of these proofs in any meaningful
way. (For example, in peano_hex.mm1 I have implemented the arithmetic
algorithm in hexadecimal, and this requires an addition and multiplication
table for all numbers 0-15, so about 256 theorems for each operation. These
theorems, things like 7p4e11, are all being generated automatically.)
Part 2: set.mm
I think it is fair to say that for many of the results that are being
proven in peano.mm1 and all the knock on CS projects that will be proven
with respect to PA, it would be nice for soundness purposes to have a
translation that targets not some peano.mm database that is still PA, but
rather set.mm. That would allow things like the MM0 formalization and the
MMC verification framework to also exist inside set.mm. But this comes with
its own, additional challenges.
1. Sorts. peano.mm0 has three sorts: wff, nat, and set. These represent
booleans, natural numbers, and the powerset of natural numbers
respectively, rather like set.mm's set and class distinction but for finite
set theory. The obvious and idiomatic thing is to map wff to wff, nat to
NN0, and set to ~P NN0, but this leads to an obvious problem: what it means
to map a sort to a set.
Whenever we have a theorem with a nat variable 'a', we need to replace that
with a class variable 'A' and an assumption that 'A e. NN0'. Where do we
put this assumption?
* Option 1: Add the assumption in a hypothesis. This is the most faithful
representation of the original theorem but it limits its applicability
unless we use dedth.
* Option 2: Change the theorem to deduction form and then add a
hypothesis under the new context. This is simple-ish to implement, but it
does mean that some theorems will have two contexts which is not great.
* Option 3: Try to identify if the theorem is already in deduction form
and then use that context. More complicated, and also obviously requires
the translator to know about how deduction proofs are done in both systems
(although for a translation at this level of faithfulness between
specifically peano.mm0 + stuff to set.mm + stuff that's not unreasonable).
* Option 4: Add the assumptions as antecedents on the theorem. I'm not a
fan of this option because it requires knowing all the syl*anc theorems and
also messes up the statements of theorems.
Also, in many cases we can deduce the typing condition from another typing
condition in the MM0 theorem. For example MM0 itself has sets and uses them
for explicit typing; if we have (a: nat) and an assumption h: $ G -> a e.
(0 .. 16) $ we might want to not generate two typing assumptions on 'a',
since 'A e. ( 0 ..^ 16 )' is already sufficient to derive that A e. NN0. We
can probably assert this in general for anything that looks like a set in
peano.mm0, because if the sort 'set' is interpreted as ~P NN0 then "a e. A"
always implies that 'a' is in NN0 because A is syntactically restricted to
be a subset of NN0. Of course we have to do the same thing for 'set', and
here we might prefer to use "A C_ NN0" instead of "A e. ~P NN0" for being
more idiomatic. Again, lots of special case reasoning.
2. Alignment. peano.mm0 defines a lot of basic functions, like addition,
multiplication, division, the cantor pairing function, and so on. Some of
these have direct analogues, for example we can more or less directly
translate "a + b" to "( A + B )", using that + is closed in NN0 for the
typing theorem. Others don't: "a - b" in peano.mm0 is truncated
subtraction, which is not defined in set.mm (IIRC) so we would have to
create a new function for this or else litter the output with things like
if ( B <_ A , ( A - B ) , 0 ) that could grow the statement exponentially.
It's a shame that this can't be translated to ( A - B ) directly but unless
the theorem has a B <_ A guard in it this probably can't be done.
Other functions exist but have more complicated lowerings. For example
peano.mm0 has the 'the' operator for definite description, which has the
type set -> nat, while set.mm has "iota" instead, which is a binder. So
that means that we would want to translate "the A" to "iota_ x e. NN0 x e.
A" and "the {x | p}" to "iota_ x e. NN0 p", and this binding mismatch would
translate to the theorems as well. This problem can be ignored though if we
just want any translation and don't go for maximum fidelity.
---
That covers the issues I can currently see with the translation process.
I'm curious to see how people feel about the merits of the different
options, what would be the most helpful. Many of the points above also
apply to MM -> MM translations, for example type guards and alignment also
occur when translating peano.mm to set.mm or hol.mm to set.mm. It would be
nice if we had a good story around interpreting MM databases into abstract
(set-theoretic?) models and from there into reasonable MM databases like
set.mm.
Mario Carneiro
--
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/CAFXXJStRbLfL%3DX-0D11%2BG7x3U8AboJ%2BSbiD7XCh8PCsK0cC8mw%40mail.gmail.com.
