Re: Preconditions /effects vs Preconditions/Postconditions

At the risk of being pedantic ...

   [Michael Kifer]
   There is a clear distinction between effects and postconditions.
   An effect is what the action *does*.
   A postcondition is a constraint that says what must hold after the action
   executed or else the action should be aborted and its effects undone. This
   constraint represented by the postcondition can be partial.

I've never heard the terms used that way before.  Sometimes the phrase
"safety conditions" is used (e.g., in PDDL 1.0), to mean roughly what
you call "postconditions."  (Well..., safety conditions are supposed
to hold in all situations, and postconditions just in situations after
a certain action.)

In the field of proving program properties, "postcondition" is used to
mean what's true after a statement given that something else is true.
Usually the inference is regressive (from effects to causes).  E.g, if
postcondition x>5 is true after x := x +1, then the weakest
precondition that would guarantee that is x > 4.

That's pretty close to what the planning community means by "effect."

However, I'm not entirely happy with saying that 
effects/postconditions are propositions.  They have the same syntactic
form, and, for pragmatic reasons, the same type (Boolean? or something
slightly hairier).  But effects differ from preconditions in certain
ways.  For instance, in PDDL the effect (when p e) means that if
proposition 'p' is true before the action, then effect 'e' is imposed
after.  Note that I use the phrase "is imposed" rather than "is true."
It's not clear in what sense (when p e) is true *after* an action; two
situations must be taken into account.  (In DAML-S, instead of 'when' we
have conditional effects.)

One can also argue that (not q) as an effect has a different semantics
from (not q) as a proposition.  There have been lots of variations on
the theme, but the basic idea is that (not q) is imposed by changing
the model of the current situation "just enough" to make 'q' false.

End core dump.

-- 
                                             -- Drew McDermott
                                                Yale Computer Science Department

Received on Tuesday, 16 September 2003 07:56:32 UTC