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.


Proofpower mailing list

Reply via email to