λ-calculus and LISP

A typical lover of λ-calculus.

One day, surfing the internet, I came across news of a lis-like, embedded programming language Shen . Previously, they had a Lisp code on their home page. In the example, the authors describe the abstract collection and functions of working with them.

It just so happened that I am a secret admirer of functional programming, which means, to some extent, lambda calculus, which consists almost entirely of abstractions. I wanted to write something as abstract as possible and, in order to complicate my task, I decided that the built-in data types are for weak applicationists, and everything must be implemented in terms of Church coding.
')
I was familiar with the lambda calculus very superficially, since almost always the articles on this branch of mathematics consist entirely of formulas that cannot be tried in practice in any way. Therefore, the idea came to deal with him in practice, and it is possible to attract the adherents of the Turing machine of the PLO to the dark side.

If you're not afraid of Lisp, a lot of lambdas and y-combinator (not the one with the news),

Introduction

The article does not claim to be complete coverage of the material or to replace the SICP . I am not a mathematician, much less am I an expert on lambda calculus. The only thing she claims is linearity of presentation. In the text, the task is to acquaint readers with the functions as first-class citizens and make it as interesting as possible for the lambda calculus. In the process of writing code, I will try to explain what is happening in a simple language understandable to engineers.

Today, there is a strong tendency to borrow concepts from functional programming with imperative languages ​​(even in C ++, after 30 years, the committee went to such an adventurous act. And yes, Java8), so there is hope that this article will be useful to someone. Naturally, if there are lambda calculator lovers on Habré that can correct me, add comments.

So, “why was Lisp chosen?” You ask. There are several reasons for this. The first is that all examples in articles on functional programming are written in Haskell. The second is the already mentioned book: Structure and Interpretation of Computer Programs, which is one of my favorite books and which I recommended reading to anyone who has not done so yet. Third, because Lisp is for real hackers.


Good old joke

On Habré there are several articles on lambda calculus. For example, here and here . Some of them reveal the theory more widely than I try to do, so I would advise you to read at least one of them to understand what we will do. I will not give here the whole theory in order not to complicate the article. To write our abstractions, we will have enough articles on Wikipedia (all real programmers write programs like this). English-language articles broader topics, so you can use articles about Lambda Calculus and a more detailed article describing Church Encoding types of coding.

We also need to know the programming language LISP. But do not worry if you do not know him, because the whole syntax of it consists of brackets, we will quickly learn it. All we need to know is how lambda terms are written in Lisp and, a little later, to shorten the record, several functions. It is enough to know that in Lisp, to execute a function, you need to enclose its call in brackets, in which the first argument will be the name of the function, followed by parameters (very similar to Polish notation ). That is, to find the amount you need to write (+ 2 3), to merge strings (string-append "Hello" "world!"). It is also worth saying that there are a myriad of Lisp dialects. We will use Racket due to a convenient development environment, but almost all of the code will work with most dialects (you may need to use other functions to manipulate strings, etc.). All download links and installation instructions can be found on the site language.

λ-calculus

If you followed my advice, read about lambda calculus, you already know that there are three rules for a term in it:

• variable x , in Lisp is written in the same way, using the variable name;
• Lambda abstraction (λx.t) , can be written as a normal function, known to us from all programming languages: (define (fun x) t); or as a nameless lambda (lambda (x) t).
• the application (ts) is a normal function call, and this is what is recorded in the Racket (ts).

So, by declaring a function and calling it, we will try to write a type system and help us with the encoding of Church (you should have the Wikipedia tab open where it is written about it). As the author of the English-language article wrote, this encoding allows you to represent data types and operators in terms of lambda calculus. We will check it out.

The slight disadvantage of Lisp being chosen is that the function always requires you to give it all the arguments, rather than curry , as Haskell or ML, for example, does. Therefore, we will need to explicitly use lisp-lambda, or use the curry function. I will try to talk about it as needed.

Also in Racket some names we need are already reserved, so all our functions will be written with a capital letter.
We start development environment of DrRacket and go.

Boolean values

We start from Boolean values, they are True and False . In the beginning, their implementation may seem a bit strange - in lambda terms everything looks strange. In the future we will make sure that it works.

