Termination of curryfied rewrite systems

Abstract

This paper studies termination of curryfied term rewriting systems (CTRSs), where functional values are introduced by "partial application". The limitations of syntactic simplification orderings for such systems are discussed. A proof method is proposed, based on three techniques: 1) Requirements on stability and monotonicity are relaxed. 2) Variables and inner function symbols of (potentially) functional types are allowed to contribute in the underlying precedence. 3) A standard polymorphic type system is refined so as to express non-functional polymorphism. Founded on this method, the curryfied path ordering with status (CPOS) is introduced. CPOS coincides with the recursive path ordering with status on first-order terms, and is comparable in strength to other approaches for higher-order rewrite systems, but also allows for polymorphism. Under mild restrictions on the underlying precedence, the so called curry rules are oriented correctly under CPOS.