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?
$\begingroup$
$\endgroup$
1
-
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$– Damiano MazzaCommented Mar 14, 2017 at 17:30
Add a comment
|