I hadn't thought of this, that's interesting. This is possible because of cv $a class x $. which permits a kind of overloading of any predicate on classes. This permits that setvar and class share "common parsable strings", as you write. Forbidding that may be "aesthetically desirable" but it would probably be too cumbersome for practical developments.
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.
