The converse principal type-scheme theorem in lambda calculus (Q1194107): Difference between revisions

From MaRDI portal
RedirectionBot (talk | contribs)
Changed an Item
ReferenceBot (talk | contribs)
Changed an Item
 
(One intermediate revision by one other user not shown)
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3691634 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Principal Type-Scheme of an Object in Combinatory Logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4722037 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Principal type-schemes and condensed detachment / rank
 
Normal rank
Property / cites work
 
Property / cites work: Principal types of BCK-lambda-terms / rank
 
Normal rank
Property / cites work
 
Property / cites work: PRINCIPAL TYPE ASSIGNMENT TO LAMBDA TERMS / rank
 
Normal rank
Property / cites work
 
Property / cites work: Condensed detachment is complete for relevance logic: A computer-aided proof / rank
 
Normal rank

Latest revision as of 12:05, 16 May 2024

scientific article
Language Label Description Also known as
English
The converse principal type-scheme theorem in lambda calculus
scientific article

    Statements

    The converse principal type-scheme theorem in lambda calculus (English)
    0 references
    0 references
    27 September 1992
    0 references
    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.
    0 references
    converse principal type-scheme theorem
    0 references
    \(\lambda\)-calculus
    0 references
    principal type-assignment figures
    0 references
    adjoint terms
    0 references
    BCIW-\(\lambda\)-terms
    0 references
    0 references

    Identifiers