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 simulate
it?

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.

Clemens






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