<p>Fixpoint combinators are just the way recursion is implemented in the <span class="math-container">$\lambda$</span>-calculus.  There's nothing you can do with them that you cannot do in any programming language allowing recursive definitions (which is to say, basically, any general-purpose programming language at all).  In particular, if your method worked in the <span class="math-container">$\lambda$</span>-calculus, it would work in any programming language.</p>
<p>Let <span class="math-container">$F$</span> be the <span class="math-container">$\lambda$</span>-term encoding the function of which you want to compute the fixpoint.  Since it's a function, it does not hurt to suppose that <span class="math-container">$F$</span> starts with an abstraction:
<span class="math-container">$$F=\lambda f.\lambda x_1\ldots\lambda x_n.G$$</span>
where <span class="math-container">$G$</span> does not start with an abstraction and <span class="math-container">$n$</span> may be zero.  Now, intuitively, the behavior of <span class="math-container">$YF$</span> (with <span class="math-container">$Y$</span> a fixpoint combinator) is exactly the same as the following Python program:</p>
<pre><code>def f(x1,...,xn):
    &lt;code corresponding to G&gt;
</code></pre>
<p>Since <span class="math-container">$G$</span> may contain the variable <span class="math-container">$f$</span>, <span class="math-container">$\mathtt{\langle code\ corresponding\ to\ G\rangle}$</span> may contain recursive calls to <span class="math-container">$\mathtt{f}$</span>.</p>
<p>For example, your method for solving the equation <span class="math-container">$x=2-x$</span> corresponds to the Python code</p>
<pre><code>def x():
    return 2 - x
