On Sun, Jun 5, 2022 at 8:19 AM Benoit <[email protected]> wrote:
> Forbidding that may be "aesthetically desirable" but it would probably be > too cumbersome for practical developments. I'm not sure I would call it desirable at all. It is very common for a string to simultaneously parse at multiple nonterminals of a CFG: you can't really do precedences without it. The whole idea is that the nonterminal to parse at is part of the input; requiring that every string parse to at most one nonterminal means you can't factor the grammar or do many other language-preserving transformations to the grammar because the identity of nonterminals is important. In MM0 the "coercion" notation command is explicitly intended to declare A -> B no-syntax functions analogous to "cv". > > On Sunday, June 5, 2022 at 1:45:40 PM UTC+2 [email protected] wrote: > >> The VTs don't have to be indistinguishable. They can actually be >> completely different, as long as they happen to have at least one common >> parsable string. Even set.mm has this situation: "class x" and "setvar >> x" are both grammatical. So for example if we added a new typecode like so: >> >> $c INHABITED $. >> ax-inh.1 $e |- x e. y $. >> ax-inh.2 $a INHABITED y $. >> >> then it would be ambiguous whether INHABITED is supposed to take a setvar >> or a class. >> >> On Sun, Jun 5, 2022 at 7:16 AM Benoit <[email protected]> wrote: >> >>> Yes, it's that kind of example, where you basically duplicate a VT, that >>> discouraged me from looking further at necessary and sufficient conditions >>> for being uniquely grammatical. It seems that such a condition would be >>> basically a reformulation, saying that there are no two indistinguishable >>> VTs (plus the equivalent of your variable-free "ax" to tie them up). So as >>> you seem to confirm, not much interest in looking further. >>> >>> I guess there is a divergence between the abstract study of systems and >>> the language design considerations (e.g., MM, MM0), for at least two >>> reasons: >>> * some declarations, even though redundant, may serve as "error >>> detecting codes", like $v and $c statements, or some $j statements; >>> * when studying the systems, it is generally convenient to ignore the >>> order of statements, whereas, if you want to minimize the number of >>> required passes, you should take it into consideration in language design; >>> plus probably performance considerations since e.g. determining unique >>> gramaticalness and the correct Syn may take time. >>> >>> Benoît >>> >>> >>> >>> On Sunday, June 5, 2022 at 4:19:13 AM UTC+2 [email protected] wrote: >>> >>>> On Sat, Jun 4, 2022 at 9:36 AM Benoit <[email protected]> wrote: >>>> >>>>> Mario: I had been wondering about something for a while: in Models for >>>>> Metamath, you define "weakly grammatical" as a property and "grammatical" >>>>> as an extra structure (the function Syn is part of the data). One could >>>>> define a system \Gamma to be *uniquely grammatical* if there exists a >>>>> unique Syn: TC \to VT such that (\Gamma, Syn) is grammatical. It is not >>>>> hard to see that set.mm-like systems are uniquely grammatical. In >>>>> general, >>>>> I haven't found non-trivial necessary or sufficient conditions to be >>>>> uniquely grammatical. Have you thought about these questions ? >>>>> >>>> >>>> Well, it's easy enough to determine which typecodes are syntax >>>> typecodes since they are the typecodes of variables, but I don't think it >>>> is very simple to figure out the mapping '|-' -> 'wff' for the logical >>>> typecodes. Especially if there are no axioms (yet) the problem is >>>> underdetermined. >>>> >>>> >>>>> It looks like if you know beforehand that a system is uniquely >>>>> grammatical, these $j commands are not necessary: upon reading the first >>>>> assertion with a non-VT typecode, say $a T expr $., the system tries to >>>>> prove $p S expr $= ? $. for all variable types S, and it will succeed for >>>>> a >>>>> unique one, which is then Syn(T). (This assumes that a typecode which >>>>> first appears in an assertion does not appear later in an $f-statement.) >>>>> >>>> >>>> More to the point, it is my opinion that these kinds of things "feel" >>>> like they should be declarations. This prevents syntax errors like using >>>> ')' as a typecode, because you know what the legal typecodes are, and it >>>> allows you to parse expressions without guessing the typecodes. >>>> >>>> In fact, the example where we truncate a grammatical database before >>>> the first axiom is actually true in general: It could be that ')' is a >>>> typecode of set.mm, and we simply have not introduced the first axiom >>>> using it. That is, the definition of "grammatical database" includes not >>>> just the data "Syn" but also "TC". (In the paper TC is inferred from the >>>> existence of axioms, but in the $j syntax approach TC is declared in >>>> advance of use, and I think this is the right approach as mentioned in the >>>> previous paragraph. In MM0 these are declared using the "sort" command.) >>>> >>>> Even if we take the paper definition of TC, there is another example of >>>> a grammatical database that is not uniquely grammatical: >>>> >>>> $c A B |- * $. $v a b $. >>>> va $f A a $. >>>> vb $f B b $. >>>> as $a A * $. >>>> bs $a B * $. >>>> ax $a |- * $. >>>> >>>> Here we have two variable typecodes A and B, and one logical typecode >>>> |-, and the question is: is Syn(|-) = A or Syn(|-) = B? It parses either >>>> way. This is actually an unambiguous formal system, because we require only >>>> that there are no two ways to derive the proof of the *same* syntax >>>> theorem, and "A *" and "B *" are different theorems. >>>> >>>> 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/4932d6bf-c373-42df-9301-1640a060768dn%40googlegroups.com >>> <https://groups.google.com/d/msgid/metamath/4932d6bf-c373-42df-9301-1640a060768dn%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- > 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/bdb5fc53-1629-427f-ba7c-667f8aa2b00an%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/bdb5fc53-1629-427f-ba7c-667f8aa2b00an%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSuezSAVsK7B_vZkkX7p77KR5Dq%3DP83j0Brv9%2BK2Utmewg%40mail.gmail.com.