The Boolean data type for is of value to us only if we can distinguish them from each other. This can be done using the If operator (function). This type is already described on Wikipedia (all types are described there), and using Lisp we will transfer them to the editor.

(define (True ab) a) (define (False ab) b) (define (If cab) (cab)) 

Using the interactive interpreter Racket (located below in our IDE), we can test the performance of our boolean logic. Types are functions that take two arguments and return either the first (in the case of True) or the second (False). The If statement simply calls them with the correct branches:

 > (If True "first" "second") "first" > (If False "first" "second") "second" 

But that is not all. We are used to checking several conditions at the same time. Therefore, we need to expand our Boolean logic and introduce operators (we’re looking at Wikipedia again). Functions are not complicated. We write:

 (define (And pq) (pqp)) (define (Or pq) (ppq)) (define (Not p) (p False True)) 

Everything is simple: And the function, in case of successful completion of the first condition, checks the second; Or , if successful, returns itself; if unsuccessful, checks the second value; Not swaps predicates. Be sure to check:

 > (If (And True False) "first" "second") "second" > (If (And True True) "first" "second") "first" > (If (Or False True) "first" "second") "first" > (If (Or False False) "first" "second") "second" > (If (Or False (Not False)) "first" "second") "first" 

All, you can consider yourself experts lambda calculus. But we will not stop there. It is worth noting here that I will use the types we are used to for simplicity. Further, when we have enough of our types, we will operate with them. For now, we will use strings and numbers for illustration.

Integers

Natural numbers are numbers that are used for counting. We use Arabic numerals and decimal notation. But in fact, natural numbers themselves are a very interesting abstraction and are often cited as an example of using algebraic data types .

To represent numbers, we implement the so-called Church numerals (Church numbers). The number in this encoding is a function that takes the current value and the growth function. For example, in the case of ordinary arithmetic, it can be 3 and +1. In the end, applying the growth function N times to the initial value, we obtain the natural number that represents it. I do not want to use ordinary arithmetic to describe it. I'll show you why later.

We have already been sufficiently savvy in technical terms. It's time to start implementation. For illustration, we will use the usual representations of natural numbers: Arabic numerals and strings. For numbers, the growth function will be a function that adds a number to a unit ( PlusOne ), for strings - a concatenation function with another string, where as the other string we will have sticks "|", like in school ( Concat ):

 (define (Nil fx) x) (define (One fx) (fx)) (define (Two fx) (f (fx))) (define (PlusOne x) (+ 1 x)) (define (Concat x) (string-append x "|")) 

Here it becomes clear why I deliberately avoided using numbers when describing natural numbers. This is because the Church digits are self-contained values. If you try to enter 'Two' in the interpreter, you will see that the interpreter returns the lambda # <procedure: Two>. But, if you do not want to define with your hands the whole set of natural numbers, but you want to get a visual representation of the natural number, you need to pass in the parameters the function of increasing the value and the initial value. The proof for this is our interpreter:

 > Two #<procedure:Two> > (Two Concat "") "||" > (Two PlusOne 0) 2 

We declared 3 natural numbers in which the execution of the function is nested into each other. But it would be nice to use for example the number 99 to define 100, and not to write a hundred nested function calls. In this case, we are in a hurry to help the functions of the next and previous elements. We implement the functions and immediately rewrite our numbers:

 (define (Succ nfx) (f (nfx))) (define (Pred nfx) ((n (lambda (g) (lambda (h) (h (gf)))) (lambda (u) x)) (lambda (u) u))) (define (Null fx) x) (define (One fx) (Succ Null fx)) (define (Two fx) (Succ One fx)) (define (Three fx) (Succ Two fx)) (define (Four fx) (Succ Three fx)) (define (Five fx) (Succ Four fx)) 

The function of increasing the number is quite simple, but the reduction is more difficult. For the next in order number, we simply wrap the source with another function call. To take a predecessor, a function is used that skips the first use of the growth function in the chain of application of the function f .

It is obvious that in lambda calculus there should be arithmetic operations with natural numbers, otherwise they would not be numbers at all. See the Wikipedia page and rewrite:

 (define (Plus mn) (lambda (fx) (mf (nfx)))) (define (Minus mn) (lambda (fx) ((n (lambda (t) (lambda (rs) (Pred trs))) m) fx))) (define (MinusC mn) (lambda (fx) ((n (lambda (t) (curry Pred t)) m) fx))) (define (Mul mn) (lambda (fx) (m (lambda (y) (nfy)) x))) (define (IsZero n) (n (lambda (x) False) True)) (define (Eq mn) (IsZero (Minus mn))) 

