The relevance graph of a BCK-formula

Sachio Hirokawa

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

2 被引用数 (Scopus)


It is known that the set of BCK-formulas which is provable by the detachment rule of Meredith is identical to the set pts(BCK) of principal type-schemes of BCK-λ-terms. This paper shows a characterization of the set pts(BCK-β) of principal type-schemes of BCK-λ-terms in β-normal form. To characterize the set pts(BCK), a 'relevance relation' is defined between type variables in a type. A type variable b is relevant to a type variable c in a type α iff α contains a negative occurrence of a subtype of the form (... → b) → ... → c. The relevance graph G(α) of the type α is the directed graph induced by this relevance relation. A type variable is said to be positive iff it occurs in a positive position and negative otherwise. It is proved that a type α is in pts(BCK-β) iff α satisfies: (a) every type variable occurs exactly once in a negative position and at most once in a positive position; (b) no negative type variable is relevant to any type variable but itself and the subgraph of G(α) whose nodes are positive type variables of α is a tree whose root is the rightmost type variable in α; (c) each positive type variable in a subtype γ is relevant to the right-most type variable in γ.

ジャーナルJournal of Logic and Computation
出版ステータス出版済み - 6月 1993

!!!All Science Journal Classification (ASJC) codes

  • 理論的コンピュータサイエンス
  • ソフトウェア
  • 人文科学(その他)
  • ハードウェアとアーキテクチャ
  • 論理


「The relevance graph of a BCK-formula」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。