Re: [isabelle] Non-determinism

Randomness presumes a sequence of events that are being observed (and
the outcome of each individual event cannot be predicted).  Doing this
formally can get pretty involved.  Joe Hurd did a formalisation of
probability theory in HOL4.

I do not know which problem you are trying to solve, but normally
non-determinism is easiest modelled through a relation (or predicate).
That is, if your system can make the transitions a -> b and a -> c,
both (a, b) and (a, c) would be in the relation.


Thank you very much.
I seem to have resolved my problem (for the moment).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.