### Numbering matters:first-order canonical forms for second-order recursive typesNumbering matters:first-order canonical forms for second-order recursive types

Access Restriction
Subscribed

 Author Pottier, François ♦ Gauthier, Nadji Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data Subject Keyword Unification ♦ Recursive types ♦ Equality ♦ Polymorphism Abstract We study a type system equipped with universal types and equire-cursive types, which we refer to as F͘. We show that type equality may be decided in time O(nlog n), an improvement over the previous known bound of $O(n^{2}$ ). In fact, we show that two more general problems, namely entailment of type equations and type unification, may be decided in time O(nlog n), a new result. To achieve this bound, we associate, with every F͘ type, a first-order canonical form, which may be computed in time O(nlogn). By exploiting this notion, we reduce all three problems to equality and unification of first-order recursive terms, for which efficient algorithms are known. Description Affiliation: INRIA (Gauthier, Nadji; Pottier, François) Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 1983-05-01 Publisher Place New York Journal ACM SIGPLAN Notices (SIGP) Volume Number 39 Issue Number 9 Page Count 12 Starting Page 150 Ending Page 161

#### Open content in new tab

Source: ACM Digital Library