[SCL] fitting interpretations onto ontologies

[pat hayes]

Chris (and others), I would appreciate your input on this technique 
which Im trying to use, to adapt your AS to the view of SCL as a 
'single language'.

The idea is to avoid the lexical classification by treating an 
interpretation initially in a very permissive way: it is just a 
structure and a mapping from a single homogenous vocabulary, with no 
lexical distinctions.  But given some sentences O and an 
interpretation I on the vocabulary of O, there is still a kind of 
lexical decision to be made about whether or not I 'fits' the 
expressions in O properly. Interpretations which don't fit are simply 
not considered as being involved in the semantic discussion - in 
effect, they are not counted as 'legal' interpretations of O - so any 
questions about the denotations of expressions in non-fitting 
interpretations simply do not arise.

Formally, I satisfies O when I fits O and I(O)=true, and then 
entailment is defined in the usual way.

The current definition of 'fit' is:
for any name x,
if x occurs in object position in O then I(x) is in UI;
if x occurs in a relation position in O then I(x) is in RI;
if x occurs in a function position in O then I(x) is in RI and I(x) 
is functional.

This is just a transliteration of your AS&S lexical construction, of 
course, but it allows the lexical categories to depend on the way the 
symbols occur in O rather than being part of an externally defined 
signature.

To emphasize, if I does not fit O then it might as well not be an 
interpretation of O - we only care about interpretations which fit - 
so we aren't obliged to say how the truth-recursions pan out in those 
cases. So we don't need to insert a whole lot of extra stuff into the 
interpretations just to avoid having 'empty' denotations.

Now, in the case where we can make lexical assignments, in the style 
of your document, then we can incorporate the 'fit' into the very 
definition of the interpretation, so we can guarantee that 
interpretations always fit, by construction, and then of course we 
don't need to mention it further.  This is a kind of lexical 
context-free notion of fit.  But this is an extreme case (the other 
is our old wild west CL where everything fits every role, and so 
again we don't need to consider explicit fitting, but at the cost of 
having to have a lot more semantic machinery to cover the peculiar 
cases.)  It is not essential that we make the fit lexically explicit 
in this way: all the semantic machinery seems to work (this is where 
I'd value your opinion, and particularly if you can see any obvious 
snag I may have missed) even if the fit is defined contextually, as 
long as it is unambiguously determined by the expressions themselves 
in all cases.

-----

Moreover, and this is where I'd *really* like your opinion, this 
seems to work in a wider range of cases, maybe even on the full WW 
syntax, so we could allow variables in function position.  Here's how 
it would go.  Say that I fits O when the above conditions hold not 
just for names but for all terms. That is, in particular, if t is any 
term in a function position then I(t) must be functional, in order 
for I to fit O. This would apply to variable mappings also, so that 
the quantifier case in the truth recursion would say that
I('forall (?x1 ... ?xn) s' ) = true when for any variable mapping A 
on {x1...xn}, *if [I+A] fits O then* [I+A](s) = true.
where the additional *-* clause ensures that bindings which would put 
a nonfunctional relation into a functional position are simply not 
considered, so we do not need to worry about what the term would 
denote in such a case. Basically, whenever we consider assignments to 
lexical entities (names or variables) we always thereby restrict 
ourselves to considering only interpretations which fit the 
expressions being considered. So rather than insist that all 
interpretations provide a 'dummy' functional meanings for all 
individuals, just in case that entity gets to be used as a function, 
we instead say that any interpretation that tries to use a 
non-function as a function is thereby disqualified as a legal 
interpretation, since it violates (subtly, but still violates) an 
essentially syntactic condition that expressions in a functional 
position must denote functions.

Now, this can be extended to more restricted signatures. For example, 
suppose we know as a 'syntactic' matter (never mind exactly how, for 
the present) that 'R' has to denote, say, a binary relation: then if 
ExtI(I(R)) contains any non-pair sequences, then I doesn't fit. 
Again, if that information is given as part of a lexicon, then of 
course we can incorporate the fitting into the very definition of an 
interpretation, rendering the concept unnecessary: but the cost of 
this conventional strategy is that we would need to provide a way to 
declare arities somehow in any interoperable SCL notation. Whereas, 
if we simply provide the special relation symbol Arity, with 
appropriate semantic conventions, then this information can be 
incorporated into the SCL ontology itself as an assertion: and the 
presence in an ontology O of an assertion like

(forall (?x) (iff Arity(R, ?x) ?x=2) )

is sufficient to ensure that any interpretation which satisfies *and 
fits* O will have an appropriate extension for R. This avoids the 
otherwise somewhat uncomfortable need to make all functions total for 
any arity in any interpretation, by the way: if they have an arity 
declared, then they need only be functional on sequences of those 
arities, since any interpretations which assign them to other kinds 
of extension will never make it through the 'fit' defined in the 
truth-recursions.

For example, consider:

forall (?f)  ?f(?f(@x) @x)

?f occurs in function position, so any interpretation which assigns a 
nonfunctional value to ?f does not fit this. An interpretation I 
satisfies and fits this when for some variable mapping A on ?f , 
[I+A](?f) fits the whole expression and satisfies the body, which of 
course it will when it is functional (for any assignment to @x, ie 
for every arity).  If there are no such functional relations in RI 
then this will not be satisfied by I and so will be false in I. So 
this axiom is satisfied by any interpretation which has at least one 
fully variadic function (like 'list', for example) in the universe of 
relations.  Being as it were a functional tautology, this makes 
sense, since this obviously ought to entail

exists (?f)   ?f(?f(@x) @x)

which simply asserts that such a function exists: and it does. 
Notice that it does not assert that all relations are functions, 
since the occurrence of the ?f in a function position in the body of 
the quantified statement in effect restricts the quantifier to 
functional relations.  This is the only nonstandard consequence, as 
far as I can see: it means that the true range of a quantifier 
depends on what kinds of position the variable occurs in in the body 
expression. But this is easy to adapt to, once you get used to it; 
and it corresponds exactly to the relation/individual case; and of 
course it does not affect the FO case at all.

Anyway, this all emerged as a kind of side-effect of trying to write 
up the document, so Im going to go ahead with this until someone 
tells me I shouldn't or I find some fatal flaw; at which time I will 
just revert to not allowing anything but constants in function 
position.

Pat

PS. In answer to John's question:

>Question:  What if I write (x y z w) in a KIF-like syntax, and x is not
>a relation?  Is that false?  Or is it syntactically incorrect?  Is there
>a distinction between simple falsity and syntax errors?  If there is no
>such distinction, what happens if I write (not (x y z w))?  Is it true?

the answer that this gives is, is that just writing that down 
*asserts* that x is a relation. And if that expression were a term 
instead of an atom, then it asserts that x is a function(al 
relation). If x is a variable, then the variable is required to range 
over relations (which may also be individuals) or functions (which 
are relations and may be individuals) respectively. In other words, 
the nasty cases are simply ruled out as examples of 'bad fit'.  The 
difference from a conventional logic is that in general, the 
determination of whether this is a syntactic matter or a semantic one 
is blurred. In particular cases we can un-blur it (eg a GOFOL syntax) 
but having this be the general case allows us to have SCL be 
self-describing in a much more uniform way than would be possible in 
a conventional framework.

PPS. It occurs to me that this is very like the distinction between a 
'static' sorted logic and a language with implicit/dynamic typing: in 
fact it is probably a special case of it with just three sorts (or 
rather more if distinguish the arities as syntactic fittings.)

-- 
---------------------------------------------------------------------
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://philebus.tamu.edu/pipermail/scl/attachments/20031204/9882781c/attachment.htm