The converse principal type-scheme theorem in lambda calculus

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

A principal type-scheme of a λ-term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc.146 (1969) 29-60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term. This paper shows a simple proof for the theorem in λ-calculus, by constructing an algorithm which transforms a type assignment to a λ-term into a principal type assignment to another λ-term that has the type as its principal type-scheme. The clearness of the algorithm is due to the characterization theorem of principal type-assignment figures. The algorithm is applicable to BCIW-λ-terms as well. Thus a uniform proof is presented for the converse principal type-scheme theorem for general λ-terms and BCIW-λ-terms.

Original languageEnglish
Pages (from-to)83-95
Number of pages13
JournalStudia Logica
Volume51
Issue number1
DOIs
Publication statusPublished - Mar 1 1992

Fingerprint

Lambda Calculus
Converse
Term
Theorem
Assignment
Characterization Theorem
Figure
Calculus
Transform
Logic

All Science Journal Classification (ASJC) codes

  • Logic
  • History and Philosophy of Science

Cite this

The converse principal type-scheme theorem in lambda calculus. / Hirokawa, Sachio.

In: Studia Logica, Vol. 51, No. 1, 01.03.1992, p. 83-95.

Research output: Contribution to journalArticle

@article{4ecd4b8ef84a4546a1ad7d5840dc01c8,
title = "The converse principal type-scheme theorem in lambda calculus",
abstract = "A principal type-scheme of a λ-term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc.146 (1969) 29-60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term. This paper shows a simple proof for the theorem in λ-calculus, by constructing an algorithm which transforms a type assignment to a λ-term into a principal type assignment to another λ-term that has the type as its principal type-scheme. The clearness of the algorithm is due to the characterization theorem of principal type-assignment figures. The algorithm is applicable to BCIW-λ-terms as well. Thus a uniform proof is presented for the converse principal type-scheme theorem for general λ-terms and BCIW-λ-terms.",
author = "Sachio Hirokawa",
year = "1992",
month = "3",
day = "1",
doi = "10.1007/BF00370332",
language = "English",
volume = "51",
pages = "83--95",
journal = "Studia Logica",
issn = "0039-3215",
publisher = "Springer Netherlands",
number = "1",

}

TY - JOUR

T1 - The converse principal type-scheme theorem in lambda calculus

AU - Hirokawa, Sachio

PY - 1992/3/1

Y1 - 1992/3/1

N2 - A principal type-scheme of a λ-term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc.146 (1969) 29-60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term. This paper shows a simple proof for the theorem in λ-calculus, by constructing an algorithm which transforms a type assignment to a λ-term into a principal type assignment to another λ-term that has the type as its principal type-scheme. The clearness of the algorithm is due to the characterization theorem of principal type-assignment figures. The algorithm is applicable to BCIW-λ-terms as well. Thus a uniform proof is presented for the converse principal type-scheme theorem for general λ-terms and BCIW-λ-terms.

AB - A principal type-scheme of a λ-term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc.146 (1969) 29-60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term. This paper shows a simple proof for the theorem in λ-calculus, by constructing an algorithm which transforms a type assignment to a λ-term into a principal type assignment to another λ-term that has the type as its principal type-scheme. The clearness of the algorithm is due to the characterization theorem of principal type-assignment figures. The algorithm is applicable to BCIW-λ-terms as well. Thus a uniform proof is presented for the converse principal type-scheme theorem for general λ-terms and BCIW-λ-terms.

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

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

U2 - 10.1007/BF00370332

DO - 10.1007/BF00370332

M3 - Article

AN - SCOPUS:0346873117

VL - 51

SP - 83

EP - 95

JO - Studia Logica

JF - Studia Logica

SN - 0039-3215

IS - 1

ER -