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

From MaRDI portal
Revision as of 00:21, 22 February 2024 by RedirectionBot (talk | contribs) (‎Removed claim: reviewed by (P1447): Item:Q1055195)
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
    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

    Identifiers