A source of inconsistency in theories of nondeterministic functions

Nondeterminacy is a useful feature of specification languages because it allows the customer to express that any of a range of outcomes is acceptable for a particular operation. However, the classical theory of functions becomes considerably complicated and counter-intuitive in the presence of nondeterminacy, and inconsistencies can easily creep in. All this is well known. In this paper, we describe a potential new source of inconsistency when functions and nondeterminacy are combined. We show that some existing theories fall foul of it, and show how to avoid it. The root cause of the problem is the substitution of a variable in a nonmonotonic position when the type of the variable is nonflat.