Rewriting with a nondeterministic choice operator

AbstractThe priveleged field of classical algebra and term-rewriting systems is that of strictly deterministic systems: the confluence property is generally assumed to hold, which implies determinism for the result of the computations, even if there exist several different computation paths. In this paper, we introduce a bounded nondeterministic choice operator “∪” into algebraic specifications and related term-rewriting systems. The operator “∪”, which constructs sets of values, satisfies AC (associative-commutative) properties, which allows to apply results about equational rewriting. Attention is then mainly restricted to so-called regular systems, where nondeterministic choice is constraint-free. Several examples are considered, including a toy concurrent language, for which nontrivial properties may be automatically proved