📜 ⬆️ ⬇️

Typeless lambda calculus, combinators, Unlambda and Fibonacci numbers

Next comes the story of the very, in my opinion, hardcore way of programming.
The subject of the post is not easy, the path will be long, and as a cookie at the end I will tell you how to count the Fibonacci numbers in Unlambda.

For experts: the article is more likely to explain how this works, rather than give a strict formal description.

The λ-calculus was invented by Alonzo Church to formalize the concept of algorithm and computability. Functions in λ-calculus should be understood exactly as a kind of algorithm that processes input data.

Typeless λ-Calculus


Suppose we have functions from a single argument. Moreover, both their argument and return value are also functions of one argument.
')
Here, mathematicians will argue: we get a set that coincides with the set of functions from itself into itself, which is impossible in set theory (even in the case of an infinite set, the set of functions is strictly greater). But this did not prevent the American Scott from constructing a Cartesian-closed category by introducing a special topology on partially ordered sets, i.e. the object presented does exist, but that is another story.

So, it would seem that we can do, having at hand only such an abstract and boundless set of strange functions? For a start, it would be nice to decide how to write these functions. In the λ-calculus adopted such rules:


Then λx.fx = f , since this function takes the argument x and returns the value fx , which is what the function f itself does. This is called the η-transform .

For example, λx.x 2 is the squaring function, and (λx.x 2 ) 3 is the application of this function to argument 3. Intuition suggests that the value of this expression is 9, which is claimed by the only axiom of λ-calculus, called β- reduction :

where F [x: = a] means the expression F, in which a is substituted for x instead of x . Together with this axiom, λ-calculus becomes a Turing-complete programming language, i.e. on it you can implement any algorithm (in a reasonable understanding of what the algorithm is). A natural question arises - how?

It is easy to sketch an identical function that simply returns its argument: λx.x
The constant function also does not cause complications: λx.c , where c does not depend on x . Indeed, for any argument, the function will return c .
It would seem, that's all. We do not even know how to build functions from several arguments! No, we can, we just do not know about it yet.

Consider this example: λx.λy.x + y . For greater clarity, put brackets: λx. (Λy. (X + y)) is a function that returns another function that returns a sum. How it works? Let's apply it to some argument: (λx. (Λy. (X + y))) a = λy. (A + y) . The resulting function is applicable to another argument: (λy. (A + y)) b = a + b . This technique is called currying , or currying (after Haskell Curry), and works for any number of arguments. We agree that if a function has the form λx. (Λy. (Λz. (F))) , then we will write it as λxyz.F. We also agree that (fabc) means
(((fa) b) c) . Now the functions of many arguments are written very simply: λxy.x + y , and their use is (fab) .

A small digression: I have already used numbers and arithmetic operations more than once, despite the fact that the article on typeless λ-calculus, and we do not yet formally know about any numbers and operations. This is done to improve understanding, and soon we will learn that both can be realized in λ-calculus.

Control structures



Now we will answer the question of how to make a cycle in λ-calculus. Since we are dealing only with functions, it is obvious with the help of the recursion mechanism. But in the λ-calculus we cannot call a function from within ourselves, so a slightly different approach is used - the function is passed to itself as an argument.

Consider the following function: w = λx.xx. She applies her only argument to herself (remember, because we have something to take - a function). Let's try to apply this function to itself: ww = (λx.xx) w = (xx) [x: = w] = ww . Oops, using the β-reduction, we came to the point where we started. This is one of the simplest examples of an infinite loop in λ-calculus, notable for doing absolutely nothing.

Another important question: how to implement a conditional operator? Here it is important to understand that the else-branch cannot be absent in it. We have all the objects - functions that are required to return the value, and we can not "do nothing." We define the following objects:

Now, if bool is a logical value in the sense of these definitions, then (bool if else) is exactly the construction we need. If bool = true , the result will be an if expression, otherwise the else expression.

Now we will try to solve the classical problem of cycles and recursion - factorial calculation. Let us have already implemented numbers, arithmetic operations (which we will now write in prefix notation, in the style of λ-calculus), the function dec , which reduces its argument by 1, as well as the function zero , with which we can check the number for equality to zero .
g = λrn. (zero n) 1 (* n (rr (dec n)))
Let's look carefully: the function checks n for equality to zero, returns 1 if successful, otherwise returns (* n (rr (dec n))) - the product of n and the values ​​of a certain function r from itself and n-1 . What is the r function? This is a kind of hack to make recursion - as r we will pass the function g itself, which means the written expression really calculates the factorial: g (n) = n * g (n-1) . Since it is inconvenient to transfer functions to itself every time, we will make the final implementation of factorial:
f = gg
Thus, g “remembers” its first argument, and it remains only to pass the necessary number to it for calculations.

Further worse.

Fixed point combinator



It turns out that in any lambda calculus for any function f there exists an argument x such that fx = x . Moreover, this x can always be found! This work is performed by the so-called fixed point combinator . One of his options, invented by our favorite Haskell Curry:
Y = λf. (Λx.f (xx)) (λx.f (xx))
Let's see how it works:
Y f = (λx.f (xx)) (λx.f (xx)) = f ((λx.f (xx)) (λx.f (xx))) = f (Yf)
Thus, Y f is really a fixed point of f , since f (Y f) = Y f .

