The converse principal type-scheme theorem in lambda calculus (Q1194107)

The converse principal type-scheme theorem states that every type-scheme of a term is a principal type-scheme of some term. It was first proved for combinatory terms by J. R. Hindley (1969). This paper shows a simple proof for the theorem in \(\lambda\)-calculus, by constructing an algorithm which transforms a type assignment to a \(\lambda\)-term into a principal type assignment to another \(\lambda\)-term that has the type as its principal type-scheme. The algorithm uses the characterization theorem of principal type-assignment figures and the notion of adjoint terms by the author [Int. J. Found. Comput. Sci. 2, 149-162 (1991; Zbl 0746.03012)]. It is shown that the algorithm is applicable to BCIW-\(\lambda\)-terms as well, so the theorem also holds for BCIW-\(\lambda\)-terms.