Re: CORE: nascent issues list

This can probably work as a shortcut, but first we need to agree on
the "ugly" version of the syntax and its semantics.

Regarding the variable arity, this is yet another complication. Some people
were pushing the requirement that each symbol can be used only in one way.
The result is that this has complicated BLD and it keeps haunting newer
developments. From my point of view, I would be happy to get rid of this
constraint, but there might still be opposition. Furthermore, since BLD is in
the last call, we probably cant make such changes any more.

michael

On Mon, 18 Aug 2008 10:37:25 -0700
Gary Hallmark <gary.hallmark@oracle.com> wrote:

> 
> you'd also need to extend builtins to support multiple arities for the 
> same function symbol.
> I think the builtin approach can be made to work but it's rather ugly 
> for my use case, because I always need to assert a classification and 
> the frame slots, so I always have a rule head like
> 
> And(func:genSym(long-argument-list)#MyType  
> func:genSym(long-argument-list)[slot1->value1 slot2->value2])
> 
> I prefer something more purpose-built:
> 
> New MyType[slot1->value1 slot2->value2]
> 
> This way, you don't have to write the long-argument-list twice -- you 
> don't write it all.
> 
> We can explain that the semantics are equivalent to the above where 
> long-argument-list is constructed from the rule ID, its Forall 
> variables, and an occurrence number (should multiple New formulas appear 
> in the same rule).
> 
> Michael Kifer wrote:
> >
> > On Sun, 17 Aug 2008 10:18:22 +0100
> > Dave Reynolds <der@hplb.hpl.hp.com> wrote:
> >
> >   
> >> Michael Kifer wrote:
> >>     
> >>> On Fri, 15 Aug 2008 16:07:45 +0100
> >>> Dave Reynolds <der@hplb.hpl.hp.com> wrote:
> >>>
> >>>       
> >>>> (c) some genSym builtin
> >>>>         
> >>> Just 0.02c: this cannot be in the Core or in BLD.
> >>>       
> >> Surely it could if it was deterministic (in which case genSym is not a 
> >> great choice of name).
> >>     
> >
> > Exactly. A builtin function instead of a gensym is a different matter.
> >
> >   
> >> Perhaps something like:
> >>
> >> """
> >> func:genSym
> >>
> >> (?arg1, ... ?argn;  func:genSym(?arg1, ... ?argn))
> >>
> >> Generates and returns a constant uniquely determined by the values of 
> >> the n arguments. This constant takes the form:
> >>     "gensym:ID"^^rif:local
> >> where ID is a string uniquely determined by the values of the arguments 
> >> ?arg1 through to ?argn. For example, this might be a digest of the 
> >> concatenation of the canonical lexical forms for each argument.
> >> """
> >>
> >> Thus to use it to generate skolem constants the rule author would need 
> >> to explicitly include a rule identifier and the values of the 
> >> universally quantified variables in the set of genSym arguments.
> >>     
> >
> > This would not be a Skolem function. You need an infinite supply of those
> > functions to achieve the behavior of Skolem functions. But because our
> > situation has restricted syntax, a builtin like this can go a long way, I
> > agree.
> >
> >
> > 	--michael  
> >
> >
> >   
> >> Would something along those lines be reasonable?
> >>
> >> Dave
> >>     
> >
> >   
> 
>

Received on Monday, 18 August 2008 18:28:37 UTC