When are Two Rewrite Systems More than None?

It is important for programs to have modular correctness properties. We look at non-deterministic programs expressed as termrewriting systems which compute normal forms of input terms and consider the case where individual systems share constructors, but not de ned symbols. We present some old and new su cient conditions under which termination existence of normal forms, regardless of computation strategy and con uence uniqueness are preserved by such combinations.

• Type: Conference
• Year: 1997
• Where: MFCS
• Authors: Nachum Dershowitz
• Keywords: Compute Normal Forms, MFCS 1997, Modular Correctness Properties, Normal Forms, Theoretical Computer Science