I have just started having a look at working with the translation to mm0 of
set.mm (that I'll call set.mm.mm0).
I started with trying to turn "1 + 1 = 2" into a tree
As set.mm.mm0 is a raw translation from set.mm, (without mm0 features like
operators(simple notations)/notations
(constructs)/definitions/coercions(set -> class)),
I used the dynamic parser built against set.mm.mm0 to parse
"( wceq ( co c1 caddc c1 ) c2 )"
to get
wceq {
co {
c1
caddc
c1
}
c2
}
The tree is correct, but the string I had to write to get the tree is not
to my liking, I just wanted to write "1 + 1 = 2" to get that tree.
But for that, you have to introduce some simple notations
For my second try, I experimented with "1 + 2 + 3"
First, I enhanced set.mm.mm0 with some operators with
prefix c1: $1$ prec max;
prefix c2: $2$ prec max;
prefix c3: $3$ prec max;
infixl mm0AddC: $+$ prec max;
def mm0AddC(a b: class): class = $(co a caddc b)$;
and then, I got
mm0AddC {
mm0AddC {
c1
c2
}
c3
}
out of
"1 + 2 + 3"
and I got
mm0AddC {
c1
mm0AddC {
c2
c3
}
}
out of 1 + (2+3)
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
}
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
}
When definitions are expanded, this uniqueness should come back. But it
implies more complicated reasonning/checks on trees.
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
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 ?
Oh well, back to play with it...
Best regards,
Olivier
--
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/379a1217-bf4f-4d36-ac7d-839749adbea8%40googlegroups.com.
