Principal type-schemes of BCI-lambda-terms

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings
EditorsAlbert R. Meyer, Takayasu Ito
PublisherSpringer Verlag
Pages633-650
Number of pages18
ISBN (Print)9783540544159
DOIs
Publication statusPublished - Jan 1 1991
Event1st International Conference on Theoretical Aspects of Computer Software, TACS 1991 - Sendai, Japan
Duration: Sep 24 1991Sep 27 1991

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume526 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other1st International Conference on Theoretical Aspects of Computer Software, TACS 1991
CountryJapan
CitySendai
Period9/24/919/27/91

Fingerprint

Substitution reactions
Directed graphs
Term
Substitution
Linear Logic
Deduction
Directed Graph
Normal Form
Figure
Roots

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Hirokawa, S. (1991). Principal type-schemes of BCI-lambda-terms. In A. R. Meyer, & T. Ito (Eds.), Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings (pp. 633-650). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 526 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-54415-1_68

Principal type-schemes of BCI-lambda-terms. / Hirokawa, Sachio.

Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings. ed. / Albert R. Meyer; Takayasu Ito. Springer Verlag, 1991. p. 633-650 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 526 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Hirokawa, S 1991, Principal type-schemes of BCI-lambda-terms. in AR Meyer & T Ito (eds), Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 526 LNCS, Springer Verlag, pp. 633-650, 1st International Conference on Theoretical Aspects of Computer Software, TACS 1991, Sendai, Japan, 9/24/91. https://doi.org/10.1007/3-540-54415-1_68
Hirokawa S. Principal type-schemes of BCI-lambda-terms. In Meyer AR, Ito T, editors, Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings. Springer Verlag. 1991. p. 633-650. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-54415-1_68
Hirokawa, Sachio. / Principal type-schemes of BCI-lambda-terms. Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings. editor / Albert R. Meyer ; Takayasu Ito. Springer Verlag, 1991. pp. 633-650 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{39f414701a2e491ab00a3bbead0b32b1,
title = "Principal type-schemes of BCI-lambda-terms",
abstract = "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.",
author = "Sachio Hirokawa",
year = "1991",
month = "1",
day = "1",
doi = "10.1007/3-540-54415-1_68",
language = "English",
isbn = "9783540544159",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "633--650",
editor = "Meyer, {Albert R.} and Takayasu Ito",
booktitle = "Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Principal type-schemes of BCI-lambda-terms

AU - Hirokawa, Sachio

PY - 1991/1/1

Y1 - 1991/1/1

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

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

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

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

U2 - 10.1007/3-540-54415-1_68

DO - 10.1007/3-540-54415-1_68

M3 - Conference contribution

AN - SCOPUS:84972503586

SN - 9783540544159

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 633

EP - 650

BT - Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings

A2 - Meyer, Albert R.

A2 - Ito, Takayasu

PB - Springer Verlag

ER -