Principal type-schemes of BCI-lambda-terms

Sachio Hirokawa

    研究成果: Chapter in Book/Report/Conference proceedingConference contribution

    4 被引用数 (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
    ページ633-650
    ページ数18
    ISBN(印刷版)9783540544159
    DOI
    出版ステータス出版済み - 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
    ISSN(印刷版)0302-9743
    ISSN(電子版)1611-3349

    その他

    その他1st International Conference on Theoretical Aspects of Computer Software, TACS 1991
    国/地域日本
    CitySendai
    Period9/24/919/27/91

    All Science Journal Classification (ASJC) codes

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

    フィンガープリント

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

    引用スタイル