</code></pre>
<p>It should be obvious now why it loops.  You should also see that the <span class="math-container">$\lambda$</span>-calculus plays no special role in your &quot;method&quot;, which may be formulated in any programming language (with recursion).</p>
<p>To see how fixpoint combinators implement recursion, it is useful to recall the formal definition: a <em>fixpoint combinator</em> in the <span class="math-container">$\lambda$</span>-calculus is a closed term <span class="math-container">$Y$</span> such that, for any term <span class="math-container">$F$</span>, we have <span class="math-container">$YF\simeq_\beta F(YF)$</span>, where <span class="math-container">$\simeq_\beta$</span> denotes <span class="math-container">$\beta$</span>-equivalence.  The term <span class="math-container">$F(YF)$</span> is just one unfolding of the recursion defined by <span class="math-container">$YF$</span>.</p>
<p>For understanding this better, it may be helpful to first consider fixpoint combinators that verify something stronger, namely that <span class="math-container">$YF\to^\ast F(YF)$</span>, that is, there is actually a finite sequence of computation steps (<span class="math-container">$\beta$</span>-reduction steps) that leads from <span class="math-container">$YF$</span> to <span class="math-container">$F(YF)$</span>. An example, usually known as Turing's fixpoint combinator, is <span class="math-container">$Y:=XX$</span> where <span class="math-container">$X:=\lambda f.\lambda x.f(xxf)$</span>.  If we try to solve the equation <span class="math-container">$x=2-x$</span> as you tried to do, using one such fixpoint combinator with <span class="math-container">$F:=\lambda x.2-x$</span> (for an arbitrary encoding of integers and subtraction), we get
<span class="math-container">$$YF\to^\ast F(YF)\to 2-YF\to^\ast 2-F(YF)\to 2-(2-YF)\to^\ast\cdots$$</span>
The exact reduction will depend on the evaluation strategy, but subtraction will at some point need to look at its second argument, which will trigger an unfolding of the recursion, which will generate another occurrence of subtraction, which will at some point need to look at its second argument, and so on.  This pattern is independent of the evaluation strategy, and obviously it will never lead to <span class="math-container">$1$</span>, but will keep reducing forever.  While this is not true of <em>every</em> fixpoint combinator, it gives a good idea of what happens in general and, I hope, makes it clear that nothing &quot;magical&quot; is going on: it's just the unfolding of a recursion.</p>
<p>To prove that this will never work in general, we need a bit of <span class="math-container">$\lambda$</span>-calculus theory, in particular the fact that the <span class="math-container">$\lambda$</span>-calculus admits models in certain partially ordered sets.  In short, recalling only what is strictly necessary for our present purposes, there is a partially ordered set <span class="math-container">$(D,\leq)$</span> with least element <span class="math-container">$\bot$</span> such that:</p>
<ul>
<li>each term <span class="math-container">$M$</span> may be interpreted at the same time as a point <span class="math-container">$[M]\in D$</span> and as a monotonic function <span class="math-container">$\{M\}:D\to D$</span>;</li>
<li><span class="math-container">$\beta$</span>-equivalence becomes equality: for all terms <span class="math-container">$M,N$</span>, <span class="math-container">$M\simeq_\beta N$</span> implies <span class="math-container">$[M]=[N]$</span>;</li>
<li>for any fixpoint combinator <span class="math-container">$Y$</span> and any term <span class="math-container">$F$</span>, <span class="math-container">$[YF]=\bigvee_{n\in\mathbb N}\{F\}^n(\bot)$</span>, where <span class="math-container">$\vee$</span> denotes supremum;</li>
<li>if <span class="math-container">$M$</span> and <span class="math-container">$N$</span> are two distinct normal forms, then <span class="math-container">$[M]$</span> and <span class="math-container">$[N]$</span> are unrelated by the order relation of <span class="math-container">$D$</span>, and they are maximal in it;</li>
<li>for every term <span class="math-container">$M$</span>, <span class="math-container">$[M]=\bot$</span> implies that <span class="math-container">$M$</span> has no normal form (its evaluation does not terminate).</li>
</ul>
<p>A well-known, completely standard example of model satisfying all of the above is given by so-called <em>Böhm trees</em> (see for example Barendregt's book <em>The Lambda-Calculus: Its Syntax and Semantics</em>).</p>
<p>With this at hand, it is easy to observe that fixpoint combinators find <em>least</em> fixpoints, that is, for any fixpoint combinator <span class="math-container">$Y$</span> and any term <span class="math-container">$F$</span>, <span class="math-container">$[YF]$</span> is a fixpoint of <span class="math-container">$\{F\}$</span> and, whenever <span class="math-container">$x\in D$</span> is another fixpoint of <span class="math-container">$\{F\}$</span>, we have <span class="math-container">$[YF]\leq x$</span>. In fact, for all <span class="math-container">$n\in\mathbb N$</span>, we have <span class="math-container">$\{F\}^n(\bot)\leq\{F\}^n(x)=x$</span> (by monotonicity and the fact that <span class="math-container">$x$</span> is a fixpoint of <span class="math-container">$\{F\}$</span>), which implies <span class="math-container">$[YF]\leq x$</span> because <span class="math-container">$[YF]$</span> is the supremum of all <span class="math-container">$\{F\}^n(\bot)$</span>.</p>
<p>Now, take any representation of integers as normalizable <span class="math-container">$\lambda$</span>-terms (for example, the Church integers), such that the set of functions of interest (for example, arithmetic functions for writing linear equations) is definable in the <span class="math-container">$\lambda$</span>-calculus on this representation.  Take any term <span class="math-container">$F$</span> representing any such function of interest.  There are two cases:</p>
<ol>
<li><span class="math-container">$\{F\}(\bot)=x\neq\bot$</span>. In that case, by monotonicity and maximality, <span class="math-container">$\{F\}$</span> is necessarily constant, so <span class="math-container">$x$</span> denotes some integer <span class="math-container">$m$</span> and <span class="math-container">$F\,n\simeq_\beta m$</span> for all <span class="math-container">$n$</span>.  The fixpoint combinator will find the integer fixpoint, but it has no interest.</li>
<li><span class="math-container">$\{F\}(\bot)=\bot$</span>.  Then <span class="math-container">$\bot$</span> is a fixpoint, and since it is certainly the least, that's what the fixpoint combinator fill find: <span class="math-container">$[YF]=\bot$</span>, hence, by the last point above, <span class="math-container">$YF$</span> loops.</li>
</ol>
<p>This settles the question (including the edit): fixpoint combinators cannot be used to find integer fixpoints of functions on integers, no matter how integers are represented.  In fact, they cannot be used to find fixpoint of functions on any data type whose elements are represented by normal(izable) terms.  As I tried to explain in the first part of the answer, fixpoint combinators are useful for finding fixpoints of <em>functionals</em>, that is, functions on functions, in which case they correctly implement recursive definitions.</p>

CC BY-SA 4.0
2022-10-16T00:05:47.817Z
Thank you for this explanation. I can count this as a good answer to sub question 1. Yet there are still 3 more sub questions that are not precisely addressed in this answer. For example, sub question 2 should have a definite answer of yes or no, while the closest I found in this answer is *...sometimes that happens to be ⊥*. For sub question 3, typing provides useful insights, but wouldn't there be some functions that work with such combinators but don't conform to such typing? For sub question 4, I don't have any clue how linear equations can be solved efficiently in lambda calculus.
Cyker
CC BY-SA 4.0
2022-10-16T07:27:21.703Z
I hope I'll have have time later to add proper explanations, but, in short, the answer to your subquestions are: 2) no; 3) fixpoint combinators always work, that is, they do what they're supposed to do.  If you think they don't, then please provide a formal explanation to what you mean by "work"; 4) the $\lambda$-calculus is a programming language.  How would you solve arithmetic equations in, say, Java or Python?  Take your favorite answer, and translate it in the $\lambda$-calculus.  This is my "most intuitive way"...
Damiano Mazza
CC BY-SA 4.0
2022-10-16T17:37:51.317Z
Sure, I'm not in a hurry. Whenever you have time. 2) I'm interested in the details of "no". 3) "work" means the combinator terminates with a valid answer. Infinite loop is not regarded as valid. Lambda terms outside of the encoding are debatable. 4) Your most intuitive way is not quite the same as mine, but this sub question is somewhat subjective. I wrote a bit about my "most intuitive way" in the question and you are free to leave a comment or not.
Cyker
CC BY-SA 4.0
2022-10-16T19:32:29.623Z
I updated the answer.  I don't think I understand your "fat" vs. "thin" combinators, but I hope the additional details clarify why what you suggest cannot work, at least not with fixpoint combinators in the standard sense of the word.
Damiano Mazza
CC BY-SA 4.0
2022-10-16T23:40:04.053Z
Thanks this is much more complete answer. It might take me a while to digest though. For what I have read, I have a minor question: Why are you able to go from `2−YF` to `2−F(YF)` using beta reductions? It would be written as `((sub two) YF)` and `((sub two) F(YF))` in lambda calculus and the evaluation of `(sub two)` could happen before the rest of the lambda term depending on the evaluation order. When you say some computation will loop forever I assume the argument shall be made using CBN not CBV, because looping in CBV doesn't necessarily mean looping in CBN?
Cyker
CC BY-SA 4.0
2022-10-17T05:13:37.960Z
I added an explanation about evaluation strategies.  I also restructured the whole answer to make it a bit more synthetic and give, in the first part, a (hopefully) better intuitive explanation of why it does not work.
Damiano Mazza
CC BY-SA 4.0
2022-10-15T08:22:13.323Z
2022-10-17T06:59:53.293Z
2022-10-17T06:59:53.293Z
Damiano Mazza
<p>The question is about this Racket program:</p>
<pre><code>#lang lazy

