[SCL] Headers and bodies

[pat hayes]

I think we are not stuck, exactly, but we are flailing. Could I ask 
you two prolific gentlemen to please stop working so hard on two 
divergent documents for the moment, and let us re-convene as a group 
to agree on our focus and try to forge a single purpose. I know you 
have both done a lot of work, but I feel that we really need to make 
sure that we are on convergent, or at least parallel, tracks.

Let me try to summarize some of the main issues that we have and try 
to suggest a way to compromise and simplify so as to find a single 
goal we can agree on. Before starting, let me mention and put aside 
issues to do with style of presentation (Greek letters, etc); those 
aren't the main issue here. I think however that there are some real 
issues that are kind of buried in there among the Greek, and will try 
to tease them out.

First, our primary goal should be to define a single language. We can 
*present* it in a 'core+modules' way purely for exposition, but it 
should *be*  a single coherent system with a single model theory. 
Somewhere in the spec, there should be a single, ideally quite 
compact, statement of what SCL as a whole) *is*, one that a developer 
can take and run with.
Second, it should be possible (and we should explain how) to 
implement a conforming SCL reasoner largely by translating SCL into a 
FOL theory in a certain way, and then applying traditional FOL 
reasoners to it. But this translation need not be central or 
particularly simple (though it would be nice if it were not 
hopelessly inefficient).
Third, we can identify subcases of SCL that have useful properties, 
including 'traditional FOL'; so that traditional FOL is indeed a 
sublanguage of SCL.
Fourth, all of the above exposition - of SCL syntax, model theory and 
translation into FOL - can be stated in terms of an abstract syntax, 
and hence projected into any conforming concrete syntax.

We had a fairly nice picture of all of this reasonably clear at the 
beginning of the year, but it seems to have got a lot more 
complicated since. The reasons for this complexity seem to be due to 
the need to keep a sharp separation between syntactic distinctions 
(particularly lexical ones) and semantic issues. Chris' style of 
language description treats these as completely distinct: a language 
is defined by its syntax, and a model theory is attached to the 
syntax: and 'syntax' here includes a lexical classification of the 
primitive lexical terms. This distinction is wired into Chris' way of 
describing abstract syntax by starting with a lexicon and building up 
from there.  This means that matters like the arity of a relation are 
part of the basic syntactic structure of the particular SCL language, 
and hence must be taken account of throughout the subsequent 
metatheoretic development; hence much of the complexity, I suggest. 
And hence also the fact that 'an SCL language' must as it were come 
clean on what its syntactic/lexical assumptions are; whereas, in 
contrast, Tanel and I both think of SCL (and FOL) as a *single* 
language, rather than a family of languages. We think in terms of 
expressions arriving which need to be parsed, and ask how they can be 
parsed. (Hence the confusion over Tanel's example where different 
sentences were predicated on different lexical presuppositions.) So, 
for example, it would be fine to have 'arity' as a special SCL 
function in the latter perspective: arity(R)=3 & R(a,b) is simply 
internally inconsistent, on this view, rather than syntactically 
illegal.

I think that the basic MT that we have worked out is right. It works, 
it has been stable now for quite a while, and we understand it fully. 
When we started, SCL was pretty damn simple: all names (except 
functions) were the same syntactic category and we didnt need 
anything like the complexity that we are now saddled with. Looking 
back, it seems to be that all of our problems have been to do, one 
way or another, with syntax. So I will start by trying to eliminate 
all this syntactic complexity, and approach the entire matter as one 
of axiomatizing the various restrictions within a single, general 
language.

------

First, define basic SCL as the language which has a single category 
of names, and the MT is defined so that terms which occur in a 
relation position must denote relations, and in object position must 
denote something in the universe of discourse (and function symbols 
denote functions, of course), and no other constraints. Call this 
'basic SCL' and 'an SCL interpretation'or just 'an interpretation' of 
a set of SCL sentences. There are no fixed arities or any such other 
complexities in basic SCL; those are handled by the use of headers.

