Unfolding of Programs with Nondeterminism

In LIsper: "Total Unfolding: Theory and Applications" some results were proved regarding properties of unfolding of purely functional programs. Especially, a theorem was shown that relates the termination of symbolic evaluation of a "less instantiated" term relative to the termination of a "more instantiated" term. An application is partial evaluation, where unfolding of function definitions is frequently performed to enable further simplifications of the resulting specialized program. The unfolding must then be kept under control to ensure that the partial evaluation terminates. In this paper, we extend the termination result from purely functional programs programs with nondeterministic operations. We give an operational semantics where the behaviour of operators is defined through rewrite rules: nondeterminism then occurs when the resulting term rewriting system is nonconfluent. For the confluent part, the previous termination results carry over. It is, however, not guaranteed in general that the resulting unfolded program has the same semantics as the original program. We give conditions on the rewrite rules that guarantee that both versions have the same semantics, and we show that they apply to a nontrivial class of nondeterministic languages