The converse principal type-scheme theorem in lambda calculus

Sachio Hirokawa

    研究成果: ジャーナルへの寄稿学術誌査読

    2 被引用数 (Scopus)

    抄録

    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.

    本文言語英語
    ページ(範囲)83-95
    ページ数13
    ジャーナルStudia Logica
    51
    1
    DOI
    出版ステータス出版済み - 3月 1 1992

    !!!All Science Journal Classification (ASJC) codes

    • 論理
    • 科学史および科学哲学

    フィンガープリント

    「The converse principal type-scheme theorem in lambda calculus」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

    引用スタイル