Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-25T07:05:00.022Z Has data issue: false hasContentIssue false

A characterization of lambda-terms transforming numerals

Published online by Cambridge University Press:  22 July 2016

PAWEŁ PARYS*
Affiliation:
Institute of Informatics, University of Warsaw, Warsaw, Poland (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

It is well known that simply typed λ-terms can be used to represent numbers, as well as some other data types. We show that λ-terms of each fixed (but possibly very complicated) type can be described by a finite piece of information (a set of appropriately defined intersection types) and by a vector of natural numbers. On the one hand, the description is compositional: having only the finite piece of information for two closed λ-terms M and N, we can determine its counterpart for MN, and a linear transformation that applied to the vectors of numbers for M and N gives us the vector for MN. On the other hand, when a λ-term represents a natural number, then this number is approximated by a number in the vector corresponding to this λ-term. As a consequence, we prove that in a λ-term of a fixed type, we can store only a fixed number of natural numbers, in such a way that they can be extracted using λ-terms. More precisely, while representing k numbers in a closed λ-term of some type, we only require that there are k closed λ-terms M1,. . .,Mk such that Mi takes as argument the λ-term representing the k-tuple, and returns the i-th number in the tuple (we do not require that, using λ-calculus, one can construct the representation of the k-tuple out of the k numbers in the tuple). Moreover, the same result holds when we allow that the numbers can be extracted approximately, up to some error (even when we only want to know whether a set is bounded or not). All the results remain true when we allow the Y combinator (recursion) in our λ-terms, as well as uninterpreted constants.

Type
Articles
Copyright
Copyright © Cambridge University Press 2016 

References

Barendregt, H., Dekkers, W. & Statman, R. (2013) Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press.Google Scholar
Clairambault, P. & Murawski, A. S. (2013) Böhm trees as higher-order recursive schemes. In IARCS annual conference on foundations of software technology and theoretical computer science, FSTTCS 2013, December 12–14, 2013, Guwahati, India. Seth, A. & Vishnoi, N. K. (eds), LIPIcs, vol. 24. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik.Google Scholar
Colcombet, T. (2013) Regular cost functions, part I: Logic and algebra over words. Log. Methods Comput. Sci. 9 (3:3), 147.Google Scholar
Kobayashi, N. (2013) Pumping by Typing. In Logic in Computer Science (Lics), 2013 28th Annual IEEE/ACM Symposium on, New Orleans, LA, 2013, pp. 398–407. doi: 10.1109/LICS.2013.46.CrossRefGoogle Scholar
Parys, P. (2012) On the Significance of the Collapse Operation. In Logic in Computer Science (Lics), 2012 27th Annual IEEE Symposium on, Dubrovnik, 2012, pp. 521–530. doi: 10.1109/LICS.2012.62.Google Scholar
Parys, P. (2014) How many numbers can a lambda-term contain? In Flops. Lecture Notes in Computer Science, Codish, M. & Sumii, E. (eds), vol. 8475. Springer.CrossRefGoogle Scholar
Schwichtenberg, H. (1976) Definierbare funktionen im lambda- kalkül mit typen. Arch. Logic Grundlagenforsch 17, 113114.Google Scholar
Statman, R. (1979) The typed lambda-calculus is not elementary recursive. Theor. Comput. Sci. 9 (1), 7381.CrossRefGoogle Scholar
Zaionc, M. (1987) Word operation definable in the typed lambda-calculus. Theor. Comput. Sci. 52 (1–2), 114.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.