The relevance graph of a BCK-formula

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

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 γ.

Original languageEnglish
Pages (from-to)269-285
Number of pages17
JournalJournal of Logic and Computation
Volume3
Issue number3
DOIs
Publication statusPublished - Jun 1 1993

Fingerprint

Directed graphs
Graph in graph theory
Relevance
Graph
Term
Directed Graph
Normal Form
Subgraph
Roots

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Software
  • Arts and Humanities (miscellaneous)
  • Hardware and Architecture
  • Logic

Cite this

The relevance graph of a BCK-formula. / Hirokawa, Sachio.

In: Journal of Logic and Computation, Vol. 3, No. 3, 01.06.1993, p. 269-285.

Research output: Contribution to journalArticle

@article{e7a35527e9764e259cdda2c897d4df40,
title = "The relevance graph of a BCK-formula",
abstract = "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 γ.",
author = "Sachio Hirokawa",
year = "1993",
month = "6",
day = "1",
doi = "10.1093/logcom/3.3.269",
language = "English",
volume = "3",
pages = "269--285",
journal = "Journal of Logic and Computation",
issn = "0955-792X",
publisher = "Oxford University Press",
number = "3",

}

TY - JOUR

T1 - The relevance graph of a BCK-formula

AU - Hirokawa, Sachio

PY - 1993/6/1

Y1 - 1993/6/1

N2 - 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 γ.

AB - 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 γ.

UR - http://www.scopus.com/inward/record.url?scp=18944404237&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=18944404237&partnerID=8YFLogxK

U2 - 10.1093/logcom/3.3.269

DO - 10.1093/logcom/3.3.269

M3 - Article

AN - SCOPUS:18944404237

VL - 3

SP - 269

EP - 285

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

SN - 0955-792X

IS - 3

ER -