A. Every SCL document/ontology (we need a better word; I'll use 
'document' for now) consists of a header plus a body, written <H,B>, 
both of which are themselves documents. The body is (a set of) SCL 
(sentences), and the header must supply enough syntactic information 
to enable a generic SCL parser to parse the SCL in the body.  'Parse' 
here includes allocating relation symbols and individual symbols to 
the appropriate category if that is required by the particular 
language. An interpretation of an SCL document is an interpretation 
of the body which satisfies the constraints described by the header.

B. Headers may cite one or more 'standard' headers of some kind (via 
a URL), or they may be local to the document. If a document is split 
into parts, each must have an appropriate header attached to it.

C. Headers may be empty, written < ,B>, or simply B, in which case 
the body is understood to be basic SCL; and they may include or cite 
other headers. The body must satisfy all the constraints in all the 
cited headers.

D. (more controversial) Headers may themselves be SCL documents. 
These are called SCL headers. (In all the following examples, the 
header of the header is assumed to be empty.)

E. If H is an SCL header then we interpret the SCL in the header in a 
particular way. Specifically, an interpretation I of <H,B> is 
*appropriate* for H, i.e. it satisfies the constraints described by 
the header, just when it can be extended to a superinterpretation 
(terminology??) which satisfies H; it *satisfies* the document when 
it is appropriate for H and satisfies B.  (A superinterpretation of I 
is an interpretation J whose universe is a superset of I and such 
that the restriction of ext-J to I is ext-I., ie so that I and J are 
identical on the universe of I. Intuitively, J is like I except that 
it might have some more 'stuff' in its universe.)

The reason for the superinterpretation condition is that H might 
quantify over things that are not individuals as far as B is 
concerned: in particular, it might need to assert that a relation is 
not an individual, which of course requires that the relation be in 
the universe of any satisfying interpretation of H but that it not be 
in the universe of B.  The narrow definition of superinterpretation 
ensures that anything that H says about relationships between 
entities in I will still be true in I, even if they are not Note that 
if I satisfies <H,B> then some superinterpretation of I satisfies 
H&B, I satisfies < ,B> iff it satisfies B, and satisfies <H, H&B> iff 
it satisfies < ,H&B>. Also if H entails H' and B entails B' then 
<H,B> entails <H', B'>.

Interpretations that can't be extended to satisfy H are 
*syntactically* inappropriate: they violate conditions that are 
thought of as syntactic conditions of the document rather than 
propositions asserted by the document. Conforming SCL inference 
engines should report inconsistencies arising from SCL inference 
applied to headers as syntax errors.

Obviously this would allow arbitrarily complex conditions to be 
labelled as 'syntactic', so we will only impose conformance on a 
narrowly defined subset of all possible SCL headers; but the idea is 
general-purpose.

Sentences can be  moved from header to body or body to header, but 
this is liable to change the satisfaction conditions: in particular, 
moving from the header to the body is liable to increase the size if 
the universe in any satisfying interpretation. More on this below.

It would be possible to always write the SCL header information as 
part of the body, and always have an empty header. This option 
effectively ignores the header and treats all assertions as part of 
the ontology, so that a document can be treated simply as a set of 
SCL sentences. It has the merit of simplicity but does not allow one 
to impose syntactic restrictions on a vocabulary, in case one wishes 
to do so. It does however provide a 'universal' case such that any 
SCL document with an SCL header can be described in a single 
framework, at some possible cost of expressivity and efficiency.

Another option might be to treat the SCL header as equivalent to a 
'T-box' and the body as an 'A-box'. I havnt gone into his idea in any 
detail, however.

Note that this allows entailment relations to hold between documents 
with different SCL headers. In particular,  < ,H&B> entails <H,B>. 
There should be a conformance level which is lower than this and is 
restricted to a particular class of headers, however.

F.  A particular SCL vocabulary is provided, called the header 
vocabulary (see below); applications must be able to appropriately 
process SCL headers written using the syntax vocabulary.

