Metamath Zero

1055 views
Skip to first unread message

Mario Carneiro

unread,
Feb 20, 2019, 6:32:56 AM2/20/19
to metamath
I'm experimenting with a new language, Metamath Zero, an amalgamation of Metamath, Ghilbert and Lean syntax. The goal is to balance human readability and ease of writing a verifier, while also making some attempts to patch the bugs in metamath soundness (not that it's wrong, but there is a lot of soundness justification currently happening outside the metamath verifier kernel). Without giving too much explanation of what the syntax means (it's all fictional syntax at the moment, there is no parser yet), I would like to use some of you as guinea pigs for the "readability" aspect. How obvious is it what things mean? I will put some more explanatory comments at the end.

  nonempty sort wff;

  var ph ps ch: wff*;

  term wi (ph ps: wff): wff; infixr wi: -> 25;

  term wn (ph: wff): wff; prefix wn: ~ 40;

  axiom ax-1: << ph -> ps -> ph >>

    (wi ph (wi ps ph));

  axiom ax-2: << (ph -> ps -> ch) -> (ph -> ps) -> ph -> ch >>

    (wi (wi ph (wi ps ch)) (wi (wi ph ps) (wi ph ch)));

  axiom ax-3: << (~ph -> ~ps) -> ps -> ph >>

    (wi (wi (wn ph) (wn ps)) (wi ps ph));

  axiom ax-mp:

    << ph >> ph ->

    << ph -> ps >> (wi ph ps) ->

    << ps >> ps;


  theorem a1i: << ph >> ph -> << ps -> ph >> (wi ps ph);


  def wb (ph ps: wff): wff :=

    << ~((ph -> ps) -> ~(ps -> ph)) >>

    (wn (wi (wi ph ps) (wn (wi ps ph)))) {

    infix wb: <-> 20;


    theorem bi1: << (ph <-> ps) -> ph -> ps >>

      (wi (wb ph ps) (wi ph ps));

    theorem bi2: << (ph <-> ps) -> ps -> ph >>

      (wi (wb ph ps) (wi ps ph));

    theorem bi3: << (ph -> ps) -> (ps -> ph) -> (ph <-> ps) >>

      (wi (wi ph ps) (wi (wi ps ph) (wb ph ps)));

  }


  def wa (ph ps: wff): wff := << ~(ph -> ~ps) >> (wn (wi ph (wn ps))) {

    infix wa: /\ 20;

    theorem df-an: << (ph /\ ps) <-> ~(ph -> ~ps) >>

      (wi (wa ph ps) (wn (wi ph (wn ps))));

  }


  def wtru (bound p: wff): wff := << p <-> p >> (wb p p) {

    notation wtru := << T. >>;

    theorem df-tru: << T. <-> (ph <-> ph) >> (wb wtru (wb ph ph));

  }


  pure nonempty sort set;

  bound x y z w: set;


  term wal (x: set) (ph: wff x): wff; prefix wal: A. 30;


  def wex (x: set) (ph: wff x): wff :=

    << ~A. x ~ph >> (wn (wal x (wn ph))) {

    prefix wex: E. 30;


    theorem df-ex: << E. x ph <-> ~A. x ~ph >>

      (wb (wex x ph) (wn (wal x (wn ph))));

  }


  axiom ax-gen: << ph >> ph -> << A. x ph >> (wal x ph);

  axiom ax-4: << A. x (ph -> ps) -> A. x ph -> A. x ps >>

    (wi (wal x (wi ph ps)) (wi (wal x ph) (wal x ps)));

  axiom ax-5 (ph: wff): << ph -> A. x ph >> (wi ph (wal x ph));


  var a b c: set;

  term weq (a b: set): wff;

  term wel (a b: set): wff;


  {

    local infix weq: = 50;

    local infix wel: e. 40;


    def weu (x: set) (ph: wff x): wff :=

      << E. y A. x (ph <-> x = y) >>

      (wex y (wal x (wb ph (weq x y)))) {

      prefix wex: E! 30;


      theorem df-ex: << E! x ph <-> E. y A. x (ph <-> x = y) >>

        (wb (weu x ph) (wex y (wal x (wb ph (weq x y)))));

    }


    axiom ax-6: << E. x x = a >> (wex x (weq x a));

    axiom ax-7: << a = b -> a = c -> b = c >>

      (wi (weq a b) (wi (weq a c) (weq b c)));


    axiom ax-8: << a = b -> a e. c -> b e. c >>

      (wi (weq a b) (wi (wel a c) (wel b c)));

    axiom ax-9: << a = b -> c e. a -> c e. b >>

      (wi (weq a b) (wi (wel c a) (wel c b)));


    axiom ax-10: << ~A. x ph -> A. x ~ A. x ph >>

      (wi (wal x ph) (wal x (wn (wal x ph))));

    axiom ax-11: << A. x A. y ph -> A. y A. x ph >>

      (wi (wal x (wal y ph)) (wal y (wal x ph)));

    axiom ax-12 (ph: wff y): << A. y ph -> A. x (x = y -> ph) >>

      (wi (weq x y) (wi (wal y ph) (wal x (wi (weq x y) ph))));


    axiom ax-ext: << A. x (x e. a <-> x e. b) -> a = b >>

      (wi (wal x (wb (wel x a) (wel x b))) (weq a b));

    axiom ax-rep (ph: wff y z):

      << A. y E. x A. z (ph -> z = x) ->

         E. x A. z (z e. x <-> E. y (y e. a /\ ph)) >>

      (wi (wal y (wex x (wal z (wi ph (weq z x)))))

          (wex x (wal z (wb (wel z x) (wex y (wa (wel y a) ph))))));

    axiom ax-pow: << E. x A. y (A. z (z e. y -> z e. a) -> y e. x) >>

      (wex x (wal y (wi (wal z (wi (wel z y) (wel z a))) (wel y x))));

    axiom ax-un: << E. x A. y (E. z (y e. z /\ z e. a) -> y e. x) >>

      (wex x (wal y (wi (wex z (wa (wel y z) (wel z a))) (wel y x))));

    axiom ax-reg:

      << E. x x e. a -> E. x (x e. a /\ A. y (y e. x -> ~ y e. a)) >>

      (wi (wex x (wel x a))

          (wex x (wa (wel x z) (wal y (wi (wel y x) (wn (wel y a)))))));

    axiom ax-inf:

      << E. x (a e. x /\ A. y (y e. x -> E. z (y e. z /\ z e. x))) >>

      (wex x (wa (wel a x) (wal y (wi (wel y x)

        (wex z (wa (wel y z) (wel z x)))))));

    axiom ax-ac:

      << E. x A. y (y e. a -> E. z z e. y ->

         E! z (z e. y /\ E. w (w e. x /\ y e. w /\ z e. w))) >>

      (wex x (wal y (wi (wel y a) (wi (wex z (wel z y))

        (weu z (wa (wel z y) (wex w

          (wa (wa (wel w x) (wel y w)) (wel z w)))))))));

  }


  nonempty sort class;

  var A B: class*;

  term cab (x: set) (ph: wff x): class;

  term welc (a: set) (A: class): wff;

  notation cab (x: set) (ph: wff x) := << { x | ph } >>;


  {

    local infix welc: e. 50;

    axiom ax-8b: << a = b -> a e. A -> b e. A >>

      (wi (weq a b) (wi (welc a A) (welc b A)));


    axiom ax-clab: << x e. {x | ph} <-> ph >>

      (wb (welc x (cab x ph)) ph);


    def wceq (A B: class): wff :=

      << A. x (x e. A <-> x e. B) >>

      (wal x (welc x A) (welc x B)) {

      infix wceq: = 50;


      theorem df-ceq: << A = B <-> A. x (x e. A <-> x e. B) >>

        (wb (wceq A B) (wal x (welc x A) (welc x B)));

    }


    def cv (a: set): class := << {x | wel x a} >>

      (cab x (wel x a)) {

      coercion cv: set -> class;


      theorem df-cv: << a e. b <-> wel a b >>

        (wb (welc a (cv b)) (wel a b));

    }

  }


  def wcel (A B: class): wff :=

    << E. x (x = A /\ welc x B) >>

    (wex x (wceq (cv x) A) (welc x B)) {

    infix wcel: e. 50;


    theorem df-cel: << A e. B <-> E. x (x = A /\ welc x B) >>

      (wb (wcel A B) (wex x (wceq (cv x) A) (welc x B)));

  }


* The "sort" keyword declares a new typecode.
* "var" is like "$f".
* "bound" is another kind of variable, that can appear in binders. (Each mm0 sort is represented by two mm sorts, one for bound variables and one for terms. Only bound variables can participate in DV conditions.)
* "term" declares a new axiomatic term constructor.
* DV conditions are implicitly declared by saying what a variable depends on. The global wff variables are declared with type " wff* " meaning that they are open terms, they are not disjoint from anything. The global set variables a,b are declared as "set" meaning that they are disjoint from all bound variables in theorems containing these variables. Bound variables are always disjoint from each other.
* "def" declares a definition. Different from both Ghilbert and Metamath, definitions here are "limited lifetime unfolded". Each def has a block after it containing one or more theorems about the definition. These theorems are proven where the definition is replaced by the definiendum, and once the block is closed these theorems are the only access to the definition. (This enables some information privacy if desired.) See wb for example, which uses characterizing theorems instead of an iff.
* The notation system turned out a bit more complicated than I'd hoped. Each "math expression" is stated twice, once in chevrons and once in s-expression notation. The intent is that the system actually uses the s-expressions to represent the axioms (so there is no parse tree funny business), and because they form part of the trust base they are displayed to the user. The notation in the chevrons is checked only in the reverse direction - the s-expression is printed and compared to the given string. (In an IDE there would be a mode where you only type the notation and the computer generates the s-expression.) There is still a danger of ambiguous parsing, but at least you can see the parse directly in the case of a mismatch, and the worst effect of a bad parse is that the theorem being proven is not what the user thought - the ambiguity can't be further exploited in the proof.

You might wonder where the proofs are. They go in a separate file, not human readable. The idea is that this file contains all the information that is necessary to appraise the content and correctness of a theorem, and the proof file is just directions to the verifier to produce a proof of the claimed theorems. In particular, if this "specification file" is inspected and correct, then there is no possible input for the proof file that makes the verifier falsely accept a bad theorem. (So no adding axioms, although new definitions are okay.)

I'm curious to hear what you all think of a project such as this. I'm especially interested in ways to simplify the grammar if we can retain readability.

Mario Carneiro

ookami

unread,
Feb 20, 2019, 8:11:20 AM2/20/19
to Metamath


Am Mittwoch, 20. Februar 2019 12:32:56 UTC+1 schrieb Mario Carneiro:
I'm experimenting with a new language, Metamath Zero, an amalgamation of Metamath, Ghilbert and Lean syntax. The goal is to balance human readability and ease of writing a verifier, while also making some attempts to patch the bugs in metamath soundness (not that it's wrong, but there is a lot of soundness justification currently happening outside the metamath verifier kernel). Without giving too much explanation of what the syntax means (it's all fictional syntax at the moment, there is no parser yet), I would like to use some of you as guinea pigs for the "readability" aspect. How obvious is it what things mean? I will put some more explanatory comments at the end.

  nonempty sort wff;

  var ph ps ch: wff*;

  term wi (ph ps: wff): wff; infixr wi: -> 25;


What does the number say? Is it a precedence weight? Is the right-associativity hinted somewhere?

 

  term wn (ph: wff): wff; prefix wn: ~ 40;

  axiom ax-1: << ph -> ps -> ph >>

    (wi ph (wi ps ph));

Is the line above an interpretation of the human readable infix, right-associative implication chain within double-angle brackets? In UPN format?

  axiom ax-2: << (ph -> ps -> ch) -> (ph -> ps) -> ph -> ch >>

    (wi (wi ph (wi ps ch)) (wi (wi ph ps) (wi ph ch)));

  axiom ax-3: << (~ph -> ~ps) -> ps -> ph >>

    (wi (wi (wn ph) (wn ps)) (wi ps ph));

  axiom ax-mp:

    << ph >> ph ->

    << ph -> ps >> (wi ph ps) ->

    << ps >> ps;


I'm at work, and have no time to go through the whole grammar file now, but I will after work.

Wolf

Sauer, Andrew Jacob

unread,
Feb 20, 2019, 11:00:26 AM2/20/19
to meta...@googlegroups.com
That looks awesome! And it's not much harder to read than Metamath, if at all.

--
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 metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

Raph Levien

unread,
Feb 20, 2019, 11:08:57 AM2/20/19
to Metamath Mailing List
I haven't dug deeply into understanding this, but it warms my heart that ideas from Ghilbert are being considered to push Metamath forward, and this direction looks fairly solid to me. I completely agree that the soundness story in current Metamath is rough, and this was one of the main motivations for Ghilbert. On the other hand, I bit off more than I could chew, and mostly never quite figured out an appropriate module system, or a way to reconcile types (of a dependent flavor) with the mostly untyped approach of Metamath. I think an intermediate approach like this could fly.

Raph
Message has been deleted

David A. Wheeler

unread,
Feb 20, 2019, 1:48:33 PM2/20/19
to metamath, metamath
On Wed, 20 Feb 2019 06:32:39 -0500, Mario Carneiro <di....@gmail.com> wrote:
> I'm experimenting with a new language, Metamath Zero, an amalgamation of
> Metamath, Ghilbert and Lean syntax.

I'm hoping it'll be designed so databases like set.mm and iset.mm can be
automatically converted into it. It looks like that's the case.

Syntax should be simple, though "simple" is in the eye of the beholder :-).

