Re: Grounding puzzle

   [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