Re: Notes on 7/20 BLD draft

On Thu, 26 Jul 2007, Chris Welty wrote:

>
> Michael,
>
> I guess I'll continue this since it appears the problem is that we
> don't understand each other, and not that there is disagreement (yet).
>
>  > Forall X (p(X) <- Exists Y q(X,Y))
>  >
>  > Please show what exactly is the form that you want for the above. As
>  > Hassan and I mentioned, this is equivalent to
>  >
>  > Forall X,Y (p(X) <- q(X,Y))
>
> Of course it is equivalent, isn't that my point????   The former is
> not in prenix and the latter is, but they are equivalent.  I don't
> understand what you are getting at.   Every sentence with existential
> in the body has an equivalent that doesn't.  I keep saying this, and
> you keep saying it back.
>
> That rule (expressed in prenex) doesn't have existentials in the body,
> but here is an example of a rule with existentials in the body
> represented in prenix normal form:
>
> Forall X Exists Y (p(X) <- q(X,Y))
>
> So nothing about prenix normal form prevents existentials in the body,
> but I can't imagine that would be your point, because I'm sure you
> know this. I *really* don't understand what you are getting at.

But the above is not a Horn and is not equivalent to Horn. That is, it is
not the same as  Forall X (p(X) <- Exists Y q(X,Y))

So, I fail to understand how does your suggestion apply to the basic logic
dialect.

> Is the problem that I'm saying "existentials in the body" and mean
> "existiallly quantified variables in the body" and you are saying
> "existentials in the body" and mean "existential quantifiers in the
> body".  Is it the case that you just want the quantifier itself to
> appear in the body?

There was a decision to allow existential quantifiers in the body.
Existential quantifiers in the body == existential vars in the body.
Horn dosnt have a prenex form which has existential vars. Your example is
prenex, but not Horn. I think uu got confused about that point.

michael

