Re: Nonmonotonic rules

> >  >
> >>  >On Jan 21, 2004, at 3:15 AM, Michael Kifer wrote:
> >  > >[snip]
> ><snip>
> >  > Its interesting that this disagreement/misunderstanding can be rooted
> >>  in the differences between two world-views of what class-based
> >>  reasoning is really *for*, one based on DL's evolution from logic,
> >>  the other based on schemas considered as data descriptions. This
> >>  difference of perspectives keeps coming up and seems to be very
> >>  important: for example, does one think of range assertions as
> >>  constraints (datatype) or simply as assertions (logic)? How about
> >>  datatyping? And so on. We keep running into cases where people have
> >>  divergent intuitions which can be traced back to the differences in
> >>  attitude arising from these two world-views.  Clearly at some level
> >>  they are similar: Codd's Relational model and the DL logic-based
> >>  semantics all agree on the ultimate nature of relations and classes;
> >>  but the ways that the two communities think seem often to be sharply
> >>  different.  Im not sure how to characterize the difference, exactly,
> >>  but it seems to be that the DB world-view sees a sharp distinction
> >>  between different kinds of information, and tends to treat general
> >>  facts as conditions imposed on concrete facts: meta-data as opposed
> >>  to data.  Distinctions like this may be operationally important but
> >>  have no natural place in a logic-based perspective which historically
> >>  has been largely motivated by the desire to unify divergent sources
> >>  of information as far as possible into one uniform framework.

<snip>

> >  > .... if you think that the more general assertion's
> >  > chief purpose is to control, select or check the internal coherence
> >>  of a body of ground data, then the purely logical account of
> >>  quantification is inadequate or at any rate incomplete, since a
> >>  combination like
> >>  (forall (x) (R x x))
> >>  (not (R a a ))
> >>  is of course inconsistent, but inconsistent in a special way: the
> >>  second item is wrong, or should be rejected, as it fails to conform
> >>  to the schema. The schema has more assertional force than the mere
> >>  data in a DB world, since the schema is a kind of filter or guardian
> >>  of the data. Logic has nothing to say about intuitions like this.
> >
> >*Classical* logic has nothing to say about it. This doesn't mean that you
> >can't define a logic in which meta-info is treated differently from
> >"regular" data.
> 
> Oh, sure.  You can define a logic to do just about anything.  But I 
> don't trust these proposals until I see some kind of semantic 
> justification  for the distinctions they draw.  (Neednt be 
> *classical* semantic, but somehow non-arbitrary.) I confess to not 
> (yet) being familiar enough with F-logic to know if it has such a 
> justification.

The justification is that you need to be able to say that the data stored
in the database and the info that can be derived by the rules conforms to
some metadata (schema).


> >F-logic does this. It defines what it means to conform to
> >the meta-data (although not completely satisfactorily from the point of
> >view of programming languages).
> >There is also Typed Predicate Calculus (LICS-91), which espouses the same
> >idea (which later went into F-logic).
> >
> >The basic idea is that there is a notion of well-typed 
> >interpretations and only
> >those things are acceptable as models. So, you are not supposed to derive
> >things that violate the meta-data.
> 
> And of course 'classical' sorted and typed logics make a similar 
> distinction, but they encode it as a purely syntactic matter. I doubt 
> if this is adequate for our purposes here, however.

Yes and no. Sorted logics give you some of the stuff that is required in
the programming languages realm. But sorts are too weak to handle
polymorphism (especially when you have ad hoc polymorphism and
inclusion polymorphism together--we discuss these problems in the LICS-91
paper that I mentioned). There are order-sorted logics that solve the
inclusion poly problem, but not the combined inclusion+ad hoc poly problem.

(Inclusion polymorphism arises due to Isa.
Ad hoc poly is sometimes called "overloading" -- the ability to call the
same function with arguments of completely different types.)

The semantics of types in F-logic and Typed Pred Calculus does *not* have
all the benefits of sorted logics, and vice versa.  I haven't seen a
satisfactory solution that subsumes both.

To explain the problem, suppose we state:

    gradStudent subclass student
    gradFaculty subclass faculty

and define the following types:

    advisor: student     -> faculty
	     gradStudent -> gradFaculty

Now, if we also have

    bob  member gradStudent
    bill member faculty

Then what is advisor(bob,bill)? Well-typed or not?

It should not be (because bill is not a gradFaculty), but sorts alone can't
solve this problem. In an order-sorted logic, bob belongs to faculty as
well, and there is no violation of the sorts. So, the wrong type is not
detected.  The model theory of Typed Pred Calculus (and F-logic) can handle
this, but it has another problem: it can't distinguish type violation from
falsehood. For instance, the query

?- advisor(bob,123).

is just false, while it should somehow be illegal. On the other hand,
this type of violation is easy to catch in sorted logics.

The two ideas can actually be combined, but only as long as you assume
that the set of types is fixed. This is OK for many purposes in
programming languages, but not in KBs and even less so on the Semantic Web.

This is why I think KBs and the SW are different. You might want to define
derived classes from other classes/resources. For instance, the resource
may be a university database, and I might define gradFaculty as faculty who
have a PhD degree and are allowed to supervise grad students. (There may be
no explicit class or resource called gradFaculty.) And then I
might want to restrict input to my service XYZ to be objects of that derived
class.

In the situation where types can be defined by rules, the sorted logic
approach is inapplicable (and you don't even need polymorphism to see that).
At least I don't know how to do it using a sorted logic.

> Can you point me to any kind of general discussion of these issues 
> from a DB perspective?

I don't remember seeing any one place where several different views are
represented.
There was a lot going on in the logic programming community (LP) around 1990
(+/- 5yrs) and in the database programming languages (DBPL) community.
I haven't been working on this for some 8-9 years, and it is possible
that there is new stuff out there.

That LICS paper might be a reference. It discusses the issue from the point
of view of LP, which has stricter requirements than what might be
acceptable in databases.

The "strictness" part is just my opinion---DBLP people may say that
database requirements are as strict as anything else. But basically, I
think that in databases, KBs, and the SW, it is more important to ensure
that whatever you derive is well-typed than to prevent queries like
advisor(bob,123) above from ever being asked during computation/derivation.

I think the above example explains the main problems in a nutshell.


	--michael

Received on Thursday, 22 January 2004 23:29:28 UTC