Re: Preconditions /effects vs Preconditions/Postconditions

Drew McDermott wrote:
>
> 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."

Well, this definition of a postcondition (in program verification) is not
that much different from mine.  The difference is that in one case
postconditions are being proved and in another they are used as
constraints. In databases, integrity constraints on the after-state of a
transaction are often called postconditions.  (If such constraints are not
satisfied, the transaction is rolled back.)

The important similarity between both cases is that they are predicates and
they are evaluated in the after-state only.

Even in programming logic, the reason why you want to prove a postcondition
on a program (assuming a precondition is true) is because you want the
postcondition to be true in the resulting state (otherwise the program is
deemed not to be correct). That is, even here the postcondition is
ultimately viewed as a constraint. (Of course, there can be other uses for
such proofs. I am just pointing out the similarities of some of these uses
to my terminology.)

The particular classification that I mentioned in my msg comes from the use
of these terms in Transaction Logic. I also remember discussing these
things with Ray Reiter about 10 years ago, when we first developed
Transaction Logic, and we didn't have terminological disagreements on that
point.


> 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.
> 

I didn't say that effects are propositions. Well, they *can* be, but there
is a big difference. The "effect" is the change that is made to the
theory. I.e., inserted facts, deleted facts, other deleted/inserted
formulas, etc. They are things that are made true or false -- i.e., they
are "imposed," as you put it.  While pre and post conditions are simply
checked. So, I don't see any difference between our views on that point.


	--michael

Received on Wednesday, 17 September 2003 01:31:27 UTC