On Thu, Nov 14, 2019 at 11:31 AM Benoit <[email protected]> wrote:
> I hope parts of this discussion will make their way into some kind of > documentation, in particular the possibility to add extra parentheses > This should be in mm0.md, in the grammar if nowhere else. This might be surprising to a metamath user, but it's basically a universal convention in other computer languages. > and the fact that MM0 uses the term "sort" instead of "type" because the > type system is voluntarily poor, and if some type theory is to be > implemented, this has to be within the logic, and not the metalogic. > Hopefully the examples will make this clear, eventually. I mean putting a coercion later in the file. It could be forbidden, but >> then this entails making precise the rules that dictate the acceptability >> of the added coercion (and an efficient decision procedure for the >> criterion). There is already a similar kind of restriction on coercions: >> the coercion graph is required to have no diamonds (more than one path >> between any two fixed vertices), and this is checked using a dynamic >> version of the Floyd-Warshall algorithm. >> > > Maybe this type of "delayed coercions" could be forbidden, but I cannot > tell whether it is worth it (nor could I tell the precise rules and > decision procedure). > Actually, this really doesn't work with the inference thing. It is reasonable to have a rule "you cannot simultaneously have X and Y" where you get an error on whichever of X or Y comes later, but if X is the result of inference then we generally want to not flag an error (because we wrote only Y, while X was inferred based on incomplete information at an earlier point), but rather we should backtrack and infer not-X based on the new information Y. This sort of thing works decently well for type inference a la Haskell, but it's a very non-local process, meaning error messages can be pretty bad, plus backtracking kills single pass analysis. Also inferring associativity plus backtracking means that a change later in the file can change the parse of an earlier statement. Very bad. > The MM0 parser specification is not deterministic >>>> >>> >>> Would it be possible (and worth it in terms of pros and cons) to make it >>> deterministic ? >>> >> >> Perhaps this is the wrong way to say it. The parser itself is >> deterministic, because the CFG is unambiguous. There is only one parse >> according to the CFG, so any valid parse algorithm will get the same result. >> > > This is what I understood. I was referring to making the CFG > deterministic, in the sense of deterministic CFGs as a proper subset of > unambiguous CFGs, which allow for simpler parsing ( > https://en.wikipedia.org/wiki/Deterministic_context-free_grammar). But > again, I don't know much in this domain. > It is a DCFG. Just about any CFG that is "unambiguous by construction" will be a DCFG. The DCFG recognizer is probably pretty big, though, without some more optimizations, because you need a nonterminal for every precedence level, while a parsing algorithm can just use integers for this purpose without a lot of repetition. Mario -- 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/CAFXXJSuo01mDMowFhwgTwgy6o4Grp%3DLzxShyVvHcEK1FOCzZ0Q%40mail.gmail.com.
