Re: SNAF, NAF, and monotonicity [was: Comments on * DRAFT * Rules...]

Dan Connolly <connolly@w3.org> wrote:
>
> On Thu, 2005-08-25 at 16:30 -0400, Michael Kifer wrote:
> > Dan Connolly <connolly@w3.org> wrote:
> > >
> > > On Thu, 2005-08-25 at 00:00 -0400, Michael Kifer wrote:
> [...]
> > > > Hi Dan,
> > > > Welcome to the discussion! Yes, it is very important to get to the bottom
> > > > of it so that everybody will start speaking the same language.
> > > > 
> > > > No, the above rule is nonmonotonic. If you add a color specification to
> > > > that car then :car.auto:specification will now include a color
> > > > specification and log:notIncludes will become false. Therefore 
> > > >     :car auto:color auto:black
> > > > will no longer be derived.
> > > 
> > > I don't understand. I understand monotonicity to mean
> > > that if you can derive F from a set of formulas A,
> > > then you can also derive it from the set A union B for
> > > any set of formulas B.
> > > 
> > > You seem to be suggesting there's some set of formulas B
> > > that when added to my A causes F to no longer hold.
> > > 
> > > Exactly what is that set of forumlas B? 
> > > Feel free to answer using Flora-2 syntax if that's more convenient.
> > > 
> > > You say "If you add a color specification ..." which suggests that
> > > B is something like...
> > > 
> > >   car auto:color auto:red.
> > > 
> > > but that doesn't falsify the premise:
> > > 
> > >  :car.auto:specification log:notIncludes {:car auto:color []}
> > 
> > I guess, I wasn't clear enough.
> > 
> > For you to show that your language is monotonic, you have to show that
> > 
> >    Forall A,B,F such that  A |= F implies A union B |= F            (*)
> 
> Yes, quite. We're clearly using the term 'monotonic' in exactly the
> same way. Good...
> 
> > So, you single example didn't prove (*). To refute your main claim,
> > I had to show the negation of (*), i.e., that
> > 
> >    Exist A,B,F such that   A |= F and  A union B |/= F              (**)
> > 
> > (|/= denotes "not entails").
> > 
> > So, I had to find A,B,F to demonstrate (**). I couldn't use your
> > example directly, because that particular example didn't provide me with
> > the appropriate A,B,F to demonstrate (**). (I only have to demo existence,
> > i.e., find one example, while you have to show (*) for all examples!)
> > So, I extended your example (or at least I thought that I did).
> > 
> > > Exactly what is that set of forumlas B? 
> > > Feel free to answer using Flora-2 syntax if that's more convenient.
> > 
> > Thanks for giving me an easy way out :-)
> > My example is indeed easier to use because it already has all the necessary
> > formulas in it.
> > 
> > Let me repeat this example for easier reference:
> 
> Thanks for going slowly...
> 
> >     We assume that the info about the cars (over which we are going to
> >     close off) is in module allAboutCars and the facts there have the form
> > 
> >     12345:car[color->red].
> >     45678:car[color->blue].
> >     ...
> > 
> >     The 12345 thing is supposed to be the vehicle id number or something.
> >     The first fact says that 12345 is an object in class car and the attribute
> >     color has the value red, etc.
> > 
> >     The above info on cars could be on some Web site, for example.
> > 
> >     Now, to express N3's
> > 	this log:forAll :car.
> > 	{ :car.auto:specification log:notIncludes {:car auto:color []}}
> > 	    => {:car auto:color auto:black}.
> > 
> >     one would write something like this:
> > 
> >     ?X[realColor->?Color] :- ?X[color->?Color]@allAboutCars.      (***)
> >     ?X[realColor->black] :- not ?X.color[]@allAboutCars.          (****)
> > 
> >     The first rule says that if the module allAboutCars has an explicit color
> >     for a car, then it is the real color of that car. You don't have this rule
> >     in your N3 example, but of course it is easy to add.
> > 
> >     The second rule says that if allAboutCars says nothing about a particular
> >     car's color then its color is black. This is a counterpart of your default
> >     rule, which involves log:notIncludes.
> > 
> > Now, let us assume that all the above formulas constitute the set A in (**).
> > 
> > Let's suppose 00007 is a car on the allAboutCars site, for which no color
> > information is available. Let 00007[color->black] be our formula F in (**).
> > 
> > Because allAboutCars says nothing about the color of 00007, we conclude
> > that 00007.color[] is false (00007.color[] means that there is some value
> > for the color attr in object 00007. We didn't find any, so it's
> > false).
> 
> Are you abbreviating there? I would think we conclude that
>  00007.color[]@allAboutCars
> is false.


