Deterministic.md 717 Bytes
Newer Older
1
2
3
4
5
6
7
Analysis of deterministic operations
------------------------------------

This analysis checks whether an operation is deterministically defined.
Intuitively, an operation is deterministic if the evaluation of
this operation applied to ground terms does not cause any non-determinism.
The determinism analysis returns `nondeterministic` for a given operation
8
if its definition contains overlapping left-hand sides or free variables,
9
or if it depends on some non-deterministic operation.
10
11
12
13
14

If calls to non-deterministic operations are encapsulated (by the
use of set functions or operations from module `AllSolutions`),
then it is classified as deterministic since the non-determinism
does not occur at the top-level.