Re: Notes on 7/20 BLD draft

> 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

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

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
>

Received on Thursday, 26 July 2007 12:17:32 UTC