Rewriting with a nondeterministic choice operator: From algebra to proofs

Abstract

The privileged field of classical algebra and term rewriting systems is that of strictly deterministic systems: the confluence property is generaly assumed to hold, which ensures determinism about the result of the computations, even if there exist several different computation paths. In this paper, we develop a new formalism introducing a bounded nondeterministic choice operator @@@@@@@*T’ into algebraic specifications and related term rewriting systems; nondeterminism about the result becomes allowed in this framework. We define the algebraic and the operational aspects of such systems, and investigate their relationship. Methods à la Knuth-Bendix are developed for automatic theorem proving in such theories. Several examples are considered, including a toy concurrent language, for which non-trivial properties may be automatically proved.