0
$\begingroup$

In this introduction to Metamath, the author suggests that the $c and $v statements can be viewed as encoding the terminals and non-terminals of a grammar. In this discussion from the Metamath authors, such grammars are examined for ambiguity.

Along similar lines, suppose that we choose a context-free grammar. Is it theoretically possible to generate a pile of $c and $v statements which encode the grammar? Is it possible if the full range of Metamath statements are allowed?

Improve this question
$\endgroup$
9
  • $\begingroup$ For what it's worth, I am expecting the answer to be "Surprisingly, no!" but don't yet have any evidence or counterexamples which lead in that direction. Also FWIW this came from the conlang community; many conlangs have CFGs and have community members interested in formalization. $\endgroup$
    – Corbin
    Commented Jul 9, 2023 at 19:37
  • 1
    $\begingroup$ What do you want to do with the grammar, once it's formalized in Metamath? Context-free grammars can generally be formalized as inductive types in proof assistants. $\endgroup$
    – Andrej Bauer
    Commented Jul 9, 2023 at 20:02
  • 1
    $\begingroup$ And what does "automatically" formalized mean? It looks to me like you could just delete the word "automatically". $\endgroup$
    – Andrej Bauer
    Commented Jul 9, 2023 at 20:04
  • $\begingroup$ @AndrejBauer: By "automatic" I mean something that could be codified as a program: insert grammar, get MM database. (Again, I was expecting a negative answer; I wasn't trying to ask about how to write such a program.) For me personally, I'm formalizing Lojban, and so after the grammar I will be formalizing Lojban's logic. $\endgroup$
    – Corbin
    Commented Jul 9, 2023 at 21:41
  • 1
    $\begingroup$ Just like was done for Douglas Hofstadter's MUI system, you should be able to encode all rules of Lojban into a Metamath file, and then write verifiable proofs that sentences are actual derivable Lojban sentences. I don't know of any tool which would, say, take a BNF for Lojban and output a valid Metamath file, though, so you'd have to write that manually. In a second step, you might also add e.g. first order logic axioms in Lojban and write proofs for logic statements in Lojban, which proof can be verified by Metamath. $\endgroup$
    – Thierry Arnoux
    Commented Jul 11, 2023 at 10:04

1 Answer 1

Reset to default
1
$\begingroup$

Yes, there are no apparent obstacles. The two nuances are typecodes and ambiguous constructions, as detailed in the second link in the question.

That said, it probably isn't a good idea to directly translate a context-free grammar to Metamath rules. In practice, grammars often encode precedence rules, unroll recursion into parser-friendly forms, make choices to avoid ambiguity, and include extraneous rules for features like comments. Instead, it may be useful to craft a simplified grammar specifically for use with Metamath.

Also, while the context-free grammar might be unambiguous for left-to-right parsing, it might be ambiguous for unification. As a result, you may need to produce several $p lemmas which serve as hints to Metamath about which sorts of syntax are allowed. This is important for producing quick proofs with improve all.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.