[SCL] Re: SCL syntax

[Pat Hayes]

>I feel strongly that in the kernel (which you write should be "just 
>sufficient" and "minimal")
>quantifier vectors should be excluded  Excluding quantifier vectors from the
>kernel and specifying the translation helps deal with the issue of 
>the meaning of
>a quantifier vector with multiple occurrences of a variable name and also
>the case of the empty variable list.

True.

OK, if you feel strongly about it I can make the kernel be really 
minimal. It was that way once, but when I wrote the MT there didnt 
seem to be any reason to restrict it so far. I'll put the changes 
back in and extend the translation table.

>You could deal with this in the semantics, but isn't it
>easier to restrict the kernel so that only the single variable case 
>need be handled
>in the semantics?

Not really. You just talk there about variable mappings, and a 
mapping applies to a vector just as well as to a singleton. But I 
take your general point.

>  Also, many pedantic and rigid GOFOL
>presentations require a quantifier symbol for each variable, so the 
>restriction is suitable for
>a kernel.  And even if your only purpose in the K[] mapping was to 
>eliminate restricted
>quantifiers, it is true that the target of the translation happens 
>to use only single variable
>quantifications, so the restriction is a natural one, and the work 
>is already done.
>
>Generally, I just think that (forall (x1 ... xn) s) is not 
>sufficiently primitive to be in what is
>called a (minimal) kernel.  I feel the same way about Common Lisp: I 
>think it's a mistake
>that let and let*, as complex as they are, are primitives instead of 
>being translated to
>simpler single-variable binding operations.
>
>"x1...xn" was such a pretty sequence variable name.  Sigh.

But people will read that first substring like a real identifier, 
seems likely to me. Consider the potential confusions between
(R x0...xn)
and
(R x1...xn)
and
(R x0 x1...xn)

You can still have  "...x1...xn"  and "...xi..." and "...xi...xn" and 
"...xn" :-)

Pat

>
>Mark
>
>Pat Hayes wrote:
>
>>>In SCL Kernel synax, replace
>>>quantsent = open 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scopen>, 
>>>'forall' , open 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scopen>, 
>>>{ name 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scname> 
>>>} , close 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scclose>, 
>>>sentence 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scksentence> 
>>>, close 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scclose> 
>>>; compare core quantsent 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scquantsent>
>>>by
>>
>>>quantsent = open 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scopen>, 
>>>'forall' , open 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scopen>,  
>>>name 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scname> 
>>>, close 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scclose>, 
>>>sentence 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scksentence> 
>>>, close 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scclose> 
>>>; compare core quantsent 
>>><http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html#scquantsent>
>>
>>
>>I think it is fine to have quantifier vectors in the kernel. It 
>>doesnt complicate the model theory. The K[ ] mapping for Uquants is 
>>designed to get rid of the restricted quantifiers.
>>
>>>Did you note my suggestion that seqvar be defined by
>>>   seqvar = {char}, "...", {char};
>>
>>
>>Whoops, no, I missed that. However...
>>
>>>I think this is even better than my initial suggestion of
>>>   seqvar = "...", {char};
>>>which you adopted, since it allows seqvars like "x1...xn".
>>
>>>What do you think?
>>
>>
>>... it is cute, but I don't think that is a good idea as it seems 
>>to give a seqvar two 'names', and also it might overconstrain what 
>>can be allowed to be a name. There might be URIs out there with 
>>three dots in them, and I want URIs to be legal names as far as 
>>possible.
>>
>>Pat
>>
>>>
>>>Mark
>>>
>>>Pat Hayes wrote:
>>>
>>>>>I didn't notice any real problems with "Core expression syntax".
>>>>>
>>>>>I suggest renaming the "atom" nonterminal to "atomsent".
>>>>
>>>>
>>>>Done in the BNF.  I will need to scour the text to make this 
>>>>change complete.
>>>>
>>>>>The very
>>>>>first time I read the document, I briefly thought "atom" 
>>>>>referred to Lisp-like
>>>>>atoms rather than atomic formulas.  I know better now, but 
>>>>>renaming it would
>>>>>eliminate the slight possibility of confusion.
>>>>>
>>>>>The "scl:comment" reserved word is a slight misnomer, since, for example,
>>>>>(scl:comment "Axiom 1" (= (* x 0) 0))) is not a comment that can be
>>>>>ignored, but rather a sentence with a comment attached.  It 
>>>>>would be more precise
>>>>>to have a "scl:commented-form" or some such reserved word and write
>>>>>(scl:commented-form "Axiom 1" (= (* x 0) 0))).
>>>>
>>>>
>>>>Or follow the RDF/OWL tradition and have 'scl:about'. Nah.....
>>>>
>>>>>However, this is
>>>>>more verbose and adds another reserved word instead of overloading
>>>>>the "scl:comment" reserved word used in phrases, so you may prefer
>>>>>to leave things as they are.
>>>>
>>>>
>>>>Yes, leave it alone.  I don't think that this will cause any 
>>>>problems in practice.
>>>>
>>>>>In the SCL Kernel, I don't see why commented forms are in the kernel.
>>>>>You could omit them from the kernel and give their translation
>>>>>K[(scl:comment str s)] -> K[s]
>>>>
>>>>
>>>>Good point. Done.
>>>>
>>>>>
>>>>>In the SCL Kernel translation table, you should add
>>>>>K[(forall () s)] -> K[s]
>>>>
>>>>
>>>>done
>>>>
>>>>>
>>>>>In the SCL Kernel translation table, you should replace
>>>>>(forall (x) (implies (t x) K[(forall (...) s)])) by
>>>>>(forall (x) K[(implies (t x) (forall (...) s))])
>>>>
>>>>
>>>>Ive changed it to
>>>>
>>>>(forall (x) (not (and (t x) K[(forall (...) s) ] )))
>>>>
>>>>>
>>>>>In the SCL Kernel translation table, do you want the translation
>>>>>of roleset elements to be translated as (ni ti x) or as (= (ni x) ti)?
>>>>
>>>>
>>>>Whoops. The latter, right. Done.
>>>>
>>>>>
>>>>>Later on in the "Sequence variables, recursion and argument 
>>>>>lists" section,
>>>>>you should replace
>>>>>(iff (= x (list)) (= (cons z x) (list z))) by
>>>>>(forall (x z) (iff (= x (list)) (= (cons z x) (list z)))).
>>>>
>>>>
>>>>Whoops again. Done.
>>>>
>>>>Ive also made the lexical changes you suggested, which simplifies 
>>>>things quite a lot . I just LOVE the ... syntax for seqvars.
>>>
>>>>
>>>>Thanks for your help.
>>>>
>>>>Pat
>>>
>>
>>
>>--
>>
>>---------------------------------------------------------------------
>>IHMC       (850)434 8903 or (650)494 3973   home
>>40 South Alcaniz St.       (850)202 4416   office
>>Pensacola                 (850)202 4440   fax
>>FL 32501                     (850)291 0667    cell
>>phayes at ihmc.us       http://www.ihmc.us/users/phayes


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes