The converse principal type-scheme theorem in lambda calculus
type: Item
instance of: scholarly article
title: The converse principal type-scheme theorem in lambda calculus
zbMATH Open document ID: 0786.03014
DOI: 10.1007/BF00370332
author: Sachio Hirokawa
published in: Studia Logica
publication date: 1992-09-27T00:00:00Z
review text: The converse principal type-scheme theorem states that every type-scheme of a term is a principal type-scheme of some term. It was first proved for combinatory terms by J. R. Hindley (1969). This paper shows a simple proof for the theorem in \(\lambda\)-calculus, by constructing an algorithm which transforms a type assignment to a \(\lambda\)-term into a principal type assignment to another \(\lambda\)-term that has the type as its principal type-scheme. The algorithm uses the characterization theorem of principal type-assignment figures and the notion of adjoint terms by the author [Int. J. Found. Comput. Sci. 2, 149-162 (1991; Zbl 0746.03012)]. It is shown that the algorithm is applicable to BCIW-\(\lambda\)-terms as well, so the theorem also holds for BCIW-\(\lambda\)-terms.
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 63834
zbMATH Keywords: converse principal type-scheme theorem
zbMATH Keywords: \(\lambda\)-calculus
zbMATH Keywords: principal type-assignment figures
zbMATH Keywords: adjoint terms
zbMATH Keywords: BCIW-\(\lambda\)-terms
reviewed by: Teruo Hikita
MaRDI profile type: Publication
cites work: Q3691634
cites work: The Principal Type-Scheme of an Object in Combinatory Logic
cites work: Q4722037
cites work: Principal type-schemes and condensed detachment
cites work: Principal types of BCK-lambda-terms
cites work: PRINCIPAL TYPE ASSIGNMENT TO LAMBDA TERMS
cites work: Condensed detachment is complete for relevance logic: A computer-aided proof
description: scientific article; zbMATH DE number 63834