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