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:
- Let f and a be some functions. Then fa means applying the function f to the function a , or, in the terminology of the λ-calculus, an application .
- Let F be an expression that freely contains the variable x or does not contain it at all. Then λx.F denotes a function of the variable x , whose value is given by the expression F , and this is called λ-abstraction.
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.xThe 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:
- true = λxy.x
- false = λxy.y
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 = ggThus,
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 :
- 0: x
- 1: f (x)
- 2: f (f (x))
- 3: f (f (f (x)))
Thus, in the λ-calculus, our numbers look like this:
- 0: λfx.x
- 1: λfx.fx
- 2: λfx.f (fx)
- 3: λfx.f (f (fx))
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.nmWe write a function that checks whether our argument is zero:
λn.n (λx.false) trueIf 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:
- The first time: (λgh.h (gf)) (λu.x) = λh.h ((λu.x) f) = λh.hx = λh.h (0 fx) (by definition, zero)
- Second time: (λgh.h (gf)) (λh.hx) = λh.h ((λh.hx) f) = λh.h (fx) = λh.h (1 fx) (here you need to understand that h inside brackets and h external - different variables)
- Third time: (λgh.h (gf)) (λh.h (fx)) = λh.h ((λh.h (fx)) f) = λh.h (f (fx)) = λh.h (2 fx)
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 = 0I note that 0 and
false in our definitions are the same.
Now it is easy to write and subtract:
sub = λmn. (n dec) mCombinators
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:
- I = λx.x - a function that returns its argument
- K = λxy.x - constant generator
- S = λxyz. (Xz) (yz)
- Y = λf. (Λx.f (xx)) (λx.f (xx)) - now you know why he was called a combinator
- B = λxyz.x (yz)
- C = λxyz.xzy
- W = λxy.xyy
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:
- We deduce N asterisks
- Print the translation to a new line (in ublambda this is done by the function r )
- 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 0It 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:
- λx.F , where F does not depend on x - we need a constant function with the value F , then this is KF
- λx.x is I by definition
- λx.FG , where F and G are expressions that (possibly) contain freely x . We need to substitute the value of x in both expressions, and then apply the first to the second. This is done by the combinator S : SFG
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:
- ` replace with` `s
- x replace with i
- G , independent of x , replaced by `kG
Now let's translate the “bricks” we need into unlambda:
0 = `ki1 = iadd:`` 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.