;church numeral 0
(define zero (lambda (f) (lambda (x) x)))
;church numeral 1
(define one (lambda (f) (lambda (x) (f x))))
;church numeral 2
(define two (lambda (f) (lambda (x) (f (f x)))))
;church numeral to int
(define to-int (lambda (n) ((n (lambda (x) (+ x 1))) 0)))
;church numeral predecessor: n - 1
(define pred (lambda (n) (lambda (f) (lambda (x) (((n (lambda (g) (lambda (h) (h (g f))))) (lambda (u) x)) (lambda (u) u))))))
;church numeral subtraction: m - n
(define sub (lambda (m) (lambda (n) ((n pred) m))))
;Y combinator
(define Y (lambda(f) ((lambda(x) (f (x x))) (lambda(x) (f (x x))))))
;Z combinator
(define Z (lambda(f) ((lambda(x) (f (lambda(v) ((x x) v)))) (lambda(x) (f (lambda(v) ((x x) v)))))))
;F(x) = 2 - x
(define F (lambda (x) ((sub two) x)))
;G(_)(x) = 2 - x
(define G (lambda (_) (lambda (x) ((sub two) x))))

(to-int one)                                                             ;ok(1)
(to-int (F one))                                                         ;ok(1)
(to-int ((Y G) one))                                                     ;ok(1)
(to-int ((Z G) one))                                                     ;ok(1)
;(to-int (Y F))                                                          ;err
;(to-int (Z F))                                                          ;err
</code></pre>
<p>As commented, this program first defines some numerals in <a href="https://en.wikipedia.org/wiki/Church_encoding" rel="nofollow noreferrer">Church encoding</a>, some arithmetic operators on these numerals as well as Y and Z combinators. Then it tries to find a solution to the arithmetic equation <code>x = 2 - x</code> using functional programming. The way it tries to solve this problem is to define <code>F(x) = 2 - x</code> (in Church encoding) then use a combinator to compute its fixed point. If the combinator is clever, it may return <code>one</code> which is a solution. But after running this program, both Y and Z combinators enter an infinite loop (marked as <code>err</code>). So this method doesn't seem to work.</p>
<p>My questions are:</p>
<ol>
<li><p>What is a high-level description of the reason why this method fails?</p>
</li>
<li><p>Are there other fixed-point combinators that can solve this equation?</p>
</li>
<li><p><code>Y</code> and <code>Z</code> combinators work with <code>G</code> but not <code>F</code>. So we know they work with some, but not all functions. How do we characterize the class of functions that work with these combinators?</p>
<p>Edit. <em>work</em> means the combinator terminates on the input and returns a meaningful result.</p>
</li>
<li><p>Because lambda calculus is Turing-complete, it should be able to solve such equations (our computers <a href="https://www.wolframalpha.com/input?i2d=true&amp;i=x%3D2-x" rel="nofollow noreferrer">can</a>). If direct application of a fixed-point combinator (to the Church encoding of the linear equations) doesn't work, what is the most intuitive way of doing so in lambda calculus?</p>
<p>Edit. The currently known best solution is to translate the whole linear equation algorithm into lambda calculus that results in a &quot;fat&quot; combinator, and it is specific to linear equations not fixed points. OTOH the most intuitive solution in my mind is a &quot;thin&quot; fixed-point combinator, which solves the linear equation by finding its fixed point. An example is solving <code>ax + b = 0</code> by solving <code>F(x) = (a+1)x + b = x</code>. The solution should be first encoding <code>F</code> into lambda calculus then <code>YF</code> magically comes to be the correct answer. Everyone knows the answer is <code>-b/a</code>, so implementing this computation as a combinator in lambda calculus is a solution, but it is &quot;fat&quot;. I am looking for a possibility of encoding the complexity in the <em>problem</em> not the <em>solver</em>. This makes the fixed-point combinator a generic tool for other problems that can be reducted to finding a fixed point.</p>
<p>The program above shows it's impossible when using <code>Y</code> as the solver in Church encoding. But what if you can use another encoding or even develop your own? In other words, can you give another set of definitions of <code>one</code>, <code>two</code> and <code>sub</code> in the Racket program so that:</p>
<pre><code>(define F (lambda (x) ((sub two) x)))
(Y F)   ;gives `one`
</code></pre>
<p>Your set of definitions must work with other numerals too, and you probably also need to define <code>add</code> and <code>mul</code>, so you can encode not only <code>F(x) = 2 - x</code> but also <code>F(x) = (a+1)x + b</code> for any <code>a</code> and <code>b</code>.</p>
</li>
</ol>

