Phil, On Sunday 23 Sep 2012 21:11, Phil Clayton wrote:
> By making initialization an operation without a before > state, the initialization can be used with schema > operators such as composition and pre, e.g. > > Init ⨟ Op > > pre Init > > the latter being another way to write the following: > ∃ Init ∙ true > ∃ State' ∙ Init That had occurred to me. But it didn't seem to me a particularly good idea. One could generally state the non-emptyness of some schema S as pre S', but surely its clearer to say ∃ S ∙ true. (and Init /\ Op does the same under Spivey's convention as Init ⨟ Op under the other). There doesn't seem to be much to chose between them. Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
