Finite Combinatory Logic with Intersection Types

  • Jakob Rehof
  • Paweł Urzyczyn
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)


Combinatory logic is based on modus ponens and a schematic (polymorphic) interpretation of axioms. In this paper we propose to consider expressive combinatory logics under the restriction that axioms are not interpreted schematically but ,,literally”, corresponding to a monomorphic interpretation of types. We thereby arrive at finite combinatory logic, which is strictly finitely axiomatisable and based solely on modus ponens. We show that the provability (inhabitation) problem for finite combinatory logic with intersection types is Exptime-complete with or without subtyping. This result contrasts with the general case, where inhabitation is known to be Expspace-complete in rank 2 and undecidable for rank 3 and up. As a by-product of the considerations in the presence of subtyping, we show that standard intersection type subtyping is in Ptime. From an application standpoint, we can consider intersection types as an expressive specification formalism for which our results show that functional composition synthesis can be automated.


Intersection Type Turing Machine Recursive Call Combinatory Logic Inhabitation Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic 48(4), 931–940 (1983)CrossRefzbMATHGoogle Scholar
  2. 2.
    Ben-Yelles, C.: Type Assignment in the Lambda-Calculus: Syntax and Semantics. PhD thesis, Department of Pure Mathematics, University College of Swansea (September 1979)Google Scholar
  3. 3.
    Coppo, M., Dezani-Ciancaglini, M.: An extension of basic functionality theory for lambda-calculus. Notre Dame Journal of Formal Logic 21, 685–693 (1980)CrossRefzbMATHGoogle Scholar
  4. 4.
    Dezani-Ciancaglini, M., Hindley, J.R.: Intersection types for combinatory logic. Theoretical Computer Science 100(2), 303–324 (1992)CrossRefzbMATHGoogle Scholar
  5. 5.
    Comon, H., et al.: Tree Automata Techniques and Applications (2008),
  6. 6.
    Hindley, J.R.: The simple semantics for Coppo-Dezani-Sallé types. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol. 137, pp. 212–226. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  7. 7.
    Kobayashi, N., Luke Ong, C.-H.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: LICS, pp. 179–188. IEEE Computer Society, Los Alamitos (2009)Google Scholar
  8. 8.
    Kozik, M.: A finite set of functions with an Exptime-complete composition problem. Theoretical Computer Science 407, 330–341 (2008)CrossRefzbMATHGoogle Scholar
  9. 9.
    Kurata, T., Takahashi, M.: Decidable properties of intersection type systems. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 297–311. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  10. 10.
    Kuśmierek, D.: The inhabitation problem for rank two intersection types. In: Ronchi Della Rocca, S. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 240–254. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  11. 11.
    Leivant, D.: Polymorphic type inference. In: Proc. 10th ACM Symp. on Principles of Programming Languages, pp. 88–98. ACM, New York (1983)Google Scholar
  12. 12.
    Lustig, Y., Vardi, M.Y.: Synthesis from component libraries. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 395–409. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  13. 13.
    Naik, M., Palsberg, J.: A type system equivalent to a model checker. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 374–388. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. 14.
    Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)zbMATHGoogle Scholar
  15. 15.
    Pottinger, G.: A type assignment for the strongly normalizable lambda-terms. In: Hindley, J., Seldin, J. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561–577. Academic Press, London (1980)Google Scholar
  16. 16.
    Rehof, J., Urzyczyn, P.: Finite combinatory logic with intersection types. Technical Report 834, Dept. of Computer Science, Technical University of Dortmund (2011),
  17. 17.
    Salvati, S.: Recognizability in the simply typed lambda-calculus. In: Ono, H., Kanazawa, M., de Queiroz, R. (eds.) WoLLIC 2009. LNCS, vol. 5514, pp. 48–60. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  18. 18.
    Urzyczyn, P.: The emptiness problem for intersection types. Journal of Symbolic Logic 64(3), 1195–1215 (1999)CrossRefzbMATHGoogle Scholar
  19. 19.
    Urzyczyn, P.: Inhabitation of low-rank intersection types. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 356–370. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  20. 20.
    Urzyczyn, P.: The logic of persistent intersection. Fundamenta Informaticae 103, 303–322 (2010)zbMATHGoogle Scholar
  21. 21.
    Venneri, B.: Intersection types as logical formulae. Journal of Logic and Computation 4(2), 109–124 (1994)CrossRefzbMATHGoogle Scholar
  22. 22.
    Wells, J.B., Yakobowski, B.: Graph-based proof counting and enumeration with applications for program fragment synthesis. In: Etalle, S. (ed.) LOPSTR 2004. LNCS, vol. 3573, pp. 262–277. Springer, Heidelberg (2005)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Jakob Rehof
    • 1
  • Paweł Urzyczyn
    • 2
  1. 1.Department of Computer ScienceTechnical University of DortmundGermany
  2. 2.Institute of InformaticsUniversity of WarsawPoland

Personalised recommendations