CC BY-SA 4.0
2022-10-15T08:24:36.533Z
This is not research level but it is a very good student-level question.  Since I am not sure it would be answered on the CS website (which I never look at), I'm giving an answer here.  To moderators: of course it would be good if both question and answer can be moved to the non-research-level site.
Damiano Mazza
CC BY-SA 4.0
2022-10-16T00:25:10.033Z
@DamianoMazza Well, I don't think this is a student-level question (if you mean students in universities or high schools). If you read sub question 4, essentially it explores a methodology to solve linear equations in lambda calculus using combinators. This might be an idea too crazy for students. It could be inefficient or inelegant, but who knows there won't be a great solution, like one combinator that magically returns the answer on the problem formulated in lambda calculus?
Cyker
CC BY-SA 4.0
2022-10-16T07:19:28.813Z
I shouldn't have said student-level, I should have said beginner-level.  That is, someone who has a basic knowledge of the $\lambda$-calculus but does not (yet) have a deeper understanding of it.  There's nothing "crazy" about your question, it's just based on a completely legitimate misunderstanding of how fixpoint combinators work (and I think it could perfectly be asked by a good student, but that's beside the point).
Damiano Mazza
CC BY-SA 4.0
2022-10-16T17:46:48.427Z
@DamianoMazza I was seeking non-typical use of fixed point combinators on purpose. This probably wasn't obvious in the question. I expanded the question a bit in its 4th part. In short, I was seeking the possibility of using fixed point combinators as a generic tool for other problems that can be reducted to finding a fixed point. The fixed point combinator itself has no knowledge of the problem domain, but maybe the problem can be well encoded to let this "silly" combinator work on it magically.
Cyker
<lambda-calculus><linear-equations><fixed-points>
Fixed-point combinator on arithmetic functions
Cyker
# Fixed-point combinator on arithmetic functions

