Re: Notes on 7/20 BLD draft

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

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

Received on Tuesday, 24 July 2007 19:35:17 UTC