Fixed-point combinator on arithmetic functions

Question

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:

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

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

3. 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.

4. 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.

Answer 1

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):
    <code corresponding to G>

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:

1. $\{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.
2. $\{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.