Confluence of Curried Term-Rewriting Systems

Term rewriting systems operate on first-order terms. Presenting such terms in curried form is usually regarded as a trivial change of notation. However, in the absence of a type-discipline, or in the presence of a more powerful type-discipline than simply typed λ-calculus, the change is not as trivial as one might first think. It is shown that currying preserves confluence of arbitrary term rewriting systems. The structure of the proof is similar to Toyamaʹs proof that confluence is a modular property of TRS.