Skip to main content
SpringerLink
Log in

The converse principal type-scheme theorem in lambda calculus

  • Published:
Studia Logica Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Bunder, M.W., Meyer, R.K., A result for combinators, BCK-logics and BCK-algebras, Logique et Analyse 109 (1985), pp. 33–40.

    Google Scholar 

  2. Hindley, J.R., The principal type-scheme of an object in combinatory logic, Trans. Amer. Math. Soc. 146 (1969), pp. 29–60.

    Google Scholar 

  3. Hindley, J.R. Seldin, J.P., Introduction to Combinators and Lambda-Calculus, Cambridge University Press, London, 1986.

    Google Scholar 

  4. Hindley, J.R., The Meyer-Bunder theorem: Every inhabited type is a P.T.S. in BB'IW-combinatory logic, Manuscript 1989.

  5. Hindley, J.R., Meredith, D., Principal type-schemes and condensed detachment, J. Symbolic Logic 50 (1990), pp. 90–105.

    Google Scholar 

  6. Hirokawa, S., Principal types of BCK-lambda terms, Theoret. Comput. Sci. (to appear).

  7. Hirokawa, S., Principal type assignment to lambda terms, International Journal of Foundation of Computer Science 2 (1991), pp. 149–162.

    Google Scholar 

  8. Howard, W.A., The formulae-as-types notion of construction, in: Hindley and Seldin (eds.), To H.B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, pp. 479–490.

  9. Meyer,R.K., Bunder,M.W., Condensed detachment and combinators, Journal of Automated Reasoning (to appear).

  10. Mints, G.E., Tammet, T., Condensed detachment is complete for relevant logic: proof using computer, Journal of Automated Reasoning (to appear).

  11. Trigg, P., Abstraction using B,B' and friends, Manuscript 1989.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science College of General Education, Kyushu University, Ropponmatsu, 810, Fukuoka, Japan

    Sachio Hirokawa

Authors
  1. Sachio Hirokawa
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Hirokawa, S. The converse principal type-scheme theorem in lambda calculus. Studia Logica 51, 83–95 (1992). https://doi.org/10.1007/BF00370332

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00370332

Keywords

Search

Navigation