> > > 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. >
Ok > I would say: MM0 trees are unique; these are different trees, that happen > to be provably equal. > Ok > 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). > Yes, I see your point. They were easy to reason about though (if you work with the (false) asumption that ambiguous parse don't happen in real life)... Well, Mathematics are probably telling me : "if there are more than one tree for the same meaning, that's how it should be, deal with it" > 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. > for the sake of our potential future conversation, is "different parser configurations" equal to 1) "the different mm0 statements I made it gobble" ? 2) "the different strings that the parser had to parse ? > 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. > already smells like trouble :/ > 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. > Yes, I guessed so. > (MM1 will automatically generate all such equality theorems so the user > pain around this is minimal.) > I'll have to do that too. MM1 and Mephistolus share some concerns (both are proof authoring tools) > >> > 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. > > S-expression stuff. At the moment, I'm implementing mm0 trees by having `data class MM0Tree(val id:String, val children:List<MM0Tree>) But I could have MM0STree(val args:List<T>) with args[0]=id and args.frop(1) = children I guess that it would be about the same optimization/view that the S expression I still have to implement in place verification of the mmb proofs. When I do that, I'll probably have to implement a S-expression like view > 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. > Don't go sybilic/esoteric on me (I'm bad at catching subtle hints :/). I saw the mm0-hs fromMM translation tool that gets me a nice mm0 file from mm stuff. I like that, by the way. > 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. > I'm not sure that I understand all that you say but maybe I got the gist of it. Anyway, here is my plan : 1) I'll use mm0-hs fromMM to translate stuff from mm into a raw mm0 file 2) I'll implement a patcher/refactor/remaper machine that eats a mm0+mmu file and spit a new enhanced mm0+mmu file (in kotlin :/, I'll open source it though because it is important to be available to anyone)...I'll get to mmb when I get to mmb. :) 3) I'll write public patchs to slowly turn set.mm into a mm0 file that use the features mm0 can provide (I hope to get some advice/guidance from you and others for that) First, I'll start with id remapping, those c1, c2, ..., c9 scream to be renamed 1, 2, ..., 9 to get usable directly in the mathparser without addition. I'll strive to replace stuff, remove stuff and add stuff only when absolutely necessary. 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/8b4a8ec4-a61d-4147-abfa-9aa8dd63a4dc%40googlegroups.com.
