On Undefined and Meaningless in Lambda Definability

Author Fer-Jan de Vries

Thumbnail PDF


  • Filesize: 0.49 MB
  • 15 pages

Document Identifiers

Author Details

Fer-Jan de Vries

Cite AsGet BibTex

Fer-Jan de Vries. On Undefined and Meaningless in Lambda Definability. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


We distinguish between undefined terms as used in lambda definability of partial recursive functions and meaningless terms as used in infinite lambda calculus for the infinitary terms models that generalise the Bohm model. While there are uncountable many known sets of meaningless terms, there are four known sets of undefined terms. Two of these four are sets of meaningless terms. In this paper we first present set of sufficient conditions for a set of lambda terms to serve as set of undefined terms in lambda definability of partial functions. The four known sets of undefined terms satisfy these conditions. Next we locate the smallest set of meaningless terms satisfying these conditions. This set sits very low in the lattice of all sets of meaningless terms. Any larger set of meaningless terms than this smallest set is a set of undefined terms. Thus we find uncountably many new sets of undefined terms. As an unexpected bonus of our careful analysis of lambda definability we obtain a natural modification, strict lambda-definability, which allows for a Barendregt style of proof in which the representation of composition is truly the composition of representations.
  • lambda calculus
  • lambda definability
  • partial recursive function
  • undefined term
  • meaningless term


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. H. P. Barendregt. Some extensional term models for combinatory logics and λ-calculi. PhD thesis, Univ. Utrecht, 1971. Google Scholar
  2. H. P. Barendregt. A global representation of the recursive functions in the lambda-calculus. Theor. Comput. Sci., 3(2):225-242, 1976. URL: http://dx.doi.org/10.1016/0304-3975(76)90025-6.
  3. H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, Revised edition, 1984. Google Scholar
  4. H.P. Barendregt. Solvability in lambda calculi. In M. Guillaume, editor, Colloque international de logique: Clermont-Ferrand, 1975, pages 209-219. Éditions du C.N.R.S., 1977. Google Scholar
  5. H.P. Barendregt. Representing `undefined' in lambda calculus. J. Funct. Program., 2(3):367-374, 1992. URL: http://dx.doi.org/10.1017/S0956796800000447.
  6. A. Berarducci. Infinite λ-calculus and non-sensible models. In Logic and algebra (Pontignano, 1994), pages 339-377. Dekker, New York, 1996. Google Scholar
  7. A. Berarducci and B. Intrigila. Church-Rosser lambda-theories, Infinite lambda-terms and consistency problems. In W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors, Logic: from Foundations to Applications, pages 33-58. Oxford Science Publications, 1996. URL: http://www.dm.unipi.it/~berardu/Art/1996Church/CRtheories.pdf.
  8. J. A. Bergstra and J. van de Pol. A calculus for four-valued sequential logic. Theor. Comput. Sci., 412(28):3122-3128, 2011. URL: http://dx.doi.org/10.1016/j.tcs.2011.02.035.
  9. A. Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2):345-363, 1936. Google Scholar
  10. A. Church. The Calculi of Lambda Conversion. Princeton University Press, 1941. Google Scholar
  11. H. B. Curry, J. R. Hindley, and J. P. Seldin. Combinatory Logic II. North-Holland, 1972. Google Scholar
  12. G. Jacopini and M. Venturini-Zilli. Easy terms in the lambda-calculus. Fundamenta Informaticae, VIII(2):225-233, 1985. Google Scholar
  13. J. R. Kennaway and F. J. de Vries. Infinitary rewriting. In Terese, editor, Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science, pages 668-711. Cambridge University Press, 2003. Google Scholar
  14. J. R. Kennaway, V. van Oostrom, and F. J. de Vries. Meaningless terms in rewriting. Journal of Functional and Logic Programming, 1999(1), 1999. URL: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-01/A99-01.html.
  15. S. C. Kleene. λ-definability and recursiveness. Duke Math. J., 2(2):340-353, 06 1936. URL: http://dx.doi.org/10.1215/S0012-7094-36-00227-2.
  16. S. C. Kleene. On notation for ordinal numbers. J. Symb. Log., 3(4):150-155, 1938. URL: http://dx.doi.org/10.2307/2267778.
  17. Beata Konikowska, Andrzej Tarlecki, and Andrzej Blikle. A three-valued logic for software specification and validation. Fundam. Inform., 14(4):411-453, 1991. Google Scholar
  18. G. Kreisel. Some reasons for generalising recursion theory. In R.O. Gandy and C.M.E. Yates, editors, Logic Colloquium 1969: proceedings of the summerschool and colloquium in mathematical logic, Manchester, August 1969, pages 139-189. North-Holland, 1971. Google Scholar
  19. P. Severi and F. J. de Vries. Order Structures for Böhm-like models. In Computer Science Logic, volume 3634 of LNCS, pages 103-116. Springer-Verlag, 2005. Google Scholar
  20. P. Severi and F. J. de Vries. Weakening the axiom of overlap in infinitary lambda calculus. In M. Schmidt-Schauß, editor, Proc. of the 22nd Int'l Conf. on Rewriting Techniques and Applications, May 30 - June 1, 2011, volume 10 of LIPIcs, pages 313-328. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2011.313.
  21. P. G. Severi and F. J. de Vries. Decomposing the lattice of meaningless sets in the infinitary lambda calculus. In L. D. Beklemishev and R. de Queiroz, editors, Proc. of the 18th Int'l Workshop on Logic, Language, Information and Computation (WoLLIC 2011), pages 210-227, 2011. URL: http://dx.doi.org/10.1007/978-3-642-20920-8_22.
  22. A. M. Turing. Computability and λ-definability. J. Symb. Log., 2(4):153-163, 1937. URL: http://dx.doi.org/10.2307/2268280.
  23. A. M. Turing. The frakp-function in λ-K-conversion. J. Symb. Log., 2(4):164, 1937. URL: http://dx.doi.org/10.2307/2268281.
  24. A. Visser. Numerations, λ-calculus &arithmetic. In J.R. Hindley and J.P. Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 259-284. Academic Press, 1980. Google Scholar