[SCL] Telecon and SCL progress
pat hayes
phayes at ai.uwf.edu
Tue Mar 4 15:03:45 CST 2003
Greetings, and sorry for the delay in getting started.
This email is an attempt to summarize the progress we think we made
at the Santa Fe ISO meeting a few weeks ago on the basic language,
and to outline the various things that need to be done. Hopefully we
can schedule a telecon for next week (this week I will be at the W3C
plenary meeting) to start discussing these.
TELECONS
Let us try to start having a telecon. We can schedule the second one
after we see how the first one goes. Early in the day US time seems
best for European members, so I suggest that we try for 0900 CT/1000
EST/1600GMT/1700 CET, on Monday 10 March. If anyone finds this
time/day impossibly inconvenient, please suggest another. The number
to call is (US) 413-351-4140. Please say your name when you arrive so
we can keep track of who is on the call. I expect the original
volunteers to phone in if possible, but others are welcome if they
feel they can contribute. The basic rule is that anyone I can talk to
is liable to be asked to actually do something.
PROGRESS
John Sowa has already summarized the positive reception of his
presentation to ISO, so we can assume that this represents progress
towards SCL or CL becoming an ISO effort. In the meantime, SCL will
move ahead.
Chis Menzel, John and myself had numerous discussions about the
possibilities for defining the basic language. We feel that the very
loose 'wild west' syntax described in the CL abstract syntax document
is too, er, relaxed for SCL, and that it is important to restrict it
to be more conventional, in order to make the initial step less
onerous for developers familiar with a conventional FOL syntax. On
the other hand there is widespread support for the syntax of SCL to
allow variables and terms in relation position and also to allow for
variadic relations. The latter is particularly bothersome, as it
seems to require that the language allow row (sequence) quantifiers.
Row quantifiers have been a continuing issue in the KIF/CL project
and have been much discussed and debated; and we had noted some time
ago that if allowed in an unrestricted fashion they take the language
beyond FO expressivity. On the other hand, the actual use cases have
always suggested that a certain pattern of 'inductive' definition is
the only really necessary case.
The progress we have made is to identify this case with some
precision, allowing us to design SCL syntax so as to allow the needed
use cases while avoiding the complexity of the wild west syntax .
This work is still being written up (by Chris) but in sum, it amounts
to the following:
1. Row variables occur only as free variables; there are no row
quantifiers. Free variables are treated as universal in the top-level
expression, as usual.
2. The model theory for the language is inherited directly from the
CL model theory.
3. There are two inference principles associated with row variables.
Expressed as natural deduction rules, these are
@E:
PHI[@x] |-- (forall (?x1,....,?xn) PHI[?x1,....,?xn]
ie any row may be replaced by a sequence of normal variables and
universally quantified at the top level (if we adopt a standard
convention for free conventional variables then the quantifier could
be omitted, of course.)
@I:
PHI[ ] and ( PHI[@x] implies (forall (?y) PHI[?y @x] ) ) |-- PHI[@x]
This second rule is not of course strictly an introduction rule since
it uses the row quantifier in the premis; but it is in a suitable
sense (which Chris is busy making explicit) equivalent to the 'real'
introduction rule @II:
@II
(PHI[ ] and PHI[?x1] and PHI[?x1, ?x2] and .... ) |-- PHI[@x]
which of course, being infinitary, takes the logic outside FOL and
yields a non-compact logic and is generally a nuisance, although
being semantically very transparent.
The systems formed by adding the rules {@E, @II} and {@E, @I}
respectively to a conventional ND proof system for FOL are in a sense
equivalent. The first has a very transparent semantics with very
obvious properties; the second is much more tractable and useful in
practice, and has a fairly satisfactory proof theory in which
expressions with row variables are treated as schema, and can be
instantiated directly to yield conventional FO expressions, but also
satisfy a general induction property expressed by the rule @I, which
allows inductive (recursive) definitions to be treated as defining a
schema. This seems to provide a clean semantic and proof-theoretic
version of a logic which closely resembles the original KIF, but now
has a clean and adequate semantics. This, therefore, is the version
of the logic which we propose to adopt as the basic version of SCL.
Notice that the rule @I fits naturally with the 'tail-position-only'
subcase which was used in KIF. Since allowing row variables in
arbitrary position introduces known intractable problems with
unification, it would be natural to impose this restriction in the
syntax, so I suggest that impose this restriction in the syntax also.
This makes SCL *very* similar to KIF, readers may note :-)
We will need to introduce a special logical predicate, by the way,
true of 'individuals', to be able to define the conventional FOL
syntax mapping (1.2 below).
THINGS TO DO
Some places which need work, apart from the basic write-up, model
theory (inherited from CL) and completeness proofs, are:
(a.) To what extent can this language be transcribed as a
conventional FO syntax applied to lists? In other words, if we
introduce sequences (lists) into the domain explicitly, what
additional list ontology is required to support a transliteration of
this SCL into a similar language without row variables, but instead a
conventional quantification over rows considered as entities? The
chief source of trouble here seems to be capturing in such a language
the idea of a sequence of quantifiers, as used in the instantiation
rule. The point being that instantiating a single conventional
variable with a list *of variables* does not seem to quite correspond
to the kind of operation specified by @E.
The reason why this question is relevant is that such explicit-list
translations are becoming almost standard in Web logics, eg, cf. the
technique used to translate OWL into RDF syntax. It seems that SCL
has here an opportunity to provide a useful foundation point for a
number of applications, therefore.
(b) Can the model theory be simplified if it is restricted to this subcase?
(c) To what extent does the induction rule @I allow for conventional
recursive function definitions? Are there any obvious significant
gaps in the expressive power of the language compared to, say, LISP ?
-----
MORE THINGS TO DO
1. IDENTIFYING SUBCASES
We should clearly identify, and provide names for, familiar subcases
of the language which are in wide use, and provide clearly written
analyses of their relationships to full SCL. The obvious ones which
occur to me offhand are:
1.1 strict first-order SCL (no free variables, so no row variables)
1.2 'conventional' FOL syntax (no row variables; all relations and
functions have fixed arity; only constant names in relation position)
(How is arity characterized in the syntax?)
1.3 Horn-clause form.
1.4 Syntactic cases corresponding to DL-style logics? To frame systems?
Any others? Nonmonotonic cases?
Issue: Do we want to allow for nonmonotonic constructions, and if so how?
2. SPECIAL DOMAINS.
To be practical, any ontology language has to allow for special
classes of identifiers which are restricted to various common
domains, even if those domains are not fully defineable in the
language itself. Examples include the integers, XML documents,
URIrefs, XML schema datatypes, etc.; and we should expect that this
list will be extended in the future. It would therefore be useful if
SCL could provide a general account of such special classes and a
general-purpose syntactic mechanism for incorporating them into the
language. It is quite acceptable to do this even though the domains
involved are not defineable or at any rate not in fact defined by SCL
ontologies.
We need to work out the details of this and provide a syntax. A first
prototype of this was done in the Lbase document
(http://www.w3.org/2002/06/lbase/20030116Snapshot.html), and this
experience suggested some basic points. First, the logic needs a
characteristic predicate for items in the special domain. Second, we
should try to characterize the essential properties of the domain and
clearly itemize those properties as relations. For example, it makes
sense to have a less-than ordering associated with the integers, but
perhaps assuming addition might be going too far. Does anyone have
any principled intuitions about what might acceptable here? Can we do
better than simply deal with these case-by-case?
Issue: how does the recursive nature of many of these domains relate
to the row-induction rule @I ?
3. SORTING AND RESTRICTED QUANTIFIER SYNTAX
Lets agree that doing sorting properly is likely to to be too
ambitious. Nevertheless, it might be worthwhile to define a
restricted-quantification syntax, since we will need to use this in
discussing 1.2., and it is widely considered useful. We need to make
this precise, however. Eg, is it useful to have any restrictions on
the forms of the restriction? (To predicates representing 'types',
say? To predicates which can be defined using a restricted subcase of
the language??)
4. CONCRETE SYNTAXES
XML, CGs, KIF-style, Principia-style are all pretty obvious. Others
might include a syntactic mapping from SCL into RDF syntax, which I
will have a try at describing, and maybe a Z-style concrete syntax
(??)
I would like volunteers to take charge of drafting each particular
concrete syntax proposal. As a preliminary suggestion:
XML: Tanel Tammet
CG's: John Sowa
KIF-style: Pat Hayes
Principia-style: Chris Menzel ?
RDF triples: Pat Hayes
Z: John Sowa ?
5. ANNOTATIONS AND COMMENTS SYNTAX
Several people have suggested the idea that the syntax should provide
for text to be associated with subexpressions which has no logical
content. We need to decide on a way to do this. I would suggest that
we do this by allowing in the abstract syntax a 'wrapper'
construction, where a wrapper is a form with two parts, a text string
and body which is an expression of any syntactic form, and the
syntactic class of any wrapper is the same as that of its body. We
can then provide a distinctive concrete syntax for wrappers (eg
square brackets in a KIF-style syntax, or a particular XML tag in an
XML syntax) which would allow us to insert text at any point in any
expression. This allows wrappers to be nested.
Issue: is it sufficient to only add text? Eg in RDF, comments may be
arbitrary expressions and may share variables with other expressions.
6. RELATIONS BETWEEN ONTOLOGIES
Practical ontology engineering seems to be getting similar to
software engineering, in that large-scale ontologies go through large
numbers of revisions, are constructed by combining parts of other
ontologies and so on. Several practical languages include special
syntax for keeping track of this kind of information. Particular
examples include (where 'item' is a definition or axiom or term)
this ontology imports material from that ontology
this ontology (item) is a revised version of that ontology (item)
this ontology was written by ... on date .... with number/id .....
this item is deprecated in favor of this other item....
This kind of information can be informally incorporated into text in
wrapped comments, but it might be worth spending some time to try to
identify common patterns and provide them as part of the syntax, or
maybe as part of a special ontology (?)
Issue: this requires a systematic way to refer to ontologies. Do we
need a syntax for naming ontologies?
(Comment. Moving in W3C circles has brought home to me very forcibly
the need to make distinctions between ontologies, documents, strings
of characters, files, etc etc., all of which distinctions are
invisible from the point of view of traditional logical syntax. Just
a heads-up to the members of the group to whom this issue seems
trivial... :-)
7. OTHER
Im sure there are some points I have missed or not discussed, so
please anyone who has any other issues to raise, send email.
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 ai.uwf.edu http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu for spam
More information about the Scl
mailing list