The converse principal type-scheme theorem in lambda calculus (Q1194107)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The converse principal type-scheme theorem in lambda calculus |
scientific article |
Statements
The converse principal type-scheme theorem in lambda calculus (English)
0 references
27 September 1992
0 references
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.
0 references
converse principal type-scheme theorem
0 references
\(\lambda\)-calculus
0 references
principal type-assignment figures
0 references
adjoint terms
0 references
BCIW-\(\lambda\)-terms
0 references