Numbers and arithmetic



As you might have guessed, all the above implementations of the necessary objects and structures are not unique - the beauty of λ-calculus is that you yourself decide how to realize the basic things you need. But if with respect to cycles and conditions it seems like the simplest implementations are revealed, then with numbers the situation is different - there are a lot of practical implementations of numbers, for each task you can think up your own specific variant. Nevertheless, there is a generally accepted implementation of numbers - the “numeral Church”, thus invented by Alonzo Church.

Define a non-negative number N as a function that takes some function f , an argument x, and N times the value of f from x :

Thus, in the λ-calculus, our numbers look like this:


Inc function:
inc = λnfx.f (nfx)
applied the function n times, and apply it once more to get n + 1 .

How to add m and n ? You need to apply f to x first m and then n times:

add = λmnfx.mf (nfx)

Multiplication is made easier; you need to apply (nf) m times to x :

mult = λmnf.m (nf)

Exponentiation is even simpler:
pow = λmn.nm

We write a function that checks whether our argument is zero:
λn.n (λx.false) true
If the argument is zero, then it (as you remember from the definition) simply returns the second argument, i.e. true , otherwise it will be many times (well, at least once) apply the function λx.false to something there. So the very constants we talked about were useful - the return value will be false .

Now something more difficult is subtraction. First, let's make a function that returns a number that is 1 less (or something, if the argument is 0). Here she is:
dec = λnfx.n (λgh.h (gf)) (λu.x) (λu.u)
I think now even the most persistent lose their nerves in connection with the question “how does this, damn it work?”. Let's try to understand.

First, look at the piece n (λgh.h (gf)) (λu.x) - something unknown n times applied to (λu.x) . Let's be like the Church numerals and apply:


So, we see that after n applications, our expression has the form:
dec n = λfx. (λh.h ((n-1) fx)) ((λu.u)) = λfx. (λu.u) ((n-1) fx) = λfx. (n-1) fx = (n-1)
Profit!
But what does the function return in the case of zero?
dec 0 = λfx. (λu.x) (λu.u) = λfx.x = 0

I note that 0 and false in our definitions are the same.

Now it is easy to write and subtract:
sub = λmn. (n dec) m

Combinators



Combinators are λ-functions that do not contain free variables, i.e. any variable in them is connected by λ-abstraction.
Examples of non- combinators:


Examples of combinators:


And one more interesting fact: it is possible to choose a finite set of combinators through which any other λ-function can be expressed! Such kits are, for example, SKI and BCKW .

Unlambda



Unlambda is a pure functional programming language using combinatorial logic. Namely, to create functions it uses a set of SKI. Applying the function F to the function G is written as `FG , which saves us from unnecessary brackets. Apply multiple arguments in a row: `` `fxyz . In addition to the built-in functions s, k, i , the language has the ability to display ( .x denotes a function similar to i , but as a side effect of displaying the x character on the screen), as well as mechanisms for entering and deferring calculations, but they are about will not go.

Once upon a time, in a galaxy far far away, I found a tutorial on unlambda that ended in about these words:

Now I wanted to explain how in this language you can write a cycle that calculates Fibonacci numbers, but already here I am powerless:
`` `s``s``sii`ki
`k. *` `s``s`ks
`` s`k`s`ks``s``s`ks``s`k`s`kr``s`k`sikk
`k``s`ksk


Well, let's try.
By the way, the program displays the Fibonacci number in the form of the corresponding number of stars on the screen.

We describe the cycle:
  1. We deduce N asterisks
  2. Print the translation to a new line (in ublambda this is done by the function r )
  3. We add N to the memorized previous Fibonacci number


For now, we’ll record everything in the (already) usual λ-calculus style.

Print N asterisks: N print i - N times, apply print to the identity function, and at the same time print N asterisks. As a result, we get the identity function. Let's apply it to something! ((N print i) newline) (cycle (+ NM) N) , where M is the previous Fibonacci number. So, we have the following function of one loop pass:
cycle = λcnm. ((n print i) newline) (c (+ nm) n)
pass the loop itself as a parameter, and initialize it with a single and zero:
fib = cycle cycle 1 0

It remains, as I promised, to translate it to unlambda. Oh.

It would be nice to introduce the reader to the algorithm for converting expressions from the λ-calculus to the SKI set (which, by the way, shows that any function can be expressed through SKI). So, the algorithm itself:



Everything is more or less obvious, except the last. Let's look at the definition of the combinator S :
S = λxyz. (Xz) (yz)
Apply it to F , then to G :
SFG = (λyz. (F z) (yz)) G = λz. (F z) (G z)
Indeed, this is what we need.

The translation algorithm λx.F is reduced to the following actions:


Now let's translate the “bricks” we need into unlambda:
0 = `ki
1 = i
add:
`` s``````````````````````````````````````````````````````````````````````````````` `s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s` `s`ks``s`kk`kk``s`kk
`kk``s``s`ks``s`kk`kk`ki``s``````kk`k`kk `` s``s`ks``s`kk`ks``
s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``` ks``s```ks``s`kk`ks`
`s``s`ks``s`kk`kk``s`kk`ks``s```````` `ks``s`kk`kk``s`kk`kk
`` s`kk`ki````````````````k`k```````````````` `kk``s``s`ks``s`kk`k
k`ki`````````````k`k`k````````````` s``s`ks``s`kk`kk``s`
kki

