Fixed points in lambda calculus. An eccentric survey of problems and solutions

Abstract The fact that every combinator has a fixed point is at the heart of the λ -calculus as a model of computation. We consider several aspects of such phenomenon; our specific, perhaps eccentric, point of view focuses on problems and results that we consider worthy of further investigations. We first consider the relation with self application , in comparison with the opposite view, which stresses the role of coding , unifying the first and the second fixed point theorems. Then, we consider the relation with the diagonal argument , a relation which is at the origin of the fixed point theorem itself. We also review the Recursion Theorem , which is considered a recursion theoretic version of the fixed point theorem. We end considering systems of equations which are related to fixed points.