[SCL] Approach to a concrete syntax

[Chris Menzel]

On Tue, May 20, 2003 at 12:36:23PM +0100, Murray Altheim wrote:
> As I mentioned above, in reading over Chris' latest draft, I'd not
> approach XCL now in the same way. But what I would still advocate is
> not hardwiring the quantifiers, connectives, and predicates as fixed
> element types.  First, it creates more element types than is really
> necessary (complicating the language), but it also locks the language
> into that fixed set, which is unnecessary (and then when people want
> to extend the language you have two types of "verbs", those hardwired
> as elements in the core syntax and those somehow defined by others).

I am sympathetic to this in general, but am a little concerned about it
with respect to the logical apparatus; see below.

> So what I'd advocate now is to have the three types as distinct
> elements:
> 
>    <quantifier />
>    <connective />
>    <predicate />

Surely we need <variable /> or the like to do quantification properly.
Also need categories, or types of higher-level elements, for individual
constants and function symbols.

> and then have a typing subelement that provides its meaning, as in
> 
>    <quantifier>
>      <type>forall</type>
>    </quantifier>
> 
> and then in some web-enabled version of the language (if that's not
> already a feature in version 1), we add a reference element to allow
> people to link to PSIs for their own types:
> 
>    <quantifier>
>      <typeRef 
>      xlink:href="http://purl.org/cyc/1.0/constants/#thereExistsAtMost"/>
>    </quantifier>

I am concerned about this.  If we allow arbitrary typerefs to arbitrary
quantifiers and the like, what's to ensure that the referenced
entities comports with the SCL semantics?  What's to ensure that the
references quantifier is even coherent?  If SCL is supposed to function
as a *standard*, then it would seem that any referenced quantifier or
connective would itelf have to be validated in some way vis-a-vis SCL.
And how else would this be done other than to show how the referenced
piece of apparatus is definable in SCL?  But then why not use SCL
directly?  Part of the idea behind [s]cl is to provide a framework that
is expressive enough to avoid having to build a framework piecemeal.

This sort of external referencing is of course critical when it comes to 
nonlogical constants and predicates, of course, but I'm not at all sure
it is desirable or even feasible for the logical apparatus.  This seems
to me to undermine the whole point of a standard logical framework.

> In the XML notation, you could have either a <type> or a <typeRef> as the
> first child element of <quantifier>, <connective>, or <predicate>.
>
> In a nutshell, all I'd change in moving from abstract to concrete syntax
> (now that I understand you all better -- and I do agree, John), is to
> generalize the syntax as described above, opening it up so that extensions
> don't need to rely on ugly things like XML namespaces and the creation of
> new elements and attributes, where element and attribute *content* would
> do. I'm trying to avoid:
> 
>    <scl:formula xmlns:scl="http://purl.org/cl/scl/1.0/"
>           xmlns:cyc="http://www.cyc.com/cycdoc/vocab/">
>      <scl:forall>
>        <scl:var>x</scl:var>
>      </scl:forall>
>      <scl:formula>
>        <cyc:thereExistsAtMost>
>          <scl:var>x</scl:var>
>          ...
>        </cyc:thereExistsAtMost>
>      </scl:formula>
>    </scl:formula>
> 
> when it's *really* not necessary:
> 
>    <formula xmlns="http://purl.org/cl/scl/1.0/">
>      <quantifier>
>        <type>forall</type>
>        <var>x</var>
>      </quantifier>
>      <formula>
>        <quantifier>
>          <typeRef xlink:href="http://purl.org/cyc/1.0/#thereExistAtMost"/>
>          <var>x</var>
>          ...
>        </quantifier>
>      </formula>
>    </formula>

I certainly agree the latter is much more attractive.  There are
probably several proposals to kick around here, but the one I understand
best is whether we should introduce the higher-level elements Murray
suggests here, i.e., <quantifier>, <predcon>, etc.  I'd also like others
reactions to my concerns above about permitting typerefs to external
logical constants like quantifiers.

-chris