> var ph ps ch: wff*;

I don't see why you need a "*" here.

> term wi (ph ps: wff): wff; infixr wi: -> 25;

Why do you need to repeat "wi:" here?
I wonder if adding a "precedence: 25" would help, else the number is a mystery.

> axiom ax-1: << ph -> ps -> ph >>
> (wi ph (wi ps ph));

I see the s-expression below the axiom, but isn't that trivial to re-discover?
I think you should apply "Don't repeat yourself (DRY)", or a verifier will
have to recheck something that shouldn't need to be said at all.

> axiom ax-mp:
>
> << ph >> ph ->
> << ph -> ps >> (wi ph ps) ->
> << ps >> ps;

That's a lot of chevrons, and that seems much harder to follow
than metamath's current approach.
Axioms, in particular, are a big deal. It should be
"as obvious as possible" to the reader that they're correct.

I'm fine with s-expressions, but a lot of people DO NOT understand them.
If you make people input s-expressions, you might lose
some people entirely. In cases where the s-expression can be easily determined,
you shouldn't make a human create them.

You might consider using neoteric expressions instead of s-expressions.
They have the same meaning, but look more like math.
Basically "x(a b c)" means the same thing as "(x a b c)".
More details available here from Readable Lisp (my project):
https://readable.sourceforge.io/

That would convert this:
> (wn (wi (wi ph ps) (wn (wi ps ph))))
into this:
> wn(wi(wi(ph ps) wn(wi(ps ph))))


> theorem bi2: << (ph <-> ps) -> ps -> ph >>
> (wi (wb ph ps) (wi ps ph));

Again, I don't see why you need to expressly state the syntax proof.
It's noise for the human, and the computer can recalculate & check that trivially.

I see infixr. Are you planning to support arbitrary-length expressions of the
same operator, e.g., "( 1 + 2 + 3 + 4 )"?

> * The notation system turned out a bit more complicated than I'd hoped.
> Each "math expression" is stated twice, once in chevrons and once in
> s-expression notation. The intent is that the system actually uses the
> s-expressions to represent the axioms (so there is no parse tree funny
> business), and because they form part of the trust base they are displayed
> to the user. The notation in the chevrons is checked only in the reverse
> direction - the s-expression is printed and compared to the given string.
> (In an IDE there would be a mode where you only type the notation and the
> computer generates the s-expression.) There is still a danger of ambiguous
> parsing, but at least you can see the parse directly in the case of a
> mismatch, and the worst effect of a bad parse is that the theorem being
> proven is not what the user thought - the ambiguity can't be further
> exploited in the proof.

Wouldn't it be simpler to simply require that you cannot add a new
axiom or definition if it results in a syntactic ambiguity?
I *think* that would get rid of the "funny business" while eliminating duplicate
declarations. But that depends on what "funny business" you mean,
and I'm not sure I know what you're referring to.

