@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 = jan,

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",

note = "1st International Conference on Theoretical Aspects of Computer Software, TACS 1991 ; Conference date: 24-09-1991 Through 27-09-1991",

}