[SCL] Headers and bodies

[pat hayes]

>Hi, everyone..
>
>Man, it's tough just trying to read all the text Pat can generate 
>much less understand it and reply to it, but here goes.  I have some 
>comments on what (I think) I understand so far..
>
>>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.
>
>Not sure about the headers yet, but I like the idea of the single 
>category of names.  To anticipate some of Pat's later comments, it 
>often comes up in practice that ontologist A writes an ontology 
>where what would conventionally be taken to denote kinds are meant 
>by them to denote individual things.  For example:
>
>   Chemical:
>     Hexokinase
>     SodiumChloride
>     ...
>
>   Model:
>     F-150
>     Taurus
>     Explorer
>
>These "individuals", for another ontologist B, would be kinds.
>
>>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.
>
>This might not be so simple.  If I have:
>
>   (forall (?r ?x ?y)
>     (=> (reflexive ?r)
>         (=> (?r ?x ?y) (?r ?y ?x)))
>
>   and
>
>   (reflexive nextTo)
>
>In the same ontology, it's not apparent from the parse that nextTo 
>is supposed to be a relation symbol without knowing something 
>(semantic) about the ontology in question, namely (=> (reflexive ?r) 
>(relation ?r))

Well, in general, unless you explicitly say so, or it can be inferred 
from the syntax, you don't know  whether or not something is a 
relation. That is a feature, let me emphasize: that is how Chris 
enabled SCL to handle the Horrocks sentences properly.

In this case, however, the general SCL syntax requires that the ?r in 
the first axiom must denote a relation (it occurs in a relation 
position) and the implication would enable you to infer as follows:

(reflexive t)
|-
(implies (t ?x ?y) (t ?y ?x))

from which again the SCL interpretation rules say is satisfiable only 
if t denotes a relation; so, in this case you can in fact infer that 
reflexive things must be relations.

>>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.
>
>Good.
>
>>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.
>
>Forgive me for perhaps not studying what Pat wrote thoroughly 
>enough, but I'm not sure that what he's talking about doesn't entail 
>arbitrary semantic conditions, or at least the presence of some 
>small super-ontology that distinguishes between relation and 
>individual.

It *allows* arbitrarily complex headers, but the only ones that we 
are obliged to research in detail are the particular ones that we 
actually use, notably the FOL headers.

>
>[lots of good stuff skipped]
>
>>-----
>>
>>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)) ))
>
>How about the case:
>
>   Rel(Foobar)
>   Rel(foobar)
>   =(Foobar,foobar)
>
>You'd need an additional axiom constraining relations to only have one name.

Ah yes, indeed. OK, what that says is that every relation has at 
least one uppercase name. OK, I havn't thought that string-dequote 
stuff through thoroughly.  Pretend I never mentioned it: lets ignore 
trying to be that clever for now.

>
>In general, I'm not sure that all of this is making things any 
>simpler.  Perhaps so and I'm not understanding fully, but it seems 
>to be blurring the line between language and content, or between 
>meta-language and language.

Yes, I agree. Lets ignore that more ambitious stuff, please.

Pat

>I will study the rest more thoroughly and make comments (and/or 
>correct my comments).
>
>   .bill


-- 
---------------------------------------------------------------------
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