- From: Drew McDermott <drew.mcdermott@yale.edu>
- Date: Thu, 2 Oct 2003 13:28:26 -0400 (EDT)
- To: www-ws@w3.org
[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.
--
-- Drew McDermott
Yale University CS Dept.
Received on Thursday, 2 October 2003 13:28:27 UTC