> You might wonder where the proofs are. They go in a separate file, not
> human readable. The idea is that this file contains all the information
> that is necessary to appraise the content and correctness of a theorem, and
> the proof file is just directions to the verifier to produce a proof of the
> claimed theorems.

I think it's important that the proofs include the specific step-by-step instructions
as metamath does now - that makes it trivial to verify by humans and computers.
If it *also* has higher-level instructions (say, to try to reconstruct a proof if some
definitions have changed) that's fine.

--- David A. Wheeler

David A. Wheeler

unread,
Feb 20, 2019, 10:40:36 PM2/20/19
to metamath, metamath
On Wed, 20 Feb 2019 06:32:39 -0500, Mario Carneiro <di....@gmail.com> wrote:
> I'm experimenting with a new language, Metamath Zero, an amalgamation of
> Metamath, Ghilbert and Lean syntax. The goal is to balance human
> readability and ease of writing a verifier, while also making some attempts
> to patch the bugs in metamath soundness (not that it's wrong, but there is
> a lot of soundness justification currently happening outside the metamath
> verifier kernel).

If possible, I think it'd be good to have an additional reason to create a new language,
or at least argue why similar results can't be done with tweaks to
existing mechanisms like $j.

1. Putting more soundness justifications into the underlying verifier
is indeed a worthy goal. But most of set.mm is proofs, not definitions,
and there are very few "axioms" in the traditional sense... so it's not clear
that all the verifiers need to check that so much.
I can also imagine tweaking existing systems instead of creating a new language.

2. Making the input "more readable" is worthwhile, but I'm not sure that
by *itself* this is enough. Making it so that we can be more flexible
about parentheses would *certainly* be a nice improvement.
Supporting ph /\ ps /\ ch /\ ... would be nice as well.

Expanding on #2: If it can manage to easily support arbitrary-length arguments like
ph /\ ps /\ ch /\ th /\ ... then I can suddenly see that it's able to do something
that Metamath today can't. Is that easy? Worth it?
I don't know, but that *would* go beyond our current setup.

No matter what, I recommend that you do NOT depend
too much on precedence, even when available.
"Developer beliefs about binary operator precedence (part 1)” by Derek M. Jones
http://www.knosof.co.uk/cbook/accu06.html
"a survey of developers at the 2006 ACCU conference to determine if they correctly applied the precedence and associativity of the binary operators common to C, C++, C#, Java, Perl, and PHP. In this experiment only 66.7% of the answers were correct (standard deviation 8.8, poorest performer 45.2% correct, best performer 80.5% correct); this was not much better than random chance (50%). Even many widely-used operator pairs had relatively poor results; only 94% of the problems were correctly solved when they combined * and +, 92% when they combined * and -, and 69% when they combined / and +."
Professional mathematicians probably do get precedence correct, but where possible I'd like the results to be understood by others.

When we developed my "Readable Lisp" we supported infix but decided to NOT support precedence. The trade-offs are very different here, so I don't think that reasoning really applies here. But my point is that supporting lots of precedence levels isn't really, by itself, a big win.

> * "def" declares a definition. Different from both Ghilbert and Metamath,
> definitions here are "limited lifetime unfolded". Each def has a block
> after it containing one or more theorems about the definition. These
> theorems are proven where the definition is replaced by the definiendum,
> and once the block is closed these theorems are the only access to the
> definition. (This enables some information privacy if desired.) See wb for
> example, which uses characterizing theorems instead of an iff.

That makes sense. However, in some cases you will want a way to say
"don't use this theorem" so you can prove statements that you don't use.

But what about proving theorems that have to "reach into" multiple definitions to work?
You might need a way to express that you're intentionally breaking the rules.

> * The notation system turned out a bit more complicated than I'd hoped.
> Each "math expression" is stated twice, once in chevrons and once in
> s-expression notation.

As I noted earlier, stating things twice is undesirable,
and I don't think it's necessary in this case.

--- David A. Wheeler

Mario Carneiro

unread,
Feb 20, 2019, 10:48:01 PM2/20/19
to metamath
Thank you everyone for all the suggestions. I will see if I can respond to each of them.

On Wed, Feb 20, 2019 at 8:11 AM 'ookami' via Metamath <meta...@googlegroups.com> wrote:
  nonempty sort wff;

  var ph ps ch: wff*;

  term wi (ph ps: wff): wff; infixr wi: -> 25;