Plus applies the function first n times, then another m. Minus applies the function of the previous element to the number to be reduced (you can use currying to get a more readable entry: MinusC ). The multiplication function m repeats n applications of the function. Check for zero: as is known IsZero returns its argument without using functions, then we get True, and all the numbers ignore their argument more and return False. The equality test makes subtraction and checks for zero (since we do not have negative numbers, we also need to check the other way). There is division and raising to a power too, but we will not implement them. They are on the page, try to write yourself. Now, with the help of operations, we can determine more numbers: tens and hundreds:

 (define (Ten fx) (Mul Five Two)) (define (Hundred fx) (Mul Ten Ten)) 

And draw a hundred sticks:

 > (Hundred Concat "") "||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||" > ((Plus Two (Mul Four Ten)) PlusOne 0) 42 > (IsZero Null) #<procedure:True> > (IsZero Two) #<procedure:False> > (Eq Two Two) #<procedure:True> > (Eq Two One) #<procedure:False> 

Couple

Let's continue with a couple of values. In lambda calculus, a pair is a function that closes two arguments and “waits” for a function, which can then be applied to these values. Obvious candidates for such functions are taking the first or second element:

 (define (Pair ab) (lambda (f) (fab))) (define (First p) (p (lambda (ab) a))) (define (Second p) (p (lambda (ab) b))) 

The access functions to the element take a pair and “feed” it a lambda, which returns the first or second argument, respectively. Checking:

 > (First (Pair "first" "second")) "first" > (Second (Pair "first" "second")) "second" 

With the help of the pair, we can implement many abstractions: for example lists and tuples.

Lists

Lists are the most frequently used and often studied collection in functional programming. In the already mentioned SICP booklet, the lists are reviewed in great detail. Actually “LISP” itself stands for Lis t P rocessing Language. Therefore, we will approach them with full responsibility and enthusiasm. On the Internet, you can often stumble upon a description of the lists in the style of lambda calculus.

Actually, the list is nothing more than a pair of values ​​(we already have a pair): the head element and the tail, which is a continuation of the list. Wikipedia describes 3 ways to encode lists:

• using a pair as an element. This allows the first element of the pair to store an indicator that the list is empty. This option is good because the function with elements is very simple - depending on the void indicator, you can perform the first or second function;
• using one element, and in the empty list store false. In this case, the list view has a shorter record, but the work is a bit more complicated than in the first case;
• define a list using the right convolution function . It does not suit us, because it is difficult.

We will choose the first option, so it is the most obvious. To output the elements of the list, use the Lisp function 'display', which outputs its argument to the terminal. Additionally, we define the output function for numbers and sticks. Let me remind you that each item in our list is another pair, where the first item is True if the list is empty and False if it contains a meaningful item. Rewrite:

 (define (NatToNumber m) (display (m PlusOne 0))) (define (NatToString m) (display (m Concat ""))) ; ... (define (Nil) (Pair True True)) (define (IsNil) First) (define (Cons ht) (Pair False (Pair ht))) (define (Head l) (First (Second l))) (define (Tail l) (Second (Second l))) (define (ProcessList lf) ((If (IsNil l) (lambda ()(void)) (lambda ()(f (Head l)))))) (define (ConsZeroList n) (n (lambda (l) (Cons Null l)) (Nil))) (define (ConsRangeList n) (Second (n (lambda (p) (Pair (Minus (First p) One) (Cons (First p) (Second p)))) (Pair n (Nil))))) 

While we do not know how to iterate through the list, because we do not know how to do recursion. Therefore, all we have to do is manually sort through the elements and work with them. The ProcessList function applies the passed argument function to the current head element, or does nothing if the list is empty. It is worth noting that the normal order is used in the lambda calculus. This means that the functions first wrap their arguments, and then they are executed. In Lisp, the applicative order is used — the function arguments are evaluated before being passed. In the body of the ProcessList function when checking with If, we don’t want to execute both branches at the same time, so we have to transfer lambdas to the execution branches and call the one that comes back after the check. ConsZeroList creates a list of zeros, the required length, and ConsRangeList creates a list from a sequence of numbers. They are based on the repeated use by the natural number of a function over an element. Check in the interpreter:

 > (define L1 (Cons One (Cons Two (Cons Three (Nil))))) > (ProcessList L1 NatToNumber) 1 > (ProcessList (Tail (Tail L1)) NatToNumber) 3 > (ProcessList (Tail (Tail (Tail L1))) NatToNumber) > 