Obviously it would be possible to allow headers to be countably 
infinite, by the way, provided that in practice this could be 
captured in some effectively computable way from a finite 
description. In particular, it can contain all instances of some 
general schema. We could even regard the numerals as being so 
described by a standard header, for example, and provide this as one 
of the 'standard' headers.

-----

OK, before you all jump on me, read on to see how this works. I will 
use a conventional syntax for illustrative purposes.

Syntax: like the old CL, but with functions marked. That is, there 
are names (constants) and variables and (free) seqvariables; terms, 
atoms and sentences are built up in the usual SCL way.  Also, 
however, numerals are a distinguished class of names with a fixed 
interpretation in *all* SCL languages, and so are quoted strings (why 
not? Its obviously useful and semantically and syntactically trivial, 
and if you don't use numerals or quotes then they do not affect your 
language) and we assume that SCL has equality.

Model theory: again very straightforward, the current MT without the 
need to be fussy about syntactic categories of symbols.  Names in a 
relation position are required to denote things in R; names in any 
argument position are required to denote things in I.  P(t1...tn) is 
true in I just when <I(t1).....I(tn)> is in ext(I(P)), end of story.

-----

The header vocabulary consists of the following:

Ind
Rel
Fun
Arity

plus numerals and =.

Note, allowing numerals in the header vocabulary does not imply that 
they must be part of the body vocabulary.

Semantic conditions (note, on the interpretation, not the superinterpretation):
ext(I('Ind'))=I (of the subinterpretation, ie the interpretation of 
the body, that is.)
ext(I('Rel'))=R (of the subinterpretation, so that we are not obliged 
to accede the truth of  Rel(Rel)) in the header.)
ext(I('Fun'))= the subset of R with functional extensions, i.e.
{r: if <x,x2....xn> and <y, x2,...xn> in ext(r) then x=y}
<R,n> in ext(I('RelArity')) iff there exists a tuple <x1,...,xn> in ext(R)

This is enough (with equality and maybe quotation) to specify a range 
of syntactic conditions. For example:

Relations are not in the universe of discourse:
not (Rel(?x) and Ind(?x))

Relations are in the universe of discourse:
Rel(x) implies Ind(x)

All relations have a fixed arity:
Fun(Arity)

The arity of relation R is 7:
Arity(?x, R) iff ?x=7
or
Arity(R)=7
Note that the latter entails Fun(Arity), however.

R can take precisely 2, 3 or 5 arguments:
Arity(?x, R) iff (?x=2 or ?x=3 or ?x=5)

-----

We could get more ambitious, by invoking other things in the header, such as

concat (a function on strings)
dequote (a function)
with conditions:
concat is concatenation of strings
<I(s),s> in ext(I('dequote')) whenever I(s) is defined, otherwise 
<s,s> in ext(I('dequote'))
  and then we can do things like:

Relation names all begin with an uppercase letter:
Upcase(?x) iff (?x='A' or ?x='B' or ... or ?x='Z')
Rel(?x) implies (exists (?y ?z) (Upcase(?y) and ?x=dequote(concat(?y,?z)) ))

BTW, this illustrates rather forcibly the way in which SCL is not higher-order.

The header would be a very natural place to put typing/sorting 
information also. Then eg an assertion like

Married(?x ?y) implies (Male(?x) and Female(?y) ) or (Male(?y) and Female(?x))

is simply an assertion when placed in the body, but it becomes a 
syntactic well-formedness restriction when placed in the header. In 
the first case,

Married(Joe, Bill)  & Male(Joe) & Male(Bill)

in the body is inconsistent: in the second case, it is consistent but 
inappropriate (a sort violation, required to be reported as a syntax 
error.)  I havn't yet worked this out in detail, however.
-----
We could also do more if we allowed more expressivity in the header, 
eg integer inequality relations. Rather than just speculate, however, 
it might be best initially to keep this very simple, e.g. just the 
Rel/Ind/Fun/Arity part of the vocabulary. We can add things later if 
this works out, or just permit more elaborate header vocabularies.

------

Horrocks sentences give no trouble, of course. But we have a little 
extra flexibility, since we can now make assertions about the 
relations in a first-order language without thereby requiring them to 
be in the universe of a satisfying interpretation, by placing the 
assertions in the header.