What does the number say? Is it a precedence weight? Is the right-associativity hinted somewhere?

It is indeed a precedence number. The right associativity is the "r" suffix, but this command and its cousins have been called out by several people, so I think I need to rethink it. Maybe even having precedences in a numeric order is a bad idea, although I am really wary about making the notation system any more complicated than it already is (and if I can simplify it dramatically that would be even better).

  term wn (ph: wff): wff; prefix wn: ~ 40;

  axiom ax-1: << ph -> ps -> ph >>

    (wi ph (wi ps ph));

Is the line above an interpretation of the human readable infix, right-associative implication chain within double-angle brackets? In UPN format?

What's UPN? The <<quoted>> expression is what it looks like with the notation system, and the s-expression is what the actual axiom is for the verifier.
 

On Wed, Feb 20, 2019 at 11:18 AM j4n bur53 <burs...@gmail.com> wrote:
How do you forbid quantification over classes. Does this happen
since it is a new sort (your nonempty sort class;)

Problem is, you might end up with something else than ZFC.

The "nonempty" modifier provides the ability to use bound variables of this sort (i.e. dummy variables). In metamath all sorts are nonempty in this sense. You can't declare a "bound X: class" if the sort "class" wasn't defined as nonempty.

But this might seem strange then, because I'm saying that you *can* quantify over classes. Why isn't it stronger than ZFC? In order to use this power, you also have to declare a binding syntax constructor for the sort. For example,
 

term wal (x: set) (ph: wff x): wff; term cab (x: set) (ph: wff x): class;


This declares wal and cab as binding operators (ph depends on the variable x), so there is a way to quantify over sets in the wff and class sorts. Without a similar operator for classes, you can't quantify over classes in the term language.

But why are we allowing bound wffs and classes anyway? Consider the definition of wtru:

  def wtru (bound p: wff): wff := << p <-> p >> (wb p p) {

    notation wtru := << T. >>;

    theorem df-tru: << T. <-> (ph <-> ph) >> (wb wtru (wb ph ph));

  }


The red coloration of the wff is deliberate here: p is a "bound wff" in the definition. As a syntax operator, "wtru" has 0 arguments, not 1. This is no different from a dummy bound variable in a definition like weu:

  def weu (x: set) (ph: wff x) (bound y: wff): wff :=

    << E. y A. x (ph <-> x = y) >>

    (wex y (wal x (wb ph (weq x y)))) {

    prefix wex: E! 30;


    theorem df-eu: << E! x ph <-> E. y A. x (ph <-> x = y) >>

      (wb (weu x ph) (wex y (wal x (wb ph (weq x y)))));

  }


(In the original post I didn't include the (bound y) quantifier but it's implicitly pulled in by the "bound y" top level declaration. I will need to work on the exact rules for how these variables get inferred, a process similar to the "optional $f" hypotheses in metamath axioms and theorems.) The meaning of a bound quantifier is that it doesn't appear in the syntax constructor (weu gets 2 arguments, wtru gets 0) but it does appear in the definition itself. This is a weird thing to do in a HOL context, but the idea is that if you know the sort is nonempty in the usual sense, then you can use this to choose values for the dummy variables. I haven't said how these theorems get translated to proof obligations but the actual theorem df-tru to be proven is

proof df-tru: (ps <-> ps) <-> (ph <-> ph) := ...

(the concrete syntax here is irrelevant, this is actually part of the binary companion file). Similarly for df-eu - the dummy bound variables are renamed and the fixed arguments aren't:

proof df-eu: E. z A. x (ph <-> x = z) <-> E. y A. x (ph <-> x = y) := ...

For most definitions this proof will be some variety of biid, but for dummy variable renames like this it will be a metatheorem which can be automated by a prover.

Here is a wish for a new system dubbed "Shullivan":
The ability to directly work with infix, etc.. no redundancy
 
with chevrons. I guess chevrons are only comments?

The chevrons are "checked comments", if you like. My idea for avoiding parsing is to take the s-expression, print it, and compare the result token-for-token with the input string (ignoring whitespace). There is still some potential for abuse if you write an ambiguous grammar, where the danger is that an ambiguous expression is disambiguated in the s-expression in a way other than what the reader expected, but the s-expression is at least available for reference.


On Wed, Feb 20, 2019 at 1:48 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:
On Wed, 20 Feb 2019 06:32:39 -0500, Mario Carneiro <di....@gmail.com> wrote:
> I'm experimenting with a new language, Metamath Zero, an amalgamation of
> Metamath, Ghilbert and Lean syntax.

I'm hoping it'll be designed so databases like set.mm and iset.mm can be
automatically converted into it.  It looks like that's the case.

It is indeed a design goal that metamath zero files can be translated to metamath files, as well as to HOL, without much encoding overhead. This means that the primitive constructs are chosen so that they both have a reasonable interpretation as a multi-sorted first order theory, as well as having a cheap metamath interpretation (so unlike HOL proper substitution will not be a one-step operation).

Translating from metamath to mm0 is a bit trickier, because some annotation information in the mm0 file is not present in mm files. If you skip some of the foundational material (roughly the contents of this file), translating a set.mm-like file should be straightforward and automatable.
 