Yes, 00007.color[]@allAboutCars. Sorry for the typo.


> (aside: In any case, in N3, the negation is not separated from the
> question of whether 00007.color[] occurs in allAboutCars.
> In N3, the notIncludes relation between syntactic formulas is just
> like stringNotMatch operation on strings or a notDivisorOf operation
> on integers; it's a decideable/computable recursive function. )


I would be more comfortable if this all were defined more formally.
I gave my best shot at informally talking about informal semantics of N3,
but we cannot really argue about logical properties of a language that
hasn't been given a model theoretic semantics.


> >  Therefore, we derive 00007[color->black] using the rule
> > (****). (The rule (***) doesn't fire, since its premise is false.)
> > Therefore,
> > 
> >         A |= F
> > 
> > Now, let B be 00007[color->yellow], which we would like to add to the
> > allAboutCars site.
> 
> add to the site? You mean change what @allAboutCars denotes? To do
> that is to consider a different interpretation of the formula(s) A,
> not to consider an additional set of formulas B.

No. We have a bunch of formulas

12345[color->red].
45678[color->blue].

at allAboutCars. Formally, being at allAboutCars means that all predicates
and methods there have a unique prefix (the same for the same module). So,
the above two being @allAboutCars really means that we have formulas like

12345['$&^allAboutCars*^%color'->red].
45678['$&^allAboutCars*^%color'->blue].                         (*****)
etc.

Adding 00007[color->yellow] to @allAboutCars means that B really is

00007['$&^allAboutCars*^%color'->yellow]                        (******)

and now we have the set of formulas A union B.

Recall that A was that bunch of formulas (*****) plus those pair of rules.
So, A union B is (*****), (******), and the rules (***)/(****).

Now we are making inference and what was a consequence of A is no longer a
consequence of A union B.


> >  Now, rule (***) fires, but (****) doesn't. So, we derive
> > 00007[color->yellow], but we don't derive 00007[color->black]. Therefore,
> > 
> >         A union B |/= F
> > 
> > so it is nonmonotonic.
> > 
> > 
> > The same thing basically happens in your N3 example.
> > 
> > There auto:specification is an attribute, which returns a set of objects
> > (which would formally be treated as terms). Somewhere you will need to
> > have a set of formulas (which will be part of the set A), which
> > would say which specific cars have which specifications.
> > 
> > So, if you have a car whose spec doesn't include color then you will derive
> > {... auto:calor auto:black} for that car. But if you throw in another
> > formula (our B above), which will give a color spec to that car then
> > { :car.auto:specification log:notIncludes {:car auto:color []}}
> > will not be satisfied and so the rule will not fire.
> 
> As I say, it seems to me that this is not exhibiting another set
> of formulas B, but just considering a different interpretation of
> the formulas A. In that interpretation, the premise is false and
> the conclusion is false, yes, but this doesn't seem to demonstrate
> non-monotonicity.


No, see above. It is a union of A and B. It is precisely what
nonmonotonicity means.


> > I should also say that it is dangerous for me to venture into making the
> > above claims about N3, since, as far as I know, N3 doesn't have a formal
> > logical semantics. So talking about logical entailment is taking too much
> > liberty. But I think I have intuitive understanding of the intent and armed
> > with the formal semantics of F-logic (which is close in spirit to N3) I
> > feel I am making a convincing informal argument for nonmonotonicity of the
> > informal semantics of N3.
> 
> The analogy between F-logic an N3 seems to work well enough in this
> case, but I am not yet convinced that this example shows
> nonmonotonicity. It still seems to me that you have to use
> unscoped NAF to get nonmonotonicity.

Unscoped NAF doesn't exist (only implicitly scoped NAF exists), so
according to you nonmonotonicity doesn't exist :-)


> 
> [...] 
> > > Monotonicity supports partial understanding...
> [...]
> > So, I don't buy the above argument of yours.
> 
> OK, well, I'd like to get to the bottom of this more clear
> technical stuff about monotonicity first; perhaps I'll return
> to the scalability discussion later...

Looks like a good plan.


	--michael

Received on Thursday, 25 August 2005 22:09:50 UTC