cycle:
`` s``````````````````````````````````````````````````````````````````````````````` `s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk`
ks```````````````````````` `` s`ks``s`kk`kk``s`kk
`ks````````````` once again s``s`ks``s`kk`kk``s`k
k`ks`````````````````````````````````````````````````` s``s`ks``s`kk`kk`ki`
`s```ks````````````````````````````````````````````````````````````````````````````````` `ks``s`kk`kk``s`kk`k. *
`` s``s`ks``s```ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s`` s`ks``s`kk`kk``s`kk`k
i``````````````````````````````````````````````````````````` `s`ks``s`kk`kk``s`kk`
kr``s````````````````````````````` `` s`ks``s`kk`kk``s`kk
`ks````````````` once again s``s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks``s
kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks`
`kk`ks``s````````kk`ksk`kk````kk`ks```` `s``s`ks``s`kk`kk``
s`kk`kk``s`kk`ki``s`````````` `` s`kk`kk``````
`s`kk`kk`ki```````````S`kk`ks``` kk`kk``s```ks``kk
`kk``s`kki``s```ks``s``````kk`ks``k``kk `kk``s``s`ks``s`kk`
kk`ki


And the finished program:
`` `
`` s``````````````````````````````````````````````````````````````````````````````` `s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk`
ks```````````````````````` `` s`ks``s`kk`kk``s`kk
`ks````````````` once again s``s`ks``s`kk`kk``s`k
k`ks`````````````````````````````````````````````````` s``s`ks``s`kk`kk`ki`
`s```ks````````````````````````````````````````````````````````````````````````````````` `ks``s`kk`kk``s`kk`k. *
`` s``s`ks``s```ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s`` s`ks``s`kk`kk``s`kk`k
i```````````````````````````````````````````````````` `s`ks``s`kk`kk``s`kk`
kr``s````````````````````````````` `` s`ks``s`kk`kk``s`kk
`ks````````````` once again s``s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks``s
kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks`
`kk`ks``s````````kk`ksk`kk````kk`ks```` `s``s`ks``s`kk`kk``
s`kk`kk``s`kk`ki``s`````````` `` s`kk`kk``````
`s`kk`kk`ki```````````S`kk`ks``` kk`kk``s```ks``kk
`kk``s`kki``s```ks``s``````kk`ks``k``kk `kk``s``s`ks``s`kk`kk`ki
`` s``````````````````````````````````````````````````````````````````````````````` `s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk`
ks```````````````````````` `` s`ks``s`kk`kk``s`kk
`ks````````````` once again s``s`ks``s`kk`kk``s`k
k`ks`````````````````````````````````````````````````` s``s`ks``s`kk`kk`ki`
`` s````````````````````````````````````````````````` `ks``s`kk`kk``s`kk`k. *
`` s``s`ks``s```ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s`` s`ks``s`kk`kk``s`kk`k
i``````````````````````````````````````````````````````````` `s`ks``s`kk`kk``s`kk`
kr``s````````````````````````````` `` s`ks``s`kk`kk``s`kk
`ks````````````` once again s``s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks``s
kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks`
`kk`ks``s````````kk`ksk`kk````kk`ks```` `s``s`ks``s`kk`kk``
s`kk`kk``s`kk`ki``s`````````` `` s`kk`kk``````
`s`kk`kk`ki```````````S`kk`ks``` kk`kk``s```ks``kk
`kk``s`kki``s```ks``s``````kk`ks``k``kk `kk``s``s`ks``s`kk`kk`ki
`` s``````````````````````````````````````````````````````````````````````````````` `s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s` `s`ks``s`kk`kk``s`kk
`kk``s``s`ks``s`kk`kk`ki``s``````kk`k`kk `` s``s`ks``s`kk`ks``
s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``` ks``s```ks``s`kk`ks`
`s``s`ks``s`kk`kk``s`kk`ks``s```````` `ks``s`kk`kk``s`kk`kk
`` s`kk`ki````````````````k`k```````````````` `kk``s``s`ks``s`kk`k
k`ki`````````````k`k`k````````````` s``s`ks``s`kk`kk``s`kki
i`ki


Yes, yes, I myself am very scared. By the way, in the collection of programs on unlambda the similar code takes not much less space. Apparently, the author of the language owns the secret ancient techniques of extremely compact and optimized translation from the λ-calculus to unlambda. However, I kept my promise. Thanks to those who read to the end.

Source: https://habr.com/ru/post/143818/


All Articles