Syntax should be simple, though "simple" is in the eye of the beholder :-).

To clarify: syntax should be "simple" in the sense of being easy to write a small program to check it, and it should be "readable" in the sense of "look it does what I said".
 
>   var ph ps ch: wff*;

I don't see why you need a "*" here.

This declares these variables as "open wffs", meaning that by default they are assumed not to be disjoint from any bound variables in the axioms and theorems. Notice that ax-5 redeclares (ph: wff), while it would normally be imported as (ph: wff x). This means that ph does *not* depend on x, and hence there is a DV condition between ph and x.
 
>   term wi (ph ps: wff): wff; infixr wi: -> 25;

Why do you need to repeat "wi:" here?
I wonder if adding a "precedence: 25" would help, else the number is a mystery.

This is actually two commands, I probably should have put them on separate lines. You are allowed to declare a notation separately from the syntax itself, and this is used for example with wel = "e." to use it as a local notation in the block and then redeclare e. to mean welc and then wcel (which is the global notation, once the class setup is complete). Metamath does a slightly sketchy thing here, where all three of these definitions are used via wcel, where first we axiomatize wcel (cv x) (cv y), then we generalize to wcel (cv x) A and finally to wcel A B, and the equivalence of these three definitions on their common domain is implicitly assumed.
 
>   axiom ax-1: << ph -> ps -> ph >>
>     (wi ph (wi ps ph));

I see the s-expression below the axiom, but isn't that trivial to re-discover?
I think you should apply "Don't repeat yourself (DRY)", or a verifier will
have to recheck something that shouldn't need to be said at all.

Here is an important point: This language is intended to be "readable", not "writable". This means that things like boilerplate are okay as long as a mistake in the boilerplate isn't compromising to correctness. In fact, I anticipate that this file will be compiled from a slightly less verbose version (not much, because it needs to be directly inspectable) where various things can be omitted. See the next point.
 
>   axiom ax-mp:
>
>     << ph >> ph ->
>     << ph -> ps >> (wi ph ps) ->
>     << ps >> ps;

That's a lot of chevrons, and that seems much harder to follow
than metamath's current approach.
Axioms, in particular, are a big deal.  It should be
"as obvious as possible" to the reader that they're correct.

I didn't demonstrate this in the file, but the chevrons are optional. So you could just write:

axiom ax-mp: ph -> (wi ph ps) -> ps;

and it would be understood just as well. In such a small axiom as this that might be a reasonable thing to do (and in particular for single wffs the << ph >> ph business just looks silly). However the s-expressions are NOT optional. This is one of the things that would be omitted in the "less verbose" version of the file - you might just write

axiom ax-mp: << ph >> -> << ph -> ps >> -> << ps >>; 

and the compiler, which has a proper parser, would produce the s-expressions for you.

The problem with metamath's current approach is that it's subtly unsafe, as we saw recently with the example of syntax ambiguity causing proofs of false. Metamath treats statements as lists of symbols, which means that you can do some shenanigans with ambiguity if the grammar supports it. To prevent this, the verifier here works entirely with trees (encoded as s-expressions). So the worst that can happen is that a theorem doesn't say what you think, it can't be exploited in the middle of a proof.

So like I said to Jan, you should think of the chevron expressions as "checked comments"; they are there to help you understand the s-expression, but it's available if you need to double check.

I'm fine with s-expressions, but a lot of people DO NOT understand them.
If you make people input s-expressions, you might lose
some people entirely.  In cases where the s-expression can be easily determined,
you shouldn't make a human create them.

People shouldn't have to write s-expressions, although they may need to look at them as in this file. (Of course I wrote all the s-expressions in the file, perhaps if I make a parser for this file it will point out where I've got it wrong. But that's just because the tool doesn't exist yet.)
 
You might consider using neoteric expressions instead of s-expressions.
They have the same meaning, but look more like math.
Basically "x(a b c)" means the same thing as "(x a b c)".
More details available here from Readable Lisp (my project):
  https://readable.sourceforge.io/

That would convert this:
>     (wn (wi (wi ph ps) (wn (wi ps ph))))
into this:
>     wn(wi(wi(ph ps) wn(wi(ps ph))))

I don't like that spaces are significant with this layout. Also the beginning and end of an s-expression is clear because of matching parentheses, which makes all the rest of the parsing that much easier. (I'm personally also used to this layout from functional programming - this is the usual notation for the lambda calculus.)

>     theorem bi2: << (ph <-> ps) -> ps -> ph >>
>       (wi (wb ph ps) (wi ps ph));

Again, I don't see why you need to expressly state the syntax proof.
It's noise for the human, and the computer can recalculate & check that trivially.

Not if the verifier doesn't have a parser! I'm worried that if I add a parser this will be a large fraction of the code, and it will be a large moving part that could contribute to uncertainty that the program has no bugs. (There will be a parser of course, for the code syntax itself, but it will be statically known so you can write it in a few functions.)

I see infixr.  Are you planning to support arbitrary-length expressions of the
same operator, e.g., "( 1 + 2 + 3 + 4 )"?

That would be handled by declaring "infixl cadd: + 60;" to say that + is left associative with precedence 60. Then "1 + 2 + 3 + 4" would be the printed form of (cadd (cadd (cadd c1 c2) c3) c4).
 
