Coming back to your example from set.mm where you introduce
${ $e |- x e. y $. $a INHAB y $. $}
one could argue that this is bad practice and that one should have
introduced instead
${ $e |- x e. A $. $a INHAB A $. $}
which is the "correct" level of generality. With that new axiom, the
system remains uniquely grammatical. What I'm trying to do is find a
criterion that would make more precise the fact that "reasonable", or
"currently encountered" databases are uniquely grammatical. Or one could
require that the types under coercions form a set of rooted trees, so that
if there are no "partially duplicate" types (as in the example above with
$a A * $. etc), then, even if the system is grammatical but not uniquely
grammatical, there is a "most stringent" Syn function making it grammatical
(in the example above with INHAB, this means taking Syn(INHAB)=setvar).
I have not practiced CFGs much, so I'll have to think a bit more about your
latest remark.
Finally: I'll be attending on Zoom next Monday (what a committee!).
Benoît
On Sunday, June 5, 2022 at 2:35:01 PM UTC+2 [email protected] wrote:
> 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/69c0846f-444e-4562-869a-d82b44c66808n%40googlegroups.com.
