- From: Drew McDermott <drew.mcdermott@yale.edu>
- Date: Sat, 20 Sep 2003 14:50:15 -0400 (EDT)
- To: www-ws@w3.org
[David Martin] Isn't this [spelling out whose phone number is returned] precisely this sort of thing one could express as either the "effect" or the "postcondition" of a service (depending on how that terminological distinction gets resolved; I'm pretty sure Michael K. would call this a "postcondition"). That is, one would specify SSN as an input, and PhoneNumber as an output, and one would have an effect (or postcondition) stating something like: exists P . [person_has_SSN(P, SSN) & person_has_phone(P, PhoneNumber)] This can't be right, because it's true before the service is contacted. I think it would be cleaner to write the following, where I'm now embedding the effect in the overall process, and extending the proposed DAML-S surface syntax to handle preconditions and effects: (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) person_has_SSN(p, ssn(v @)) -> then person_has_phone(p, pn(^ @)))) Here pn(^ @) means "the pn output of this process"; and ssn(v @) means "the ssn inputs of this process." ^ and v are approximations to the official uparrow and downarrow notation, which indicates that the notation need some fixing. It might be necessary to strengthen the final conclusion by stating explicitly the knowledge effect: i_know(person_has_phone(p, pn)) or i_know_referent(phone_number(p)). (See Reiter's book "Knowledge in Action" for one good theory of how knowledge effects work.) We also need to strengthen the process description to make it clear that the Ashcroft service didn't change the person's phone number and then send you the new number. The definition of call_ashcrofts_friendly_db is from the point of view of the agent using the service. The input to this process gets transferred to the message input of the 'send' process; the response output of the 'send' then gets transferred to the 'ssn' output of this process. -- -- Drew McDermott Yale Computer Science Department
Received on Saturday, 20 September 2003 14:52:13 UTC