The converse principal type-scheme theorem in lambda calculus

Sachio Hirokawa

    Research output: Contribution to journalArticlepeer-review

    2 Citations (Scopus)

    Abstract

    A principal type-scheme of a λ-term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc.146 (1969) 29-60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term. This paper shows a simple proof for the theorem in λ-calculus, by constructing an algorithm which transforms a type assignment to a λ-term into a principal type assignment to another λ-term that has the type as its principal type-scheme. The clearness of the algorithm is due to the characterization theorem of principal type-assignment figures. The algorithm is applicable to BCIW-λ-terms as well. Thus a uniform proof is presented for the converse principal type-scheme theorem for general λ-terms and BCIW-λ-terms.

    Original languageEnglish
    Pages (from-to)83-95
    Number of pages13
    JournalStudia Logica
    Volume51
    Issue number1
    DOIs
    Publication statusPublished - Mar 1 1992

    All Science Journal Classification (ASJC) codes

    • Logic
    • History and Philosophy of Science

    Fingerprint Dive into the research topics of 'The converse principal type-scheme theorem in lambda calculus'. Together they form a unique fingerprint.

    Cite this