Re: Grounding puzzle

[Drew McDermott]
> 
> 
>     [me]
>    > (define_process call_ashcrofts_friendly_db
>                     :inputs (ssn: US_Social_Security_number)
>        :outputs (pn: US_phone_number)
>        :definition
>           (send dest <= ashcrofts_pn_port
>                 message <= ssn
>                 response => pn)
>        :effect (forall (p: Person pn: US_phone_number)
>                      person_has_SSN(p, ssn(v @))
>      & person_has_phone(p, pn)
>     |->
>     pn = pn(^ @)
>      & i_know(person_has_phone(p, pn(^ @)))))
> 
>    > Is that elegant or what?  
> 
>    [Yuzhong Qu]
>    So far so good. But the modal operator "i_know" may complicate the
>    formalism, while it brings more powerful expressiveness.
> 
> Yes.
> 
>    In this case, in addition to " pn = pn(^ @)", the another effect
>    may be the recording of the successful query event.
> 
> What is a successful query event?  One that terminated, one that got
> the right answer, ...?  In any event, surely the query was successful
> if after receiving the answer one knows that the result returned by
> Friendly DB, Inc. is the phone number of the person inquired about.

I meant that the event recording should be taken place at the service endpoint as an effect.

The record may contain the event time, which ssn is required, the phone number is found and returned, etc. It's not related with the decision issue of whether or not the answer (returned phone number) is right. I think it's another issue, and should be represented by another process.

> 
>                                              -- Drew McDermott
>                                                 Yale University CS Dept.

Thanks!


Yuzhong Qu
Dept.Computer Science and Engineering
Southest University, Nanjing, China

Received on Thursday, 2 October 2003 23:27:46 UTC