Y-combinator

So, we have reached the apogee of our article. In order to process the entire list, we need to be iterated on it. At the moment we do not know how to do it. And this can be done using Y-combinator , aka Fixed-point combinator, aka fixed point combinator. To understand why it is so called, you need to read a lot of text. It is enough for us to know that if to transfer the function to it, it will transfer itself to the first argument of the function. With this we can recursively perform operations on objects (for example, lists).

The Y-combinator is very well explained in Mike Venier's article . Wikipedia has a precise definition of a combinator. In the above article, there is a Lisp code. We need a function for applicative order. Just rewriting. In the same place, we look at the factorial calculation function, which we can rewrite for our natural numbers:

 (define (Y f) ((lambda (x) (xx)) (lambda (x) (f (lambda (y) ((xx) y)))))) (define (Fac n) ((Y (lambda (f) (lambda (m) ((If (Eq m Null) (lambda () One) (lambda () (Mul m (f (Minus m One))))))))) n)) 

Check the result. The factorial of ten, due to the fact that our function creates almost 4 million lambdas, and then executes them, is calculated for a rather long time:

 > (NatToNumber (Fac Five)) 120 > (NatToNumber (Fac Ten)) 3628800 

Now take up the lists. With the help of the Y-combinator, we implement the favorite trinity of functions for list processing: Map, Filter, Reduce; and a function for output:

 ;Lists (define (PrintList l) (display "[") ((Y (lambda (r) (lambda (m) ((If (IsNil m) void (lambda () (NatToNumber (Head m)) (display ", ") (r (Tail m)))))))) l) (display "]")) (define (Map lf) ((Y (lambda (r) (lambda (m) ((If (IsNil m) Nil (lambda () (Cons (f (Head m)) (r (Tail m))))))))) l)) (define (Filter lf) ((Y (lambda (r) (lambda (m) ((If (IsNil m) Nil (lambda () ((If (f (Head m)) (lambda () (Cons (Head m) (r (Tail m) f))) (lambda () (r (Tail m) f)))))))))) l)) (define (Reduce lfz) ((Y (lambda (r) (lambda (m) ((If (IsNil m) z (lambda () (f (Head m) (r (Tail m) fz)))))))) l)) 

The implementation of these functions is described in many articles, so I will not talk a lot about them. Better apply them in practice:

 > (PrintList (ConsRangeList Ten)) [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, ] > (PrintList (Map (ConsRangeList Ten) (lambda (x) (Plus x One)))) [2, 3, 4, 5, 6, 7, 8, 9, 10, 11, ] > (PrintList (ConsZeroList Ten)) [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ] > (PrintList (Map (ConsZeroList Ten) (lambda (x) (Plus x Hundred)))) [100, 100, 100, 100, 100, 100, 100, 100, 100, 100, ] > (PrintList (Filter (ConsRangeList Ten) (lambda (x) (Not (Eq x Five))))) [1, 2, 3, 4, 6, 7, 8, 9, 10, ] > (NatToNumber (Reduce (ConsRangeList Ten) (lambda (xy) (Plus xy)) Null)) 55 > (NatToNumber (Reduce (ConsZeroList Ten) (lambda (xy) (Plus xy)) Null)) 0 

Epilogue

So, using only the functions we were able to implement everything that a regular functionary needs for programming. I hope you liked the material. Lambda calculus deserves to be at least familiar with it. For 30 years, functional languages ​​have been predicted to kill the PLO and imperative languages. But today more and more is created by the multi-programming language. Perhaps that is why Haskell never became widespread.

Nevertheless, the mathematical beauty of the lambda calculus will attract programmers of all specialties for many decades.

All code can be viewed / downloaded on github .

UPD: In the comments mapron remembered a similar publication with a code in Javascript.