[SCL] Proposed additions to the SCL draft standard
John F. Sowa
sowa at bestweb.net
Sun May 25 13:09:15 CDT 2003
Folks,
Tanel's suggested additions to the SCL draft standard are also
on the list of features that are needed to support conceptual
graphs. It's fine to have a minimalistic "core" semantics,
but the standard should also include some commonly used
extensions to the core. If they're not included in the
standard, every language that needs them will have to
implement them independently (and probably incompatibly).
Some comments relevant to CGs:
1. Integers are essential for the overwhelming majority of
practical applications, and some means of accommodating
them must be provided. There is, however, a question of
whether the standard should support full integer arithmetic
as defined by Peano's axioms or whether it should allow
for some limited subset.
I believe that full arithmetic must be available, along
the lines of the Z standard, which includes a library of
theories for integers, sets, and sequences. I recommend
adopting at least the Z library as an option, but we might
also have a more limited subset in the core that would be
sufficient to define quantifiers such as "exactly N" or
"at least N but no more than M". People have been using
such notations in CG extensions for a long time, but we
have to standardize them.
2. Comments (including "structured annotations") are essential
for most practical applications. We have defined a version
of comments for CGs, but there are still some issues about
how fine-grained the commenting should be -- i.e., whether
comments at the level of complete formulas are sufficient
or whether comments can be attached to smaller syntactic
units. In CGs, for example, the box and circle notation
makes it convenient to add comments to smaller units.
But it would be best if some level of comments could be
associated with categories in the abstract syntax so that
they could be preserved in cross-language translations.
3. The free-form SCL syntax, which allows quantifiers to
range over any kind of entities (individuals or predicates
indiscriminately), allows assertions that are unusual and
certainly unexpected for people who use other versions of
logic (including both conceptual graphs and traditional
predicate calculus).
To accommodate traditional predicate calculus as well as
languages with various type conventions (including CGs and Z)
the standard should include the definition of restricted
quantification as an option. I don't believe that we have
to support the strict typing of Z, since that could be
interpreted as restricted quantification with additional
syntactic constraints -- i.e., any true statement in Z would
have an equivalent true statement in CGs and vice-versa, but
some false statements in CGs would be syntactically illegal
in Z.
For the benefit of those who are not on the SCL mailing list,
Tanel's complete note is copied below.
John Sowa
_______________________________________________________________
Tanel Tammet wrote:
> Before additional work on the XML concrete syntax I thought
> that it would be more important to put some new features
> into SCL proper. These "new" features have been discussed
> a lot on the SCL list, but they are not present in Chris's
> minimalistic SCL draft.
>
> If we do not have these features in SCL proper (the
> abstract syntax and semantics), it would not be suitable
> to put them into the XML concrete syntax: the latter
> has to reflect the SCL abstract syntax, not extend it.
>
> I took Chris Menzel's SCL draft from
> http://cl.tamu.edu/docs/scl-latest.html at 24 May
> and added a number of PROPOSED modifications directly
> to it.
>
> Attached please find the modified SCL draft, as
> a zip file (sent a message with unzipped html before,
> but this was too big for the list program).
>
> The additions introduced are proposals. I have colored
> the background of all the additions green, so that it
> would be easier to follow (tested the Amaya editor
> while writing the additions).
>
> Please have a look at the additions and decide whether
> some of them or all of them are in principle worth
> keeping. Once the list of OK additions is decided,
> further modifications to the presentation would
> be suitable.
>
> Found a few parts of the SCL draft which contained
> errors or were in obvious need for further details.
> More about this after the list of proposed additions.
>
> The following is a list of the additions in the
> SCL draft html file along with motivations:
>
> - SCL standard is split into four levels or layers.
>
> Motivation: it is easier to implement a smaller standard
> than a larger standard. Fancier parts of SCL might
> be hard to implement/understand for users. It would
> be good to indicate that even partial implementations
> may correspond to an identified subset of a standard,
> if done properly. Othwerwise we stand the serious risk of
> partial implementations claiming to be SCL, while
> nobody really knows which parts are implemented and which
> not (or we stand the risk that very few people take up courage
> to implement and use SCL at all).
>
> - Annotations (might be called also comments or documentation
> strings). Free text (strings) may be attached to terms
> and formulas.
>
> Motivations:
> - Obvious need for documentation. Most probably will
> be implemented in concrete syntaxes. Hence it would be
> good to define in the abstract syntax, so that different
> concrete syntaxes would be intertranslatable.
> - Possibility to encode additional (nonlogical) information
> for specialised systems in annotation strings.
> For example, in the automated
> theorem proving (ATP) context it is really crucial to identify
> that some parts of the formula stem from general axioms
> while some parts stem from a specification of a system
> explored while yet others stem from a query asked.
> This is absolutely unavoidable for practical ATP needs.
> And we DO NOT want to go into serius metalogic in the SCL
> context in order to attack this everyday necessity.
>
> - Integers and bounded existential quantifications (a possibility
> to say that there exist exactly N objects with some property P).
> By 'integers' I mean the use of numerals with a predefined
> property that all lexically different numerals map to
> different elements of the domain. Ie, not(id(4,7)) holds,
> no need for a user to define this.
>
> I have NOT defined the semantics of integer-bounded
> existential quantifier in the text, since the predicate-bounded
> existential quantifier was not defined either (see later in
> the 'omissions' section).
>
> Motivations:
> - OWL Full contains bounded existential quantification.
> While this can be encoded in plain FOL (or SCL), it is
> pretty cumbersome. Would be more convenient to use integers
> in the language.
> Once we do allow to use bounded existential quantification,
> it would be a bit weird not to allow integers in general.
> - Integers and integer arithmetic is, not surprisingly, very
> important in many practical ATP fields, like verification.
> Essentially, you have to build in integers and arithmetic
> for doing practical verification of hardware (electronics,
> railroads, etc). You have to build in integers for creating
> e-commerce system rules, etc (think prices, quantities of goods,
> etc).
> - Integers are not just syntactic sugar. It is not enough to
> decide that, say, let us use 0 to denote 0, s(0) to denote
> 1, s(s(0)) to denote 2, etc.
> The crucial issue is that you need to define that 1 is not equal
> to 2, 3 is not equal to 7, etc for all pairs of integers.
> As we know, this CANNOT BE DONE IN FOL. This can be done
> only using induction. However, it is easy to PREDEFINE that
> different numerals map to different integers in the domain,
> essentially building in the infinite list of disequalities
> (similar to the equality predicate, which also cannot be defined
> in pure FOL).
> - Once we have integers in the language, we could in principle
> (if we want to) encode strings and string equalities as
> integers (for example, by using ascii or utf) along with
> the ascii or utf string type constuctor taking an integer as
> an argument. Strictly speaking we would not need to extend
> the core language to encode strings (or any other datatypes,
> for that matter: integers suffice, at least theoretically).
>
> Small errors and omissions found:
>
> - In the early part of text the name of the identity function
> used was Ind, not Id as later.
> - The semantics of quantifiers bounded by predicates was IMHO
> not defined. This needs to be done. Once it is defined, the
> definition can be extended to the existential quantifier bound by an
> integer (not done in the proposed additions).
> - XML DTD was IMHO not complete: again, the possibility for
> bounded quantifiers was not there in the DTD. Hence I have not
> put in the integer-bounded quantifier into the DTD either.
>
> Some serious extension possibilities worth considering (not introduced
> as proposals in the attached text):
>
> - Identity (equality) on the object level.
>
> Chris mentioned that once we encode predicates using the App/Pred
> functions, the formula (forall x. P(x) & -Q(x)) & (forall x,y. x=y) is
> NOT valid, while it IS valid in the standard, non-app/pred semantics
> of FOL.
>
> This means that it is very hard to use SCL for encoding
> standard logical problems, including a large part of the
> thousands of problems in TPTP, used extensively in the
> ATP community. People cannot use Id in these contexts:
> they'd have to define their own equality not present
> in SCL and not axiomatisable in pure SCL alone.
>
> This might be survivable, but is really
> unpleasant, since it unnecessarily limits
> or confuses our audience.
>
> We could use the App/Pred-based SCL for standard FOL problems
> IF:
> - we explicitly identify a "simple" subclass of SCL where any first
> arguments of App and Pred are constants. This subclass
> can be trivially mapped to non-App/Pred, classical
> semantics (just drop the App and Pred and lift the first
> argument to the function/predicate symbol position: validity
> of formulas is not changed by this transformation).
>
> The "simple" subclass can be extended, of course, allowing
> cases where a variable is used in the first argument: the
> mapping will be harder, though.
>
> - We do provide an equality predicate on the individual
> constants only: ie, not usable on predicate/function name
> constants.
>
> Observe that the current Id predicate is NOT such an
> individual-constants only predicate.
>
> Also, the current
> SCL does explicitly differentiate between object constants
> and function/predicate constants, simplifying the introduction
> of the second equality predicate.
>
> Hence I suggest to:
> - write a chapter identifying the "simple" subclass of SCL
> and properties of its semantics,
> - introduce the second equality predicate, different from
> Id, defined only on the object constants.
>
> - Including other text.
>
> Both in the semantic web context and "ordinary" ATP it is
> important to import other files or parts of other files into
> the formula.
>
> If we want to put this into SCL (and why shouldn't we?) we
> do need an "include" operation. Include should IMHO take an
> URI as an argument and return the text at the URI. In case
> namespaces or any external links are used in the text referred
> by our URI, these namespaces and/or links should be resolved
> before including the text (a simple recursive process).
>
> If we do NOT put "include" into SCL, then inevitably people using
> SCL would have to construct their own inclusion constructions,
> different for different concrete syntaxes and users.
>
> Observe that the XML concrete syntax would not automatically
> introduce the linking possibility. Pure XML provides us with
> namespaces, but does not provide including text. We could
> try to use additional XML-based languages like XLINK, but
> these are highly complex. IMHO it would be better to put
> text inclusion into SCL directly, as an additional layer.
>
> Regards,
> Tanel Tammet
More information about the Scl
mailing list