Document Open Access Logo

On Undefined and Meaningless in Lambda Definability

Author Fer-Jan de Vries

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.18.pdf
  • Filesize: 0.49 MB
  • 15 pages

Document Identifiers

Author Details

Fer-Jan de Vries

Cite As Get 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) https://doi.org/10.4230/LIPIcs.FSCD.2016.18

Abstract

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.

Subject Classification

Keywords
  • lambda calculus
  • lambda definability
  • partial recursive function
  • undefined term
  • meaningless term

Metrics

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

References

  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
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact