Principal types of BCK-lambda-terms

研究成果: ジャーナルへの寄稿記事

14 引用 (Scopus)

抄録

BCK-λ-terms are the λ-terms in which each variable occurs at most once. The principal type of a λ-term is the most general type of the term. In this paper we prove that if two BCK-λ-terms in β-normal form have the same principal type then they are identical. This solves the following problem (Y. Komori, 1987) in more general form: if two closed βη-normal form BCK-λ-terms are assigned to the same minimal BCK-formula, are they identical? A minimal BCK-formula is the most general formula among BCK-provable formulas with respect to substitutions for type variables. To analyze type assignment, the notion of "connection" is introduced. A connection is a series of occurrences of a type in a type assignment figure. Connected occurrences of a type have the same meaning. The occurrences of the type in distinct connection classes can be rewritten separately; as a result, we have more general type assignment. By "formulae-as-types" correspondence, the result implies the uniqueness of the normal proof figure for principal BCK-formulas. The result is valid for BCI-logic or implicational fragment of linear logic as well.

元の言語英語
ページ(範囲)253-276
ページ数24
ジャーナルTheoretical Computer Science
107
発行部数2
DOI
出版物ステータス出版済み - 1 18 1993

Fingerprint

Substitution reactions
Term
Assignment
Normal Form
Figure
Linear Logic
Substitution
Fragment
Correspondence
Uniqueness
Valid
Logic
Distinct
Imply
Closed
Series

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

これを引用

Principal types of BCK-lambda-terms. / Hirokawa, Sachio.

:: Theoretical Computer Science, 巻 107, 番号 2, 18.01.1993, p. 253-276.

研究成果: ジャーナルへの寄稿記事

@article{24d6d0bd73224e4f89e278aa1f12c3ba,
title = "Principal types of BCK-lambda-terms",
abstract = "BCK-λ-terms are the λ-terms in which each variable occurs at most once. The principal type of a λ-term is the most general type of the term. In this paper we prove that if two BCK-λ-terms in β-normal form have the same principal type then they are identical. This solves the following problem (Y. Komori, 1987) in more general form: if two closed βη-normal form BCK-λ-terms are assigned to the same minimal BCK-formula, are they identical? A minimal BCK-formula is the most general formula among BCK-provable formulas with respect to substitutions for type variables. To analyze type assignment, the notion of {"}connection{"} is introduced. A connection is a series of occurrences of a type in a type assignment figure. Connected occurrences of a type have the same meaning. The occurrences of the type in distinct connection classes can be rewritten separately; as a result, we have more general type assignment. By {"}formulae-as-types{"} correspondence, the result implies the uniqueness of the normal proof figure for principal BCK-formulas. The result is valid for BCI-logic or implicational fragment of linear logic as well.",
author = "Sachio Hirokawa",
year = "1993",
month = "1",
day = "18",
doi = "10.1016/0304-3975(93)90171-O",
language = "English",
volume = "107",
pages = "253--276",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "2",

}

TY - JOUR

T1 - Principal types of BCK-lambda-terms

AU - Hirokawa, Sachio

PY - 1993/1/18

Y1 - 1993/1/18

N2 - BCK-λ-terms are the λ-terms in which each variable occurs at most once. The principal type of a λ-term is the most general type of the term. In this paper we prove that if two BCK-λ-terms in β-normal form have the same principal type then they are identical. This solves the following problem (Y. Komori, 1987) in more general form: if two closed βη-normal form BCK-λ-terms are assigned to the same minimal BCK-formula, are they identical? A minimal BCK-formula is the most general formula among BCK-provable formulas with respect to substitutions for type variables. To analyze type assignment, the notion of "connection" is introduced. A connection is a series of occurrences of a type in a type assignment figure. Connected occurrences of a type have the same meaning. The occurrences of the type in distinct connection classes can be rewritten separately; as a result, we have more general type assignment. By "formulae-as-types" correspondence, the result implies the uniqueness of the normal proof figure for principal BCK-formulas. The result is valid for BCI-logic or implicational fragment of linear logic as well.

AB - BCK-λ-terms are the λ-terms in which each variable occurs at most once. The principal type of a λ-term is the most general type of the term. In this paper we prove that if two BCK-λ-terms in β-normal form have the same principal type then they are identical. This solves the following problem (Y. Komori, 1987) in more general form: if two closed βη-normal form BCK-λ-terms are assigned to the same minimal BCK-formula, are they identical? A minimal BCK-formula is the most general formula among BCK-provable formulas with respect to substitutions for type variables. To analyze type assignment, the notion of "connection" is introduced. A connection is a series of occurrences of a type in a type assignment figure. Connected occurrences of a type have the same meaning. The occurrences of the type in distinct connection classes can be rewritten separately; as a result, we have more general type assignment. By "formulae-as-types" correspondence, the result implies the uniqueness of the normal proof figure for principal BCK-formulas. The result is valid for BCI-logic or implicational fragment of linear logic as well.

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

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

U2 - 10.1016/0304-3975(93)90171-O

DO - 10.1016/0304-3975(93)90171-O

M3 - Article

AN - SCOPUS:38249005852

VL - 107

SP - 253

EP - 276

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 2

ER -