(Asked by: username_0 on 2022-10-14)

The question is about this Racket program:
#lang lazy

;church numeral 0
(define zero (lambda (f) (lambda (x) x)))
;church numeral 1
(define one (lambda (f) (lambda (x) (f x))))
;church numeral 2
(define two (lambda (f) (lambda (x) (f (f x)))))
;church numeral to int
(define to-int (lambda (n) ((n (lambda (x) (+ x 1))) 0)))
;church numeral predecessor: n - 1
(define pred (lambda (n) (lambda (f) (lambda (x) (((n (lambda (g) (lambda (h) (h (g f))))) (lambda (u) x)) (lambda (u) u))))))
;church numeral subtraction: m - n
(define sub (lambda (m) (lambda (n) ((n pred) m))))
;Y combinator
(define Y (lambda(f) ((lambda(x) (f (x x))) (lambda(x) (f (x x))))))
;Z combinator
(define Z (lambda(f) ((lambda(x) (f (lambda(v) ((x x) v)))) (lambda(x) (f (lambda(v) ((x x) v)))))))
;F(x) = 2 - x
(define F (lambda (x) ((sub two) x)))
;G(_)(x) = 2 - x
(define G (lambda (_) (lambda (x) ((sub two) x))))

(to-int one)                                                             ;ok(1)
(to-int (F one))                                                         ;ok(1)
(to-int ((Y G) one))                                                     ;ok(1)
(to-int ((Z G) one))                                                     ;ok(1)
;(to-int (Y F))                                                          ;err
;(to-int (Z F))                                                          ;err

