λ calculus and LISP


A typical lover of λ-calculus.

Once, surfing the Internet, I came across the news of the lisp-like, embedded Shen programming language . Previously, they had a sample Lisp code on their home page. In the example, the authors describe an abstract collection and functions for working with them.

It just so happened that I was 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 applicants, and everything must be implemented without fail in terms of Church encoding.

I was very superficially familiar with lambda calculus, since almost always 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 OOP to the dark side .

If Lisp doesn't scare you, there are a lot of lambdas and y-combinator (not the one with the news),

Introduction


The article does not purport to cover the entire material or replace SICP . I am not a mathematician, much less a connoisseur of lambda calculus. The only thing she claims is linearity. The text sets the task of introducing readers to functions as first-class citizens and making it as interesting as possible for lambda calculus. In the process of writing the code, I will try to explain what happens in a language that is understandable to simple engineers.

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

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


Good old joke

On Habré there are some articles about lambda calculus. For example here and here . Some of them reveal the theory more broadly than I try to do, so I would advise reading at least one of them to understand what we are going to do. I will not give the whole theory here, so as not to complicate the article. To write our abstractions, we will have enough Wikipedia articles (all real programmers write programs this way). English-language articles cover the topic more widely, so you can use articles about Lambda Calculus and a more detailed article describing the encoding of Church Encoding types .

We also need to know the LISP programming language. But don’t worry if you don’t 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 reduce the recording, several functions. It is enough to know that in Lisp, in order to execute a function, you need to enclose its call in brackets in which the first argument will be the name of the function, and parameters will follow it (very similar to the 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 racketdue to the 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 language website.

λ calculus


If you followed my advice and read about lambda calculus, you already know that it has three rules for the term:
  • variable x , in Lisp is written in the same way, using the variable name;
  • lambda abstraction (λx.t) , can be written as an ordinary function, known to us from all programming languages: (define (fun x) t); or as an unnamed lambda (lambda (x) t).
  • application (ts) , this is a normal function call, it is written in the Racket (ts).

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

A small drawback of what Lisp chose was that the function always requires all arguments to be supplied to it, rather than currying , like Haskell or ML does. Therefore, we will need to explicitly use lisp lambdas, or use the curry function. I will try to talk about it as needed.

Also in Racket some of the names we need are already reserved, so all our functions will be written to write with a capital letter.
We launch the development environment DrRacket and let's go.

Boolean values


We start from Boolean values, they are True and False . At first, their implementation may seem a little strange - in lambda terms, everything looks strange. In the future, we will make sure that this 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 statement (function) . This type has already been described on Wikipedia (all types are described there), and using Lisp, we will transfer them to the editor.

(define (True a b) a)
(define (False a b) b)
(define (If c a b) (c a b)) 

Using the interactive Racket interpreter (located at the bottom of our IDE), we can test the functionality 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 desired 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 (again, we look at Wikipedia). Functions are not complicated. We write:

(define (And p q) (p q p))
(define (Or p q) (p p q))
(define (Not p) (p False True))

Everything is simple here: And the function, if the first condition is successfully passed, 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"

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

Integers


Natural numbers are numbers that are used for counting. We use Arabic numbers 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. Ultimately, applying the growth function N times to the initial value, we get a natural number that represents it. I do not want to use ordinary arithmetic to describe. Next I will show why.

We are already quite savvy in technical terms. It's time to get started. To illustrate, we will use the usual representation of natural numbers: Arabic numbers and strings. For numbers, the growth function will be a function that adds a number with a unit ( PlusOne ), for strings, a concatenation function with another string, where we will have "|" sticks as another string, as in school ( Concat ):

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

Here it becomes clear why I deliberately avoided the use of numbers in the description of natural numbers. This is because Church numbers are self-contained values. If you try to enter 'Two' in the interpreter, you will see that the interpreter returns a lambda #. But, if you don’t want to manually determine the whole set of natural numbers, but want to get a visual representation of a natural number, you need to pass the function of increasing the value and the initial value in the parameters to it. The proof for this is our interpreter:

> Two
#
> (Two Concat "")
"||"
> (Two PlusOne 0)
2

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

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

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

Obviously, in lambda calculus arithmetic operations with natural numbers must exist, otherwise they would not be numbers at all. We look at the Wikipedia page and rewrite:

(define (Plus m n) (lambda (f x) (m f (n f x))))
(define (Minus m n) (lambda (f x) ((n (lambda (t) (lambda (r s) (Pred t r s))) m) f x)))
(define (MinusC m n) (lambda (f x) ((n (lambda (t) (curry Pred t)) m) f x)))
(define (Mul m n) (lambda (f x) (m (lambda (y) (n f y)) x)))
(define (IsZero n) (n (lambda (x) False) True))
(define (Eq m n) (IsZero (Minus m n)))

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 record: MinusC ). The multiplication function m repeats n times the application of the function. Zero Check: IsZero Knownreturns its argument without using a function, then we get True, and all numbers ignore their argument more and return False. The equality check does a subtraction and checks for zero (since we don’t have negative numbers, we need to check the other way too). There is division and exponentiation 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 larger numbers: tens and hundreds:

