Re: [isabelle] Non-determinism
On Thursday 07 September 2006 16:09, Gabriele Pozzani wrote:
it's possible to do a non-deterministic assignment in Isabelle, or
Or, it's possible generate a random integer?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and