the new construct

I have a problem with IRC, and it does not deliver what I typed. So, I put
my latest in this email:

<MichaelKifer> the new builtin or a function symbol act differently from
object creation in PR systems. In particular, multiple invocation of the
same new will give the same new object.

<ChrisW> ...so what is the semantics of NEW - does it behave that way? Could you use it for mapping constructor calls?
 GaryHallmark: i intend the semantics to be the same as if you replaced it in logic with a conjunction of 
 ...frames and membership
 
<MichaelKifer> new is just a builtin relation n+1 args that is supposed to be interpreted by a 1-1 function from D^n -> D.
 This was actually Dave's proposal. I am not aware of other logically clean ways to to this. It approximates function symbols and the new construct in PR, but is not exactly.
 N is the number of variables.
 Basically, u want to simulate a skolem function of N variables. The difference is that each time u use a skolem function, it is a new function (or constant). With the builtin, we have only one builtin like that, so it is always the same function.
 Christian, pls remember that there is no such a thing as a "newly created
 frame". Nothing is really created. It is a crude approximation of object
 creation.

Received on Tuesday, 2 September 2008 16:31:44 UTC