As commented, this program first defines some numerals in Church encoding, some arithmetic operators on these numerals as well as Y and Z combinators. Then it tries to find a solution to the arithmetic equation x = 2 - x using functional programming. The way it tries to solve this problem is to define F(x) = 2 - x (in Church encoding) then use a combinator to compute its fixed point. If the combinator is clever, it may return one which is a solution. But after running this program, both Y and Z combinators enter an infinite loop (marked as err). So this method doesn't seem to work.
My questions are:

What is a high-level description of the reason why this method fails?

Are there other fixed-point combinators that can solve this equation?

Y and Z combinators work with G but not F. So we know they work with some, but not all functions. How do we characterize the class of functions that work with these combinators?
Edit. work means the combinator terminates on the input and returns a meaningful result.

Because lambda calculus is Turing-complete, it should be able to solve such equations (our computers can). If direct application of a fixed-point combinator (to the Church encoding of the linear equations) doesn't work, what is the most intuitive way of doing so in lambda calculus?
Edit. The currently known best solution is to translate the whole linear equation algorithm into lambda calculus that results in a "fat" combinator, and it is specific to linear equations not fixed points. OTOH the most intuitive solution in my mind is a "thin" fixed-point combinator, which solves the linear equation by finding its fixed point. An example is solving ax + b = 0 by solving F(x) = (a+1)x + b = x. The solution should be first encoding F into lambda calculus then YF magically comes to be the correct answer. Everyone knows the answer is -b/a, so implementing this computation as a combinator in lambda calculus is a solution, but it is "fat". I am looking for a possibility of encoding the complexity in the problem not the solver. This makes the fixed-point combinator a generic tool for other problems that can be reducted to finding a fixed point.
The program above shows it's impossible when using Y as the solver in Church encoding. But what if you can use another encoding or even develop your own? In other words, can you give another set of definitions of one, two and sub in the Racket program so that:
(define F (lambda (x) ((sub two) x)))
(Y F)   ;gives `one`

Your set of definitions must work with other numerals too, and you probably also need to define add and mul, so you can encode not only F(x) = 2 - x but also F(x) = (a+1)x + b for any a and b.

**Tags:** lambda-calculus, linear-equations, fixed-points
> **Comments:**
> **username_1**: This is not research level but it is a very good student-level question.  Since I am not sure it would be answered on the CS website (which I never look at), I'm giving an answer here.  To moderators: of course it would be good if both question and answer can be moved to the non-research-level site.  
> **username_0**: @DamianoMazza Well, I don't think this is a student-level question (if you mean students in universities or high schools). If you read sub question 4, essentially it explores a methodology to solve linear equations in lambda calculus using combinators. This might be an idea too crazy for students. It could be inefficient or inelegant, but who knows there won't be a great solution, like one combinator that magically returns the answer on the problem formulated in lambda calculus?  
> **username_1**: I shouldn't have said student-level, I should have said beginner-level.  That is, someone who has a basic knowledge of the $\lambda$-calculus but does not (yet) have a deeper understanding of it.  There's nothing "crazy" about your question, it's just based on a completely legitimate misunderstanding of how fixpoint combinators work (and I think it could perfectly be asked by a good student, but that's beside the point).  
> **username_0**: @DamianoMazza I was seeking non-typical use of fixed point combinators on purpose. This probably wasn't obvious in the question. I expanded the question a bit in its 4th part. In short, I was seeking the possibility of using fixed point combinators as a generic tool for other problems that can be reducted to finding a fixed point. The fixed point combinator itself has no knowledge of the problem domain, but maybe the problem can be well encoded to let this "silly" combinator work on it magically.  

---

## 1 answers

### Answer by username_1 on 2022-10-15. Score: 3 | Accepted answer

Fixpoint combinators are just the way recursion is implemented in the $\lambda$-calculus.  There's nothing you can do with them that you cannot do in any programming language allowing recursive definitions (which is to say, basically, any general-purpose programming language at all).  In particular, if your method worked in the $\lambda$-calculus, it would work in any programming language.
Let $F$ be the $\lambda$-term encoding the function of which you want to compute the fixpoint.  Since it's a function, it does not hurt to suppose that $F$ starts with an abstraction:
$$F=\lambda f.\lambda x_1\ldots\lambda x_n.G$$
where $G$ does not start with an abstraction and $n$ may be zero.  Now, intuitively, the behavior of $YF$ (with $Y$ a fixpoint combinator) is exactly the same as the following Python program:
def f(x1,...,xn):
    

Since $G$ may contain the variable $f$, $\mathtt{\langle code\ corresponding\ to\ G\rangle}$ may contain recursive calls to $\mathtt{f}$.
For example, your method for solving the equation $x=2-x$ corresponds to the Python code
def x():
    return 2 - x

It should be obvious now why it loops.  You should also see that the $\lambda$-calculus plays no special role in your "method", which may be formulated in any programming language (with recursion).
To see how fixpoint combinators implement recursion, it is useful to recall the formal definition: a fixpoint combinator in the $\lambda$-calculus is a closed term $Y$ such that, for any term $F$, we have $YF\simeq_\beta F(YF)$, where $\simeq_\beta$ denotes $\beta$-equivalence.  The term $F(YF)$ is just one unfolding of the recursion defined by $YF$.
For understanding this better, it may be helpful to first consider fixpoint combinators that verify something stronger, namely that $YF\to^\ast F(YF)$, that is, there is actually a finite sequence of computation steps ($\beta$-reduction steps) that leads from $YF$ to $F(YF)$. An example, usually known as Turing's fixpoint combinator, is $Y:=XX$ where $X:=\lambda f.\lambda x.f(xxf)$.  If we try to solve the equation $x=2-x$ as you tried to do, using one such fixpoint combinator with $F:=\lambda x.2-x$ (for an arbitrary encoding of integers and subtraction), we get
$$YF\to^\ast F(YF)\to 2-YF\to^\ast 2-F(YF)\to 2-(2-YF)\to^\ast\cdots$$
The exact reduction will depend on the evaluation strategy, but subtraction will at some point need to look at its second argument, which will trigger an unfolding of the recursion, which will generate another occurrence of subtraction, which will at some point need to look at its second argument, and so on.  This pattern is independent of the evaluation strategy, and obviously it will never lead to $1$, but will keep reducing forever.  While this is not true of every fixpoint combinator, it gives a good idea of what happens in general and, I hope, makes it clear that nothing "magical" is going on: it's just the unfolding of a recursion.
To prove that this will never work in general, we need a bit of $\lambda$-calculus theory, in particular the fact that the $\lambda$-calculus admits models in certain partially ordered sets.  In short, recalling only what is strictly necessary for our present purposes, there is a partially ordered set $(D,\leq)$ with least element $\bot$ such that:

each term $M$ may be interpreted at the same time as a point $[M]\in D$ and as a monotonic function $\{M\}:D\to D$;
$\beta$-equivalence becomes equality: for all terms $M,N$, $M\simeq_\beta N$ implies $[M]=[N]$;
for any fixpoint combinator $Y$ and any term $F$, $[YF]=\bigvee_{n\in\mathbb N}\{F\}^n(\bot)$, where $\vee$ denotes supremum;
if $M$ and $N$ are two distinct normal forms, then $[M]$ and $[N]$ are unrelated by the order relation of $D$, and they are maximal in it;
for every term $M$, $[M]=\bot$ implies that $M$ has no normal form (its evaluation does not terminate).

A well-known, completely standard example of model satisfying all of the above is given by so-called Böhm trees (see for example Barendregt's book The Lambda-Calculus: Its Syntax and Semantics).
With this at hand, it is easy to observe that fixpoint combinators find least fixpoints, that is, for any fixpoint combinator $Y$ and any term $F$, $[YF]$ is a fixpoint of $\{F\}$ and, whenever $x\in D$ is another fixpoint of $\{F\}$, we have $[YF]\leq x$. In fact, for all $n\in\mathbb N$, we have $\{F\}^n(\bot)\leq\{F\}^n(x)=x$ (by monotonicity and the fact that $x$ is a fixpoint of $\{F\}$), which implies $[YF]\leq x$ because $[YF]$ is the supremum of all $\{F\}^n(\bot)$.
Now, take any representation of integers as normalizable $\lambda$-terms (for example, the Church integers), such that the set of functions of interest (for example, arithmetic functions for writing linear equations) is definable in the $\lambda$-calculus on this representation.  Take any term $F$ representing any such function of interest.  There are two cases:

$\{F\}(\bot)=x\neq\bot$. In that case, by monotonicity and maximality, $\{F\}$ is necessarily constant, so $x$ denotes some integer $m$ and $F\,n\simeq_\beta m$ for all $n$.  The fixpoint combinator will find the integer fixpoint, but it has no interest.
$\{F\}(\bot)=\bot$.  Then $\bot$ is a fixpoint, and since it is certainly the least, that's what the fixpoint combinator fill find: $[YF]=\bot$, hence, by the last point above, $YF$ loops.

This settles the question (including the edit): fixpoint combinators cannot be used to find integer fixpoints of functions on integers, no matter how integers are represented.  In fact, they cannot be used to find fixpoint of functions on any data type whose elements are represented by normal(izable) terms.  As I tried to explain in the first part of the answer, fixpoint combinators are useful for finding fixpoints of functionals, that is, functions on functions, in which case they correctly implement recursive definitions.

> **Comments:**
> **username_0**: Thank you for this explanation. I can count this as a good answer to sub question 1. Yet there are still 3 more sub questions that are not precisely addressed in this answer. For example, sub question 2 should have a definite answer of yes or no, while the closest I found in this answer is *...sometimes that happens to be ⊥*. For sub question 3, typing provides useful insights, but wouldn't there be some functions that work with such combinators but don't conform to such typing? For sub question 4, I don't have any clue how linear equations can be solved efficiently in lambda calculus.  
> **username_1**: I hope I'll have have time later to add proper explanations, but, in short, the answer to your subquestions are: 2) no; 3) fixpoint combinators always work, that is, they do what they're supposed to do.  If you think they don't, then please provide a formal explanation to what you mean by "work"; 4) the $\lambda$-calculus is a programming language.  How would you solve arithmetic equations in, say, Java or Python?  Take your favorite answer, and translate it in the $\lambda$-calculus.  This is my "most intuitive way"...  
> **username_0**: Sure, I'm not in a hurry. Whenever you have time. 2) I'm interested in the details of "no". 3) "work" means the combinator terminates with a valid answer. Infinite loop is not regarded as valid. Lambda terms outside of the encoding are debatable. 4) Your most intuitive way is not quite the same as mine, but this sub question is somewhat subjective. I wrote a bit about my "most intuitive way" in the question and you are free to leave a comment or not.  
> **username_1**: I updated the answer.  I don't think I understand your "fat" vs. "thin" combinators, but I hope the additional details clarify why what you suggest cannot work, at least not with fixpoint combinators in the standard sense of the word.  
> **username_0**: Thanks this is much more complete answer. It might take me a while to digest though. For what I have read, I have a minor question: Why are you able to go from `2−YF` to `2−F(YF)` using beta reductions? It would be written as `((sub two) YF)` and `((sub two) F(YF))` in lambda calculus and the evaluation of `(sub two)` could happen before the rest of the lambda term depending on the evaluation order. When you say some computation will loop forever I assume the argument shall be made using CBN not CBV, because looping in CBV doesn't necessarily mean looping in CBN?  
> **username_1**: I added an explanation about evaluation strategies.  I also restructured the whole answer to make it a bit more synthetic and give, in the first part, a (hopefully) better intuitive explanation of why it does not work.  

---

