Re: Notes on 7/20 BLD draft

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.

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?

-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 Thursday, 26 July 2007 21:01:36 UTC