Hello
I have started working with mm0 and I'll be using this thread to talk about
it.
My goals with this thread :
By explaining what I have understood about mm0, I might
- gain even better insights, especially if people interact and correct
me.
- get some sound advice
- make it easier for other people to understand what mm0 is and what it
can do
I'll be comparing mm0 with metamath (and somewhat evangelising mm0) :
- because I have worked a lot with metamath and I need to know how the
same things can be done in mm0 and what are the benefits and the pain
points of using mm0 over metamath
I'll somewhat evangelized mm0 (I'm sold to it and so I got a bias) though
I'll try to be fair with the awesomeness that is metamath (but remember
that I am human, correct me when I am wrong please)
- at some point in time, when mm0 is ready (stable, with much better
tooling than metamath), I hope that people will jump ships because the
(human brains/contributions of the) metamath community is really really
precious and such a community is needed for mm0 also (at the moment, there
is Mario... me since a few days... and hopefully others)
You have been warned :)
Let's dive into the subject :
mm0 and metamath can have the exact same internal representation of math
expressions as trees.
the tree Node(wi) { Node(ph) { Node(wi) {Node(ps) Node(th)}}} where we have
Node(id){ 0+ node children here},
- represents the metamath string "( ph -> ( ps -> th ) )"
- represents the mm0 string "( ph -> ( ps -> th ) )" or the string "ph ->
ps -> th" or the string "ph -> (ps -> th)" or the string "ph -> (ps -> th
)"
the parsers for mm0 is way more simpler that the one for metamath
- I wrote a pure kotlin antlr parser for metamath (I'll open source it)
that is somewhat heavyweigth :
- it requires a few second to build from cold start (I guess you have to
build a huge automat to make it work)
- it has a dependency on a pure kotlin antlr runtime
- it is be cpu intensive in some complex case (If I remember correctly)
- it work on the jvm (battle tested), on the browser/javascript (tested)
and should work on native platforms like linux, windows, mac, ios,
android, webasm (not tested yet)
- it is reasonnably fast (it is possible to build decent tools with that,
see the mephistolus videos)
- it is *static* and only works for a particular version of set.mm
- I wrote a pure kotlin primary mm0 parse (I'll open source it)
- it is really lightweight : instantaneus to build (it is just a string
and a few variables)
- it is performant (just looks the next token for branching, really
simple, no headaches, minimal branches, minimal string copy operations
- lightest on cpu/memory
- works on every platform, no dependency, easily portable (360 locs for
the parser, 60 locs for the tree structure)
-I wrote a pure kotlin secondary dynamic mm0 parser (I'll open source it)
- same stuff that the primary parser
- Major feature : it is dynamic, you can enhance it *at runtime* with
- sorts (stuff you care about) like wffVar, classVar, setvar but it
could also be nat (natural number ?), or other things (I guess that "|-" is
not needed because it is embedded in the mm0 language/keywords)
strict provable sort wff;
pure sort set;
strict sort class;
- operators/tree nodes (term) : like the implication or the negation
logical operators
term wi (ph ps: wff): wff;
term wn (ph: wff): wff;
- definitions (def), like you define logical and from from the logical
implication and negation
def wa (ph ps: wff): wff = $ ~(ph -> ~ps) $;
- binary operators symbols (simple notations) : you can associate one
(or many) symbols to a binary operator (a term or a definition) to allow
the parser to work with it
infixl wa: $/\$ prec 20;
infixr wi: $->$ prec 25;
prefix wn: $~$ prec 40;
- constructs (general notations) like { x | ph }
notation cab {x: set} (ph: wff x): class = (${$:0) x ($|$:0) ph ($}$:0);
- delimiters (tokens for the parser are split around delimiters)
delimiter $ ( ) ~ { } $;
Major features :
- you can tune the parser to recognise ->, =>, \rightarrow,
\longrightarrow for id=wi,k so users from different part of the world can
have the notation they like
- someone without years of mathematical training can write ((ph -> (ps
-> th )) and still be understood by the parser, without complain about
missing spaces, etc..
This helps to lessen the barrier of entry to computer checked maths
mm0 was designed for expressiveness and efficiency and so it cleanly
separates in the software code stuff (variables, different structures) that
are all bundled together in a metamath string
like in the metamath string
|- ( ph -> ( ps -> th ) )
you have
- the provable notion |-
- variables, that have the wffVar types : ph, ps, th
- the term constructors wff ( ph -> ps )
- with substitution type checking/correctness wff ( ph -> ps ), wff ( ph
-> ( ps -> th ) )
Well, that's all for documenting today...
In the future, I would like to ask (or speak when I have understood it)
about
- definition unfolding in proofs (what is the point with that ?, does it
make things simpler, more efficient ? I would like to work with <-> and not
with unfolded -> and not ? )
- the possibility of having variadic antecedents in a theorem
(mephistolus uses Gamma|-ph theorems instead of |-ph theorems...in the form
of ( v0w -> v1w ) + ( v0w -> ( v1w -> v2w ) ) ---> ( v0w -> v2w ) where
v0w stands for any number of antecedents
- dummy variables
- distinct variables (does mm0 have that ? does it need it, or is the
free/bound of variables built in mm0 enough to get things done)
- open term (what are the possibilities of that compared to HOL
metavariables/compared to what mm has)
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/d86bc363-9c4f-4430-a39d-172a27e5495b%40googlegroups.com.
