Termination of curryfied rewrite systems

Autor:	Bjørn Kristoffersen
Rok vydání:	1996
Předmět:	TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Theoretical computer science Path-ordering Computer science TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Partial application Monotonic function Rewriting Lambda calculus computer Principal type computer.programming_language
Zdroj:	Recent Trends in Data Type Specification ISBN: 9783540616290 COMPASS/ADT
DOI:	10.1007/3-540-61629-2_51
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::31e5fdff2f9e15139dee20452e50a174 https://doi.org/10.1007/3-540-61629-2_51 Zobrazit plný text záznamu