Calculate factorial on Church numbers

Good day friends!

The topic of functional programming is quite well covered in Habré, there are a whole bunch of articles devoted to λ-calculus , Church numbers and similar topics, so I will not reveal anything new, but we will write one useless and extremely inefficient program.

In order that life does not seem to be honey, we limit ourselves to a small subset of the JavaScript language, namely, we will use only anonymous functions from a single argument. More we will not need anything (well, almost).
')
Let's start with the definition of factorial, and see what we need in the process of solving the problem:

var fact = function (n) { if (n === 0) return 1; return n * fact(n - 1); }; 

So, we will need functions, logical values ​​(for the result of the comparison operation with zero), the conditional operator, multiplication and subtraction operations, besides, we will need to implement a recursive function call.

Ready?

Let's start with a simple, with logical values True , False and If functions. True and False are represented by the curried functions of two arguments that select the first or second argument. True selects the first argument, and False selects the second. If takes three arguments, a boolean value, a then branch, and an else branch.

 var True = function (x) { return function (y) { return x; }; }; var False = function (x) { return function (y) { return y; }; }; var If = function (p) { return function (t) { return function (e) { return p(t)(e); } }; }; 

You can indulge in the console by executing the type code:

 console.log(If(True)('foo')('bar')); console.log(If(False)('foo')('bar')); 

Next we need numbers. The set of natural numbers can be obtained by determining the value of the number ZERO and the operation PLUS_ODIN. Church numbers, roughly speaking, are functions of two arguments, applying the first argument to the second n times, where n is the corresponding natural number.

 var Zero = function (f) { return function (x) { return x; }; }; var Succ = function (n) { return function (f) { return function (x) { return f(n(f)(x)); }; }; }; 

Additionally, we define a predicate that checks whether a number is zero, the implementation of factorial will require such a check. The predicate returns False if the first argument of the number is executed at least once.

 var IsZero = function (n) { return n(function (x) { return False; })(True); }; 

Check how the numbers work:

 Succ(Succ(Succ(Zero)))(function (x) { return x + 1; })(0); console.log(If(IsZero(Zero))('zero')('not zero')); console.log(If(IsZero(Succ(Zero)))('zero')('not zero')); 

As you can see, one has been added to zero three times, and the predicate correctly recognizes the transferred number.

Now, when we have all natural numbers, we define a function that multiplies two numbers, the result of multiplication is a function that takes its argument n times m times.

 var Mul = function (n) { return function (m) { return function (f) { return n(m(f)); }; }; }; 

It remains to learn how to take one from the number. It's all a little more complicated. The idea of ​​subtraction is to build a pair of numbers (n, n - 1) and take the second element of the pair. Thus, we need to get the constructor of the pair, as well as the functions of getting the first and second element. After which we will be able to determine the function of getting the previous number.

 var Pair = function (a) { return function (b) { return function (t) { return t(a)(b); }; }; }; var Fst = function (p) { return p(True); }; var Snd = function (p) { return p(False); }; var Pred = function (n) { return function (s) { return function (z) { return Snd(n(function (p) { return Pair(s(Fst(p)))(Fst(p)); })(Pair(z)(z))); }; }; }; 

Let's play with couples and subtraction:

 Fst(Pair('foo')('bar')); // => "foo" Snd(Pair('foo')('bar')); // => "bar" Pred(Succ(Succ(Zero)))(function (x) { return x + 1; })(0); // => 1 

It would seem that everything is ready and factorial can be implemented:

 var fact = function (n) { return If(IsZero(n))(Succ(Zero))(Mul(n)(fact(Pred(n)))); }; 

But there are two problems, the first is that JavaScript is a language with an applicative order of computation and our factorial will just hang, because will perform a recursive call regardless of the value of the argument. This problem is easily solved by wrapping the recursive call into an anonymous function and thereby postponing execution.

 var fact = function (n) { return If(IsZero(n))(Succ(Zero))(function (x) { return Mul(n)(fact(Pred(n)))(x); }); }; 

Now the function works correctly:

 fact(Succ(Succ(Succ(Zero))))(function (x) { return x + 1; })(0); // => 6 

The last problem remains. At first, I promised to use only anonymous functions, and here we see a recursive call named fact . We need to get rid of it and the Y-combinator will help us in this. I will not explain the principle of his work; there are articles on this topic both on Habré and outside of Habr. For example, I recommend this blog post . Y-combinator in applicative language looks like this:

 var Y = function (f) { return function (x) { return x(x); }(function (x) { return function (y) { return f(x(x))(y); }; }); }; 

You can check the correctness of his work as follows:

 Y(function (f) { return function (n) { return If(IsZero(n))(Succ(Zero))(function (x) { return Mul(n)(f(Pred(n)))(x); }); }; })(Succ(Succ(Succ(Zero))))(function (x) { return x + 1; })(0); // => 6 

Now we substitute the factorial in the Y-combinator and get the final version:

 var fact = function (x) { return x(x); }(function (x) { return function (y) { return function (f) { return function (n) { return If(IsZero(n))(Succ(Zero))(function (x) { return Mul(n)(f(Pred(n)))(x); }); }; }(x(x))(y); }; }); 

For more convenience, we define the functions NatToChurch and ChurchToNat :

 var NatToChurch = function (n) { return n == 0 ? Zero : function (f) { return function (x) { return f(NatToChurch(n - ChurchToNat(Succ(Zero)))(f)(x)); }; }; }; var ChurchToNat = function (n) { return n(function (x) { return x + 1; })(0); }; 

Now you can set up experiments in the console:

 ChurchToNat(fact(NatToChurch(5))); // => 120 

Last step, make all substitutions and get the final function:



It remains to answer the question "Why do this?". I admit honestly, I have no answer to this question. All good!