A combination of many-sorted algebraic term rewriting systems and polymorphic lambda term rewriting is studied in this paper. The results show that some important properties of algebraic systems are preserved when algebraic rewriting and polymorphic lambda-term rewriting are combined.

Given a set R of rewriting rules between algebraic &Sgr;-terms, if R is strong normalizing on algebraic &Sgr;-terms, then R+&bgr;+&eegr;+(type-&bgr;)+(type-&eegr;) rewriting of mixed terms is also strong normalizing. This result is obtained using a technique that nicely extends Girard’s reducibility candidates, which were introduced in the original proof of strong normalization for the polymorphic lambda calculus. The authors conclude by considering some directions for future research.