Hostname: page-component-74656f9884-j7cmm Total loading time: 0 Render date: 2026-11-10T12:07:14.889Z Has data issue: false hasContentIssue false
  • English
  • Français

Lambda theories allowing terms with a finite number of fixed points

Published online by Cambridge University Press:  29 July 2015

BENEDETTO INTRIGILA  and
RICHARD STATMAN
BENEDETTO INTRIGILA
Affiliation:
Dipartimento di Ingegneria dell'Impresa, Università di Roma ‘Tor Vergata,’ Rome, Italy
RICHARD STATMAN
Affiliation:
Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA
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.

A natural question in the λ-calculus asks what is the possible number of fixed points of a combinator (closed term). A complete answer to this question is still missing (Problem 25 of TLCA Open Problems List) and we investigate the related question about the number of fixed points of a combinator in λ-theories. We show the existence of a recursively enumerable lambda theory where the number is always one or infinite. We also show that there are λ-theories such that some terms have only two fixed points. In a first example, this is obtained by means of a non-constructive (more precisely non-r.e.) λ-theory where the range property is violated. A second, more complex example of a non-r.e. λ-theory (with a higher unsolvability degree) shows that some terms can have only two fixed points while the range property holds for every term.

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 27 , Issue 3 , March 2017 , pp. 405 - 427
Copyright
Copyright © Cambridge University Press 2015 

References

Barendregt, H.P. (1984). The Lambda Calculus. Its Syntax and Semantics, North-Holland, Amsterdam, The Netherlands.Google Scholar
Barendregt, H.P. (1993). Constructive proofs of the range property in lambda calculus. Theoretical Computer Science 121 (1–2) 59–69.CrossRefGoogle Scholar
Bezem, M., Klop, J.W. and de Vrijer, R. (eds.) (Terese). (2003). Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, volume 55, Cambridge University Press.Google Scholar
Intrigila, B. and Biasone, E. On the number of fixed points of a combinator in lambda calculus. Mathematical Structures in Computer Science 10 (5) 595–615.Google Scholar
Intrigila, B. and Statman, R. (2005). Some results on extensionality in lambda calculus. Annals of Pure and Applied Logic 132 (2–3) 109–125.Google Scholar
Polonsky, A. (2012). The range property fails for $\mathcal{H}$ . The Journal of Symbolic Logic 77 (4) 1195–1210. doi:10.2178/jsl.7704080.Google Scholar
Rogers, H. Jr. (1967). Theory of Recursive Functions and Effective Computability, MacGraw Hill, New York.Google Scholar
Statman, R. (1999). Morphisms and partitions of V-sets. In: Proceedings of the 12th International Workshop on Computer Science Logic, Springer-Verlag London, UK 178–193.Google Scholar
TLCA List of Open Problems (2014). Available at http://tlca.di.unito.it/opltlca/.Google Scholar