Re: ISSUE-91

Chris Welty wrote:
> 
> At the F2F12, there was discussion of "bounded quantifiers" (e.g. Forall 
> (x in C) ...) in PRD, and the suggestion was made to put them in Core, 
> and thus into BLD as well.
> 
> This would require re-issuing LC for BLD.
> 
> 
> It seems to me this could be done simply as syntactic sugar, ie
> 
> Forall (x in C) Q :- P
> 
> is syntactic sugar for
> 
> Forall (x) Q :- P AND C(x)
> 
> and just allows an implementor to more easily recognize the restriction 
> on the quantification (this is a common source of optimization in 
> implementations).
> 
> Anyway, let's have a brief discussion about the pros/cons on Tuesday.

It seems like a simple bit of syntactic sugar and if that noticeably 
helps uptake then it may be worth doing. I certainly wouldn't object to 
it if that is the consensus.

However, I don't quite see why detecting that there are terms of the 
form C(x) in a rule premise is such a hard job and so why a custom 
syntax really helps that much with implementing such optimizations.

Would the syntactic sugar really be needed in Core (and thus BLD) or 
would it only be needed in PRD?

Dave
-- 
Hewlett-Packard Limited
Registered Office: Cain Road, Bracknell, Berks RG12 1HN
Registered No: 690597 England

Received on Monday, 16 March 2009 17:25:51 UTC