>
> -Chris
>
> Michael Kifer wrote:
> >
> >> Hassan Aït-Kaci wrote:
> >>> Chris,
> >>>
> >>> Prenex form is a normal form for FOL, butnot for Horn logic. In other
> >>> words,
> >>> the prenex form of a Horn sentence may be non-Horn. Existentials in the
> >>> condition part (the 'body' of a clause) are universals in hiding due to
> >>> the 'not' lurking there (a <- b = a \/ not b). In fact, existentials in
> >>> the body are allowed in (non-Horn) logic programming languages - e.g.,
> >>> based on Hereditary Harrop Formulae -or H2Fs). They are conveniently
> >>> used programmatically for hiding local variables. The same for local
> >>> implications (used for hypothetical reasoning) - also possible in
> >>> H2F programming - e.g., lambdaProlog).
> >>>
> >>> Conclusion: your proposal re using prenex only will work for pure Horn
> >>> languages, but not for other FOL dialects. This is what Michael tried
> >>> to explain - I think.
> >> *sigh*
> >>
> >> I failed again to completely capture my proposal in that one
> >> paragraph, but I know I said it at some point - in addition to prenex
> >> syntax, the BLD would of course need additional constraints to stay in
> >> horn, such as (but not limited to) restricting existentially
> >> quantified variables from the head.  But for sure EVERY *first order*
> >> dialect can be expressed (with suitable restrictions for the dialect
> >> of course) in prenex.
> >>
> >> I think it is just a cleaner syntax, but as I said I really don't feel
> >> that strongly about it....each time I reply to a message in this
> >> thread I hesitate even longer wondering if it is worth it....
> >>
> >> I guess the thing that "bothers" me about the current syntax is the
> >> asymmetry of quantification, and this is what I'm trying to "fix".
> >> Logic has a certain beauty to it, you know.
> >>
> >> -Chris
> >
> > Chris,
> > it does not look like what you are proposing is simpler, since after all
> > these messages neither Hassan, nor Harold, nor me were able to understand.
> > Perhaps you could explain this by example? For instance, let's consider
> >
> >
> > But then you do not have existentials in the body. And we made a decision
> > to allow them for various reasons (e.g., to set the stage for Lloyd-Topor,
> > to let people write things the way they like, etc.).
> >
> >
> > 	--michael
> >
> >
> >
> >>> -hak
> >>>
> >>> Chris Welty wrote:
> >>>
> >>>>
> >>>> Michael Kifer wrote:
> >>>>
> >>>>>> Michael Kifer wrote:
> >>>>>>
> >>>>>>>>>> * It seems to me a cleaner syntax is to remove existentials from
> >>>>>>>>>> conditions and unify all quantifiers outside the rule (as with
> >>>>>>>>>> universal now), and add a restriction in horn that existentially
> >>>>>>>>>> quantified vars cannot appear in the conclusion.
> >>>>>>>>> The RIF Basic Condition Language is meant to be reusable also
> >>>>>>>>> (in PR and) outside the context of any rule, stand-alone (e.g.
> >>>>>>>>> for queries and integrity checking), where existentials cannot
> >>>>>>>>> be rewritten as universals in the Example 3b.->3a. manner.
> >>>>>>>> Oh, you misunderstood - I did not mean eliminate existentials from
> >>>>>>>> the syntax entirely, I meant move them outside conditions into
> >>>>>>>> some sort of wrapper or context (like, rules).  This would make,
> >>>>>>>> at least, the rule syntax cleaner.
> >>>>>>> Unless I misunderstood you, what you are proposing is not sound in
> >>>>>>> FOL:
> >>>>>>>
> >>>>>>> Exists X foo <- bar(X)
> >>>>>>>
> >>>>>>> is not the same as
> >>>>>>>
> >>>>>>> foo <- Exists X bar(X).
> >>>>>> As you know full well this kind of mapping is easily fixed by
> >>>>>> rewriting the variable names.
> >>>>>>
> >>>>>> -Chris
> >>>>>
> >>>>> No. foo <- Exists X bar(X) is foo \/ not Exists X bar(X)
> >>>>> which is foo \/ forall X not bar(X)
> >>>>> which is forall X foo <- bar(X) (after possible variable renamings).
> >>>>> This is different from Exists X foo <- bar(X).
> >>>>
> >>>> Hmmmm.  We seem to be agreeing furiously.  Sorry if I'm being too
> >>>> opaque and imprecise - it comes from terseness.  I'm merely proposing
> >>>> prenix normal form (for rules).  Any first order sentence can be
> >>>> written in prenex.
> >>>>
> >>>> My only reason for this proposal is that it seems to be a cleaner and
> >>>> easier to process syntax.  Do you agree?  I don't feel that strongly
> >>>> about it, but each time I see the abstract syntax it reminds me that
> >>>> prenix would be simpler.
> >>>>
> >>>> -Chris
> >>>>
> >>>>> So, your proposal amounts to removing existentials from the rules
> >>>>> completely.
> >>>>> This is how we understood it and Harold pointed out that there was
> >>>>> a decision to keep the existentials in the rule body.
> >>>>> Then you said that you did not mean to delete the existentials, but
> >>>>> to move
> >>>>> them to the outside of the rule. I pointed out that this is unsound, and
> >>>>> your remark about fixing this by renaming is wrong, as shown above.
> >>>>>
> >>>>> Did I misunderstand u again?
> >>>>>
> >>>>>
> >>>>>     --michael
> >>>>
> >>>
> >> --
> >> Dr. Christopher A. Welty                    IBM Watson Research Center
> >> +1.914.784.7055                             19 Skyline Dr.
> >> cawelty@gmail.com                           Hawthorne, NY 10532
> >> http://www.research.ibm.com/people/w/welty
> >>
> >
> >
> >
>
> --
> Dr. Christopher A. Welty                    IBM Watson Research Center
> +1.914.784.7055                             19 Skyline Dr.
> cawelty@gmail.com                           Hawthorne, NY 10532
> http://www.research.ibm.com/people/w/welty
>

Received on Saturday, 28 July 2007 22:15:55 UTC