Skip to main content
SpringerLink
Log in

A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms

  • Conference paper
  • First Online:
Logic-Based Program Synthesis and Transformation (LOPSTR 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10184))

Abstract

Contrary to several other families of lambda terms, no closed formula or generating function is known and none of the sophisticated techniques devised in analytic combinatorics can currently help with counting or generating the set of simply-typed closed lambda terms of a given size.

Moreover, their asymptotic scarcity among the set of closed lambda terms makes counting them via brute force generation and type inference quickly intractable, with previous published work showing counts for them only up to size 10.

By taking advantage of the synergy between logic variables, unification with occurs check and efficient backtracking in today’s Prolog systems, we climb 4 orders of magnitude above previously known counts by deriving progressively faster Horn Clause programs that generate and/or count the set of closed simply-typed lambda terms of sizes up to 14. A similar count for closed simply-typed normal forms is also derived up to size 14.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Barendregt, H.P.: The Lambda Calculus its Syntax and Semantics. Revised edn. vol. 103. North Holland (1984)

    Google Scholar 

  2. Hindley, J.R., Seldin, J.P.: Lambda-Calculus and Combinators: An Introduction. vol. 13. Cambridge University Press, Cambridge (2008)

    Google Scholar 

  3. Barendregt, H.P.: Lambda calculi with types. In: Handbook of Logic in Computer Science, vol. 2. Oxford University Press (1991)

    Google Scholar 

  4. Palka, M.H., Claessen, K., Russo, A., Hughes, J.: Testing an optimising compiler by generating random lambda terms. In: Proceedings of the 6th International Workshop on Automation of Software Test, AST 2011, pp. 91–97. ACM, New York (2011)

    Google Scholar 

  5. Grygiel, K., Lescanne, P.: Counting and generating lambda terms. J. Funct. Program. 23(5), 594–628 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  6. David, R., Raffalli, C., Theyssier, G., Grygiel, K., Kozik, J., Zaionc, M.: Some properties of random lambda terms. Logical Methods Comput. Sci. 9(1) (2009)

    Google Scholar 

  7. Bodini, O., Gardy, D., Gittenberger, B.: Lambda-terms of bounded unary height. In: ANALCO, SIAM, pp. 23–32 (2011)

    Google Scholar 

  8. David, R., Grygiel, K., Kozik, J., Raffalli, C., Theyssier, G., Zaionc, M.: Asymptotically almost all \(\lambda \)-terms are strongly normalizing. Preprint: arXiv: math. LO/0903.5505 v3 (2010)

  9. Flajolet, P., Sedgewick, R.: Analytic Combinatorics, 1st edn. Cambridge University Press, New York (2009)

    Book  MATH  Google Scholar 

  10. Sloane, N.J.A.: The On-Line Encyclopedia of Integer Sequences. (2014) Published electronically at https://oeis.org/

  11. Tarau, P.: On logic programming representations of lambda terms: de bruijn indices, compression, type inference, combinatorial generation, normalization. In: Pontelli, E., Son, T.C. (eds.) PADL 2015. LNCS, vol. 9131, pp. 115–131. Springer, Cham (2015). doi:10.1007/978-3-319-19686-2_9

    Chapter  Google Scholar 

  12. Tarau, P.: Ranking/unranking of lambda terms with compressed de bruijn indices. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 118–133. Springer, Cham (2015). doi:10.1007/978-3-319-20615-8_8

    Chapter  Google Scholar 

  13. Tarau, P.: On a uniform representation of combinators, arithmetic, lambda terms and types. In: Albert, E. (ed.) PPDP’15: Proceedings of the 17th international ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, pp. 244–255. ACM, New York (2015)

    Google Scholar 

  14. Tarau, P.: On type-directed generation of lambda terms. In: De Vos, M., Eiter, T., Lierler, Y., Toni, F. (eds.) 31st International Conference on Logic Programming (ICLP 2015), Technical Communications, Cork, Ireland, CEUR available online at September 2015 http://ceur-ws.org/Vol-1433/

  15. Tarau, P.: A logic programming playground for lambda terms, combinators, types and tree-based arithmetic computations. CoRR abs/1507.06944 (2015)

    Google Scholar 

  16. Stanley, R.P.: Enumerative Combinatorics. Wadsworth Publ. Co., Belmont (1986)

    Book  MATH  Google Scholar 

  17. Statman, R.: Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci. 9, 67–72 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  18. Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-Prolog. Theory Pract. Logic Program. 12, 67–96 (2012)

    Google Scholar 

  19. Costa, V.S., Rocha, R., Damas, L.: The YAP Prolog system. Theory and Practice of Logic Programming 12, 5–34 (2012)

    Google Scholar 

  20. Grygiel, K., Lescanne, P.: Counting and generating terms in the binary lambda calculus. J. Funct. Program. 25 (2015)

    Google Scholar 

  21. Bendkowski, M., Grygiel, K., Lescanne, P., Zaionc, M.: A natural counting of lambda terms. In: Freivalds, R.M., Engels, G., Catania, B. (eds.) SOFSEM 2016. LNCS, vol. 9587, pp. 183–194. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49192-8_15

    Chapter  Google Scholar 

  22. Lescanne, P.: Boltzmann samplers for random generation of lambda terms. CoRR abs/1404.3875 (2014)

    Google Scholar 

  23. Fetscher, B., Claessen, K., Pałka, M., Hughes, J., Findler, R.B.: Making random judgments: automatically generating well-typed terms from the definition of a type-system. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 383–405. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46669-8_16

    Chapter  Google Scholar 

  24. Genitrini, A., Kozik, J., Zaionc, M.: Intuitionistic vs. classical tautologies, quantitative comparison. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 100–109. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68103-8_7

    Chapter  Google Scholar 

  25. Fioravanti, F., Proietti, M., Senni, V.: Efficient generation of test data structures using constraint logic programming and program transformation. J. Logic Comput. 25(6), 1263–1283 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  26. Kuraj, I., Kuncak, V., Jackson, D.: Programming with enumerable sets of structures. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pp. 37–56. ACM, New York (2015)

    Google Scholar 

Download references

Acknowledgement

This research has been supported by NSF grant 1423324.

We thank the anonymous reviewers of LOPSTR’16 for their constructive suggestions and the participants of the 9th Workshop Computational Logic and Applications (https://cla.tcs.uj.edu.pl/) for enlightening discussions and for sharing various techniques clarifying the challenges one faces when having a fresh look at the emerging, interdisciplinary field of the combinatorics of lambda terms and their applications.

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, University of North Texas, Denton, USA

    Paul Tarau

Authors
  1. Paul Tarau
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Paul Tarau .

Editor information

Editors and Affiliations

  1. IMDEA Software Institute and Universidad Politécnica de Madrid, Madrid, Spain

    Manuel V Hermenegildo

  2. IMDEA Software Institute and CSIC, Madrid, Spain

    Pedro Lopez-Garcia

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Tarau, P. (2017). A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms. In: Hermenegildo, M., Lopez-Garcia, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2016. Lecture Notes in Computer Science(), vol 10184. Springer, Cham. https://doi.org/10.1007/978-3-319-63139-4_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63139-4_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63138-7

  • Online ISBN: 978-3-319-63139-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation