A fixed point combinator is supposed to find the fixed point of any function. Yet I am wondering what if a function happens to have no fixed point, such as the add1 function over $\mathbb{Z}$, mapping -1 to 0, 0 to 1, etc. Does the fixed point combinator make sense any more?

  • 1
    $\begingroup$ Welcome to TCS StackExchange! This forum is for research-level questions on theoretical computer science. Your question is better suited for CS StackExchange. A quick answer: if your language is total (everything terminates), then there is no fixpoint combinator. Therefore, the very existence of a fixpoint combinator implies the existence of partial (nonterminating) functions, hence the existence of a $\bot$ (undefined) element in any type, including $\mathbb Z$. In the case you mention, the fixpoint of $\mathtt{add1}$ is precisely $\bot$. $\endgroup$ Mar 14, 2017 at 17:30


Browse other questions tagged or ask your own question.