Principal types of BCK-lambda-terms

Sachio Hirokawa

Research output: Contribution to journalArticle

14 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)253-276
Number of pages24
JournalTheoretical Computer Science
Volume107
Issue number2
DOIs
Publication statusPublished - Jan 18 1993

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Principal types of BCK-lambda-terms'. Together they form a unique fingerprint.

  • Cite this