I hope parts of this discussion will make their way into some kind of documentation, in particular the possibility to add extra parentheses 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.
> 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). > > >> 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. Benoît -- 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/e6c1824a-5d6d-4584-bf62-65ef8c0dedb1%40googlegroups.com.
