Re: CORE: nascent issues list

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 17:40:23 UTC