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?
Zcombinators work with
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 = 0by solving
F(x) = (a+1)x + b = x. The solution should be first encoding
Finto lambda calculus then
YFmagically 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
Yas 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
subin 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
mul, so you can encode not only
F(x) = 2 - xbut also
F(x) = (a+1)x + bfor any