- From: Michael Kifer <kifer@cs.sunysb.edu>
- Date: Sun, 17 Aug 2008 14:23:37 -0400
- To: Dave Reynolds <der@hplb.hpl.hp.com>
- Cc: RIF WG <public-rif-wg@w3.org>
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 Sunday, 17 August 2008 18:24:58 UTC