Skip Navigation

Journal of Logic and Computation 1993 3(3):269-285; doi:10.1093/logcom/3.3.269
© 1993 by Oxford University Press
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by HIROKAWA, S.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Original Articles

The Relevance Graph of a BCK-Formula

SACHIO HIROKAWA

Department of Computer Science, College of General Education, Kyushu University Ropponmatsu 4-2-1, Fukuoka 810, Japan.E-mail: hirokawa{at}ec.kyushu-u.ac.jp

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-{lambda}-terms. This paper shows a characterization of the set pts(BCK-ß) of principal type-schemes of BCK-{lambda}-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 {alpha} iff {alpha} contains a negative occurrence of a subtype of the form (... -> b) -> ... -> c. The relevance graph G({alpha}) of the type {alpha} 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 {alpha} is in pts(BCK-ß) iff {alpha} 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({alpha}) whose nodes are positive type variables of {alpha} is a tree whose root is the rightmost type variable in {alpha}; (c) each positive type variable in a subtype {gamma} is relevant to the right-most type variable in {gamma}.

Keywords: Typed lambda-calculus; principal types; condensed detachment; BCK-logic.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.