FOL in SCL:

For any FOL language L there is a corresponding SCL header containing

not (Rel(?x) and Ind(?x))
Fun(Arity)
and for each relation symbol R in L of arity n,
Rel(R) and Arity(n,R)
and each function symbol f in L of arity n-1
Fun(f) and Arity(n,f)
and for each individual name a in L
Ind(a)

I think that is all that is needed (?); then any satisfying FO 
interpretation of the body will be a satisfying SCL interpretation of 
the document, and any SCL interpretation satisfying the document is a 
superinterpretation of a FO interpretation satisfying the body.

One aside which will be relevant. Obviously in this FO case, the 
header vocabulary 'Rel' and 'Fun' and 'Arity' cannot appear in the 
body since they are syntactically illegal there. However, 'Ind' 
could; but there is no need to change the signature of the language 
in order to effectively use it, since in any body, Ind can be 
replaced by any tautological property: in particular, we can think of 
Ind(x) as represented in the body by the sentence x=x, ie something 
is an individual iff it is in the range of the identity. This will be 
significant below.

-------

SCL in FOL

We can give a uniform translation of any  basic SCL axioms (ie 
documents with an empty header) into a standard FOL language using 
holds-n and app-n in the usual way. Call this HAL (holds-app 
language): its header has the form

not (Rel(?x) and Ind(?x))
Fun(Arity)
Rel(holds-n) and Arity(n, holds-n)  for any n
Fun(app-n) and Arity([n+1], app-n) for any n (where [n+1] is the 
numeral one greater than n, ie [2+1]=3 etc.)

That's all we need for documents with an empty header: but now we 
need to consider how to translate a document <H1,B1> with a real, 
non-empty, SCL header, which is where Tenel's 'two equalities' thing 
becomes relevant. First, the Fun and Rel assertions in the header are 
replaced by Ind assertions, and all the Arity assertions are just 
deleted (they are used in the translation in order to map to the 
appropriate holds-n and app-n, of course). But we also have to modify 
the body, since the intended universe of discourse for H1 is 
different from that in the HAL embedding: all the relation and 
function names from H1 are now individuals, and they didn't used to 
be. The general technique for this is obviously to introduce a 
category of 'real individual', to assert that the old rels and funs 
are not real individuals, and to restrict all quantifiers to real 
individuals.

That is the general-purpose way to do it, but we can be more 
efficient in this case since the HAL body is so very special and 
regular in its construction. Note that all terms denoting 
H1-non-individuals occur in the first argument position of holds-n or 
app-n, and do not occur anywhere else.  Recall also that Ind(x) can 
be rendered as x=x; so the effect of this embedding is to replace = 
by a special 'HAL-FOL-equals',  which is = restricted to that part of 
the universe corresponding to Ind in the H1 header, which we can 
characterize syntactically in HAL as equality applied only to terms 
in the second and subsequent arguments of holds-n and app-n 
relations.  Write this as infix ~, then HAL indeed (as Tanel has 
always insisted) needs to have two distinct identities: = translates 
general SCL identity, and ~ translates FOL identity. Of course ~ is 
identical to = everywhere the former is defined.

This last part needs to be argued more carefully, of course, but I am 
confident that it works out as Tanel suggested.

-----

Anyway, I feel that this header/body idea can be used as a useful 
framework within which to unify and regularize a number of the issues 
we have been threshing on, and might allow us (not to mention 
everyone else) avoid talking past each other. It also deals with a 
central issue we have not yet paid any serious attention to, which is 
how SCL users can 'declare' particular SCL languages.

Comments?

I plan to try to get this written up in a reasonably exact and 
readable way in the next few days, unless anyone objects, 
<em>hopefully</em> by Thanksgiving (Thursday). I think the best way 
to do it for pedagogic purposes is to do it using a particular 
concrete syntax, then subsequently generalize to an abstract syntax. 
Otherwise there is too much 'new' stuff to swallow all at once.

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