It is important for programs to have modular correctness properties. We look at non-deterministic programs expressed as term-rewriting systems (which compute normal forms of input terms) and consider the case where individual systems share constructors, but not defined symbols. We present some old and new sufficient conditions under which termination (existence of normal forms, regardless of computation strategy) and confluence (uniqueness) are preserved by such combinations.
This research was supported in part by the National Science Foundation under grants INT-95-07248 and CCR-97-00070 and was performed while on leave at the Hebrew University, Jerusalem, Israel and at École Normale Supérieure de Cachan, France.