Principal type-schemes of BCI-lambda-terms

Sachio Hirokawa

    研究成果: 書籍/レポート タイプへの寄稿会議への寄与

    5 被引用数 (Scopus)


    A BCI-λ-term is a λ-term in which each variable occurs exactly once. It represents a proof figure for implicational formula provable in linear logic. A principal type-scheme is a most general type to the term with respect to substitution. The notion of “relevance relation” is introduced for type-variables in a type. Intuitively an occurrence of a type-variable b is relevant to other occurrence of some type-variable c in a type α, when b is essentially concerned with the deduction of c in α. This relation defines a directed graph G(α) for type-variables in the type. We prove that a type a is a principal type-scheme of BCI-λ-term iff (a), (b) and (c) holds: (a) Each variable occurring in α occurs exactly twice and the occurrences have opposite sign. (b) G(α) is a tree and the right-most type variable in α is its root. (c) For any subtype γ of α, each type variable in γ is relevant to the right-most type variable in γ. A type-schemes of some BCI-λ-term is minimal iff it is not a non-trivial substitution instance of other type-scheme of BCI-λ-term. We prove that the set of BCI-minimal types coincides with the set of principal type-schemes of BCI-λ-terms in βη-normal form.

    ホスト出版物のタイトルTheoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings
    編集者Albert R. Meyer, Takayasu Ito
    出版社Springer Verlag
    出版ステータス出版済み - 1月 1 1991
    イベント1st International Conference on Theoretical Aspects of Computer Software, TACS 1991 - Sendai, 日本
    継続期間: 9月 24 19919月 27 1991


    名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    526 LNCS


    その他1st International Conference on Theoretical Aspects of Computer Software, TACS 1991

    !!!All Science Journal Classification (ASJC) codes

    • 理論的コンピュータサイエンス
    • コンピュータ サイエンス(全般)


    「Principal type-schemes of BCI-lambda-terms」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。