> * The notation system turned out a bit more complicated than I'd hoped.
> Each "math expression" is stated twice, once in chevrons and once in
> s-expression notation. The intent is that the system actually uses the
> s-expressions to represent the axioms (so there is no parse tree funny
> business), and because they form part of the trust base they are displayed
> to the user. The notation in the chevrons is checked only in the reverse
> direction - the s-expression is printed and compared to the given string.
> (In an IDE there would be a mode where you only type the notation and the
> computer generates the s-expression.) There is still a danger of ambiguous
> parsing, but at least you can see the parse directly in the case of a
> mismatch, and the worst effect of a bad parse is that the theorem being
> proven is not what the user thought - the ambiguity can't be further
> exploited in the proof.

Wouldn't it be simpler to simply require that you cannot add a new
axiom or definition if it results in a syntactic ambiguity?
I *think* that would get rid of the "funny business" while eliminating duplicate
declarations.  But that depends on what "funny business" you mean,
and I'm not sure I know what you're referring to.

How will you know if new notation (not axiom/definition) results in a syntax ambiguity? The general problem is undecidable. What I want to avoid is a gnarly grammar with a complicated ambiguity being exploited somewhere deep in the proof (which isn't even being displayed) and causing something to be provable that shouldn't be.
 
> You might wonder where the proofs are. They go in a separate file, not
> human readable. The idea is that this file contains all the information
> that is necessary to appraise the content and correctness of a theorem, and
> the proof file is just directions to the verifier to produce a proof of the
> claimed theorems.

I think it's important that the proofs include the specific step-by-step instructions
as metamath does now - that makes it trivial to verify by humans and computers.
If it *also* has higher-level instructions (say, to try to reconstruct a proof if some
definitions have changed) that's fine.

This language is not intended as a replacement for metamath. It's not designed for showing you proofs. It is intended to convince you *that* a fact is true, not *why* a fact is true. The trustedness of the verifier is an essential component of the design, which is why it has to be so simple. My intention is to use this as the base of a bootstrap chain for more complicated compilers and verifiers, possibly including metamath itself.

There are a variety of sublanguages of mm0 that can be investigated. For example, dropping the notation system makes everything a lot simpler, but now you're staring at s-expressions. Dropping variable declarations means you have to declare them in every axiom/theorem, which is unergonomic but doesn't harm readability. Some of the sort modifiers are not strictly necessary but make translations to FOL easier. Maybe the lowest level of the bootstrap will actually be one of these simplified languages, but if I start asking people to read hexadecimal for the sake of simplifying the program then it makes it much harder to understand what was proven, even if they believe that the program checked *something*. I'm looking for a minimal point on this tradeoff curve - the program is dead simple, the axioms are easy to understand, the theorems are easy to interpret, so if you believe your computer is reliable enough to execute instructions then a theorem has to be true. It's "extreme formal verification".

[Translated from Portuguese]
On Wed, Feb 20, 2019 at 3:09 PM André L F S Bacci <andrebac...@gmail.com> wrote:
On Wed, Feb 20, 2019 at 8:32 AM Mario Carneiro <di....@gmail.com> wrote:
I'm experimenting with a new language, Metamath Zero, an amalgamation of Metamath, Ghilbert and Lean syntax. The goal is to balance human readability and ease of writing a verifier, while also making some attempts to patch the bugs in metamath soundness (not that it's wrong, but there is a lot of soundness justification currently happening outside the metamath verifier kernel). Without giving too much explanation of what the syntax means (it's all fictional syntax at the moment, there is no parser yet), I would like to use some of you as guinea pigs for the "readability" aspect. How obvious is it what things mean? I will put some more explanatory comments at the end.

  nonempty sort wff;

Easy to write a verifier: Stop right here.

A large number of keywords will make any verifier complex. Think about how to be able to declare syntax, in the language itself. This will leave the compiler "soft", but will also allow expansions not to make the collection invalid. Look at proofs in HOL that are no longer possible to run today.

In a language I started, almost all statements started with "def" or "var". This allowed for having zillions of keywords within def, but which were not reserved words in the language itself.

In basic definitions, verbose:


typecode wff ::nonempty;

I agree that lots of keywords makes things harder. But actually there doesn't need to be a notion of "keyword" here, in the sense that just because a command starts with a word like "nonempty" or "term" doesn't mean that these words are unavailable as names of variables or names of axioms/theorems. Each command begins and ends in a definite way, so you should never be guessing about the token class of the next word. That said, it's true that prefix modifiers like "pure nonempty sort set;" can be problematic. In this case I think it's okay since there are a finite number of ways to start a command, so for example the first word of the file can only be "pure", "nonempty", "sort", "var", "def", "{", and so on without any "open classes" like identifiers. After reading "var" or "def" or "sort" we expect an identifier, or in the case of "var" we expect an identifier or ":". It's all expressible as a finite state machine on the token classes. Sentinel tokens like ":" and ";" and "<<" can't be legal identifiers, but beyond that there shouldn't be much constraint necessary. For safety's sake I think identifiers will be limited to roughly alphanumeric sequences anyway, but command-starting "keywords" will be legal identifiers as well.

  var ph ps ch: wff*;


The : is also a keyword from what I understand. Style suggestion. Use var a b c :wff instead of var a b c: wff. That is, leave the : more attached to the type than to one of the variables.

By the way, only one type per variable? Think about adding something like partial types, or to use concepts of statically typed languages, declaring interfaces (::)?


The ":" is indeed a keyword here. I'm not sure I like to align the colon like that, but in Lean syntax (which is the inspiration for most of the concrete syntax here) the colon has spaces on both sides, as in:

var ph ps ch : wff*;

If I separate out all the tokens, it should rightly be

var ph ps ch : wff * ;

(oh, I guess "*" is also a keyword here, that is, identifiers can't contain a * in them) but I think this is a bit ugly, and metamath has often been criticized for its gratuitive spacing. Assuming there is a lexer that can handle lack of spaces, it shouldn't matter how it's aligned. There won't be a "multiple var" statement where you can have different types anyway, you just use "var" multiple times.

  term wi (ph ps: wff): wff; infixr wi: -> 25;

  term wn (ph: wff): wff; prefix wn: ~ 40;


Here I suggest being as verbose as possible, more syntactic than logical.

syntax wi ( ph :wff "->" ps :wff) :wff infix.right 25;

Alternatively:

syntax wi :wff ( ph :wff "->" ps :wff) infix.right 25;

That is, types closest to the name, definition inside the parentheses, operator defined within quotes (escaped by \)

Operators like this, in quotes, allow a bit of language abuse, but also allow you to create things like writing Latex-style operations: \dot

The advantage of having a separate command for prefix/infix/suffix precedence is to tweak the priorities in advance. But it is asking for confusion. I will not suggest taking the command, but at least have the option to put priority in the syntax command itself to encourage it to stay in one place.

For me part of the appeal of the order

term wi (ph ps: wff): wff;

or equivalently

term wi: wff -> wff -> wff;
 
is the direct connection to typing terms in simple type theory. (It's not real STT, so (wff -> wff) -> wff or other things are not allowed. But in as much as I can suggest the connection, I think it is helpful to organize things so the analogy makes sense.) With binders it gets harder to do this so directly, and I think this might be unavoidable given the way metamath handles binding variables and dummy variables, but I try to keep the notation suggestive.

As for putting the syntax in the term, I originally played with the following syntax:

@[infixr -> 25] term wi: wff -> wff -> wff;

The @[...] notation is used for annotations in lean, and it seemed like a nice use for them. But when I wanted to have separate notations I needed a standalone command, and having two syntactic constructs for the same thing seemed like a bad idea. Lean also has a way to apply annotations in a standalone context:

attribute [infixr -> 25] wi; local attribute [infixr -> 25] wi;

But this seems like a lot of extra infrastructure for little readability gain. (I think term -> syntax and infixr -> infix.right are good ideas, though, given that someone already missed the "r" when asking about why this means -> is right assoc.) I grant that having two commands and repeating the name of the term is boilerplate, but I'm not sure that the alternative is  that much more readable. If every term had a mandatory notation I could see that adding them together would be a good idea, but I don't think this is necessary. (I am still not sure what the best approach is here.)

For parsing the arrow properly, my original intent was to use whitespace to separate the token, whatever it is. There should be some lattitude in what is allowed at this spot, in order to allow as many kinds of math notation as possible. Alternatively it could be surrounded by chevrons to reinforce the idea that this is intended for use in the math strings (but it would still need to have spaces around it so that the arrow doesn't lexically collide with the chevrons).

  axiom ax-1: << ph -> ps -> ph >>

    (wi ph (wi ps ph));


Here a weird suggestion, but... Axioms -> syntax. Then use the command, much like...

syntax ax-1 : "ph -> ps -> ph" :: (wi ph (wi ps ph)) ;

Here : and :: are reused, with space to the right (without a type), only to denote clear points for the parser.

Or if you find overloading the syntax ugly (and it is), the suggestion above about "def":

def.syntax wi :wff ( ph :wff "->" ps :wff) infix.right 25;
def.axiom ax-1 : "ph -> ps -> ph" :: (wi ph (wi ps ph)) ;

I don't think this is a good idea. syntax and axiom have different interpretations and different parsing, so there isn't much gain for the parser to use the same word for both. And making them semi-namespaced under "def" doesn't make anything easier - we still have to handle them as different constructs.

Your notation for math string + s-expression is a bit nicer to read than mine, I think, although I hope there won't be too much string escaping going on. (It's supposed to be directly readable so there's no point in escaping things.) Also the string tends to suggest that whitespace is significant and newlines are not allowed, at least to me. (I think set.mm uses " for function image, but we could use '' (two single quotes) instead. Also <" "> (my fault) might be replaceable with <' '> if it's not too confusing. With those replacements, I think you can completely get away with quoting math expressions, which would make everything a lot easier.)

  axiom ax-2: << (ph -> ps -> ch) -> (ph -> ps) -> ph -> ch >>

    (wi (wi ph (wi ps ch)) (wi (wi ph ps) (wi ph ch)));

  axiom ax-3: << (~ph -> ~ps) -> ps -> ph >>

    (wi (wi (wn ph) (wn ps)) (wi ps ph));

  axiom ax-mp:

    << ph >> ph ->

    << ph ->