(define (Ten f x) (Mul Five Two))
(define (Hundred f x) (Mul Ten Ten))

And draw a hundred sticks:

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


Couple


We continue with a pair of values. In the lambda calculus, steam is a function that closes two arguments and “waits” for a function that it can then apply to these values. Obvious candidates for such functions are taking the first or second element:

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

The element access functions take a pair and feed them a lambda, which returns the first or second argument, respectively. We check:

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

With a pair, we can implement many abstractions: for example lists and tuples.

Lists


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

Actually, a list is nothing more than a pair of values ​​(we already have a pair): the head element and the tail, it is also a continuation of the list. Wikipedia describes 3 ways to encode lists:
  • using a pair as an element. This allows you to store the first element of the pair indicator that the list is empty. This option is good in that the function with the elements is very simple - depending on the void indicator, you can execute the first or second function;
  • using a single element, and store false in an empty list. In this case, the list view has shorter entries, 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 complicated.

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

(define (NatToNumber m) (display (m PlusOne 0)))
(define (NatToString m) (display (m Concat "")))
; ...
(define (Nil) (Pair True True))
(define (IsNil) First)
(define (Cons h t) (Pair False (Pair h t)))
(define (Head l) (First (Second l)))
(define (Tail l) (Second (Second l)))
(define (ProcessList l f) ((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 over the list, because we do not know how to do recursion. Therefore, all that remains for us is to 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 in the lambda calculus normal order is used . This means that functions first wrap their arguments and then execute. In Lisp, the applicative order is used - the arguments of the function are evaluated before being passed. In the body of the ProcessList functionwhen checking with If, we don’t want to execute both branches at the same time, so we have to pass lambdas to the execution branches and call the one that returns after the check. ConsZeroList creates a list of zeros the required lengths, and ConsRangeList creates a list of sequences of numbers. They are based on the repeated use by a 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 peak of our article. In order to process the entire list, we need to iterate over it. At the moment, we do not know how to do this. 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 you pass a function to him, he will pass on to himself as the first argument to the function. With this, we can recursively perform operations on objects (such as lists).

The Y-combinator is very well explained in an article by Mike Wenier. Wikipedia has an exact definition of combinator. The above article has Lisp code. We need a function for applicative order. Just rewriting. We will also look at the factorial calculation function, which we can rewrite for our natural numbers:

(define (Y f) ((lambda (x) (x x)) (lambda (x) (f (lambda (y) ((x x) 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 let's get down to the lists. Using the Y-combinator, we implement the beloved trinity of functions for processing lists: Map, Filter, Reduce; and 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 l f)
  ((Y 
    (lambda (r)
      (lambda (m)
        ((If (IsNil m)
          Nil
          (lambda () (Cons (f (Head m)) (r (Tail m))))))))) l))
(define (Filter l f)
  ((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 l f z)
  ((Y 
    (lambda (r)
      (lambda (m)
        ((If (IsNil m) z
          (lambda () (f (Head m) (r (Tail m) f z)))))))) l))

The implementation of these functions is described in many articles, so I will not talk much about them. Better put them into 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 (x y) (Plus x y)) Null))
55
> (NatToNumber (Reduce (ConsZeroList Ten) (lambda (x y) (Plus x y)) Null))
0


Epilogue


So, using functions only, we were able to implement everything that an ordinary functional worker needs for programming. I hope that I liked the material. Lambda calculus deserves to at least become familiar with it. For 30 years now, functional languages ​​have been prophesied of killing OOP and imperative languages. But today, more and more is being created by a multi-paradigm programming language. Perhaps that is why Haskell did not become widespread.

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

All code can be viewed / downloaded on github .

UPD: In the comments, mapron recalled a similar post with Javascript code.

Also popular now: