# Fixed-point combinator on arithmetic functions

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

• 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. Oct 15, 2022 at 8:24
• @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? Oct 16, 2022 at 0:25
• 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). Oct 16, 2022 at 7:19
• @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. Oct 16, 2022 at 17:46

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.

• 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. Oct 16, 2022 at 0:05
• 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"... Oct 16, 2022 at 7:27
• 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. Oct 16, 2022 at 17:37
• 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. Oct 16, 2022 at 19:32
• 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? Oct 16, 2022 at 23:40