J Symbolic Computation Conuence of Curried TermRewriting Systems

Term rewriting systems operate on rstorder terms Presenting such terms in curried form is usually regarded as a trivial change of notation However in the absence of a typediscipline or in the presence of a more powerful typediscipline than simply typed calculus the change is not as trivial as one might rst think It is shown that currying preserves conuence of arbitrary term rewriting systems The structure of the proof is similar to Toyamas proof that conuence is a modular property of TR