On Sun, Mar 1, 2020 at 1:07 PM Olivier Binda <[email protected]> wrote:
> Quite satisfying but this raises a question :
> The parser of mm0 is great at parsing stuff with binary operators and
> turns things like
> 1 + 2 into
> a tree of the form
> + {
> 1
> 2
> }
> Yet Metamath was designed around co, that takes 3 classes A B C to define
> ( A B C )
> so the Metamath for the same tree is
> co {
> 1
> +
> 2
> }
>
This is correct. I have said on a few occasions that the metamath and mm0
notation systems are incompatible, and this is why. In MM0, every piece of
notation is associated to a syntax constructor, while in metamath syntax
constructors are associated to productions in a global CFG that need not
have any particular characteristics. While parentheses are reserved for
grouping, you could use another character as a notation character for the
"co" constructor. Thus:
notation co (a b c: class): class = ($[$:max) a b c ($]$:0);
prefix cadd: $+$ prec max;
Now you can write [a + [b + c]] and it will be parsed as (co a cadd (co a
cadd b)) just as in metamath. Note that in this situation + is not a binary
operator at all, it is a "nullary prefix" operator, which is to say, a
constant symbol.
> I tried to workaround that by adding a definition
> def mm0AddC(a b: class): class = $(co a caddc b)$;
> that is like a bridge between the 2 trees.
>
> But now, this made me think
> 1) metamath trees are unique but not mm0 trees, because you can have
> definitions that allow to express the same tree in different manners
> As you can see 1 + 2 + 3 can be represented by both trees in mm0 :
> just terms (no definition, which are expended)
> co {
> co {
> 1
> +
> 2
> }
> +
> 3
> }
> and (with definition)
> mm0AddC {
> mm0AddC {
> c1
> c2
> }
> c3
> }
>
I would say: MM0 trees are unique; these are different trees, that happen
to be provably equal. Metamath does not have unique trees in the sense that
a given token string can have two parses (although set.mm doesn't have this
pathology). You have created these two trees by using different parser
configurations for the same string, which is of course fine because the
parser configuration (the sequence of "infix", "notation", etc) is fixed
for a given database.
This is "mm0AddC" is another way to get metamath-ish notations inside MM0,
and probably what I would do in a hand translation. It has some drawbacks,
though. Because the terms are not literally the same as the corresponding
metamath terms, a bunch of additional proofs have to be inserted, and it's
not completely trivial to work out where those proofs should go. What's
more, in metamath because there is only one operation, "co", involved,
there is only one theorem "opeq2d" that gets used for a wide variety of
operations, for example it can prove "B = C -> A + B = A + C" and also "B =
C -> A - B = A - C". In MM0, these are two different syntax constructor,
rather than the same syntax constructor with a different middle argument,
so you need different theorems for these two cases. (MM1 will automatically
generate all such equality theorems so the user pain around this is
minimal.) But in an automated translation that means you have to do
something clever whenever this theorem gets used.
> 2. set.mm.mm0 might not be the correct way to express maths in mm0 (ok,
> I'm naive).
> It provides nice tests for the parsers/verifiers but eventually math will
> have to be rewritten in mm0
>
> For example, maybee the 3 arguments structs like co should disappear.
> They make it nice to have equalities like A=B, C= D, E=F -> ( A C E ) = (
> C D F ) for a lot of operators but they don't play well with mm0
> parser/trees
>
> the logical stuff (and or, not)/2 args stuff should be simpler to migrate
> to mm0
>
Actually, I find MM0 much nicer to use than metamath when it comes to
functions with 3 or more arguments, which come up a lot in the computer
science type applications I have been working on. That's because there is a
notation that requires no "notation", the default notation that everything
gets, which is "foo x y z". This generalizes trivially to any number of
arguments and does not require any parser directives, so it is the natural
option for big and complicated predicates with many arguments. In metamath
you would have to define a new notation for this, and the syntax is not so
great; for functions you have the options of ( foo ` <. a , b , c >. )
(which doesn't generalize past 3), ( foo ` <. a , <. b , c >. >. ), ( foo `
<" a b c "> ), or ( ( ( foo ` a ) ` b ) ` c ) (which doesn't always work
for class functions). The most generally applicable form is ( foo ` <. a ,
<. b , c >. >. ), but the syntax is the worst among all the options. (The
<" A B ... Z "> notation was created specifically for this use case, but
you still have to select the right constructor depending on how many
arguments you have, and the notation gets verbose again once you get past 8
arguments.) You can also do funny things with arguments on the left and
right with stuff like ( c ( a foo b ) d ) to make it more compact but this
is pretty mind bending to read.
But tools that refactor the mm theory/proofs into mm0 friendly expression
> should probably be written/used to translate set.mm into a more working
> condition for mm0
>
> Probably quite a lot of things will have to change (And I had this hope to
> implement mephistolus on mm0 in 2 months, ahah, I'm so dumb...)
> It will be hard as refactoring set.mm.mm0 requires refactoring the proof
> at the same time, which is not easy at a point in time where there aren't
> that many tools available
>
> 3. I'm wondering how set.mm should be turned into mm0. What are the major
> implementation differences ?
>
Well, I think you've already seen the answer. The logical part is a one
time cost; there is some work on the translator and then boom, you've got
megabytes of raw MM0 to play with. That's already happened, but as you can
see this leaves a lot to be desired when it comes to presentation. If you
analyze the notations with an eye for the way set.mm writes things, you can
probably reverse engineer a good number of MM0 notations. For example,
things like df-an are easy (although you would have to specify the
precedence and associativity manually, because metamath doesn't have any
information to give in that regard). Some notations would have to change,
like df-al and df-ral overlap their first symbol, which is not allowed. So
for an automatic translation you have to somehow stick disambiguating marks
on things without it looking terrible. And then there are notations "via
co", which are difficult because you don't know which operations are going
to be used in advance. If you want to declare a new constructor like your
"mm0AddC" for each operation, you have to identify that df-pl, whose
definition is |- + = ..., is a class that is meant to be used as a binary
operation, whereas "|- 0 = ..." is a constant, not a binary operation, and
"|- sin = ..." is a unary operation. One cue is that the binary operations
are usually declared using df-mpt2, but not always. But there will always
be "funny terms" like ( a ( x e. A , y e. B |-> C ) b ) that will actually
be using co directly, so there is a fallback option if detection doesn't
work out, and this can be viewed as an optimization.
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJStKhWc%2BYbNDv4n91TFwC%3Ddp2cVLjJj_AUxELgE1BPXjfg%40mail.gmail.com.
