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