λ-calculus and LISP

Typical Amateur λ-calculus.

One day, while surfing on the Internet, I came across the news about listopadovka, embeddable programming language Shen. Before their home page was hanging the sample code in Lisp. In the example, the authors describe an abstract collection of functions and work with them.

It just so happened that I am a secret admirer of the functional programming, and thus, to some extent, the lambda calculus, which consists almost entirely of abstractions. I wanted to write something as abstract and that would make the task easier, I decided that built-in data types is for the weak appliers, and implement all imperative in terms of the encoding of the Church.

With lambda calculus, I knew very superficially, as is almost always the articles on the mathematics section consists entirely of formulas that do not try in practice, not possible. So I decided to deal with it in practice, and perhaps draw on the dark side of the force adepts Turing machine OOP.

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

the

Introduction

The article is not intended to be complete coverage of the material, or to replace SICP. I am not a mathematician and certainly not an expert lambda calculus. The only thing it claims is the linearity of the presentation. In the text the task is to acquaint readers with functions such as first-class citizens and make it as interesting for the lambda calculus form. In the process of writing code, I'll try to explain what happen understandable to the engineers language.

Today, the trend is much borrowing of concepts from functional programming imperative languages (even in C++ after 30 years, the Committee went to such an adventurous act. And Yes, Java 8 at), so there is hope that someone this article useful. Of course, if on Habre there are fans of lambda calculus, which I will be able to improve, add comments.

So, "why was I chosen Lisp" you ask. There are several reasons. The first is that all the examples in the articles about functional programming, written in Haskell'E. the Second is the already mentioned book: Structure and Interpretation of Computer Programs, which is one of my favorite books and one I recommend to read to all who haven't done it yet. Third, because Lisp is for real hackers.


Old joke

On Habre there some articles about the lambda calculus. For example here and here. Some of them reveal the theory is broader than try to do it, so I would advise to read at least one of them for understanding what we are going to do. I shall not quote all the theory in order not to complicate the article. For writing our abstractions, we will have enough articles on Wikipedia (all real programmers write programs). English articles wider open, so you can use the articles on Lambda Calculus and a more detailed article describing the encoding of types Church Encoding.

We also need to know the programming language LISP. But don't worry if You don't know, because the syntax consists of the parentheses, we'll pick it up. What we need to know how the lambda Terme, written in Lisp, and a little later, to reduce entry multiple functions. Enough to know that in Lisp to make the function, you need to enclose it in brackets, where the first argument is the name of the function, and it will go to the settings (very similar to Polish notation). That is, for calculating the sum you need to write (+ 2 3) to merge rows (string-append "Hello" "world!"). It is also worth to say that there are countless dialects of Lisp. We will use Racket because of the convenient development environment, but almost all of the code will work with most dialects (may need to use other functions for manipulation of strings, etc.). All download links and installation instructions You can find on the website of the language.br> the

λ-calculus

If You followed my advice read about the lambda calculus, you already know that there are three rules for the term
the

the
• variable x in Lisp is written exactly the same by using the name of the variable.
the
• lambda abstraction (λx.t), can be written as an ordinary function, we know from all programming languages: (define (fun x) t); or as a nameless lambda (lambda (x) t).
the
• applique (t s), is a normal function call Racket'e and is written (t s).

So, with the help of the function Declaration and call, we will try to write a type system and will help us in the coding of the Church (You must have a tab open with Wikipedia, where it is written). As the author wrote the English article, this encoding allows to represent data types and operators in terms of the lambda calculus. We will check it.

Small flaw that was chosen Lisp that the function is always requires to provide arguments, not carraroe how does such as Haskell or ML. We will therefore need to explicitly use the lisp lambda, or use a curry function. I'll try to talk about this as needed.

Also, the Racket is already reserved, we need some names, so all of our functions will be to write to write with a capital letter.
Start the development environment is DrRacket and went.

the

Boolean values

We start from the Boolean values, they are True and False. At first they can seem a little strange – in the lambda calculus, everything looks weird. In the future we will make sure it works.

The Boolean data type is of value to us only if we will be able to distinguish them from each other. This can be done with the help of the operator (function) If. Wikipedia already described this type (where all the types described), and we are using Lisp, and get them in the editor.

the

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

Using the interactive interpreter Racket (located at the bottom in our IDE), we can check the performance of our Boolean logic. Types are functions that take two arguments and return either the first (if True) or second (False). The If statement just calls them with the necessary branches:

the

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

But that's not all. We used to check for multiple conditions at the same time. Therefore, we need to expand our bolevoy logic and to enter operators (again peeks at Wikipedia). Functions are not complicated. Write:

the

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

Everything is simple: And function in the case of successful completion of the first condition checks the second; Or if successful, returns itself in case of failed checks and the second value; Not changes the predicate places. Be sure to check:

the

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

All can consider themselves connoisseurs of the lambda calculus. But we will not stop at that. It is worth noting that I will use our usual types for simplicity. Further, when we have enough of their types, we will operate with them. While we use strings and numbers to illustrate.

the

Natural numbers

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

To represent numbers we are implementing the so-called Church numerals (numbers of Church). A number in this encoding is a function that takes the current value and growth function. For example, in the case of conventional arithmetic it can be 3 and 1. Ultimately, by applying to the initial value of the growth function N times, obtain the natural number that it represents. I don't want to use to describe ordinary arithmetic. Then I will show why.
We are already quite savvy technically. It is time to begin implementation. For illustration we will use our customary representation of natural numbers: Arabic numerals and strings. For numbers a function of growth will be a function that adds number to the unit (PlusOne) for strings concatenation with another string, another string we will have sticks "|", like in school (Concat):

the

(define (f x Nil) x)
(define (One f x) (f x))
(define (Two f x) (f (f x)))

(define (PlusOne x) (+ x 1))
(define (Concat x) (string-append x "|"))

Then it becomes clear why I intentionally shied away from using numbers in the description of natural numbers. This is because the numbers of the Church are self-contained values. If you try in the shell enter 'Two', you will see that the interpreter returns lambda #<procedure:Two>. But, if you do not want to define hands all the set of natural numbers, but want to get a visual representation of a natural number, you need to pass in parameters to the function increment and initial value. The proof for this is our interpreter:

the

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

We have declared 3 integers, which the function nested within each other. But it would be nice to use for example the number 99 that would determine 100, instead of writing hundred of nested function calls. In this case, we rush to the aid of the functions next and previous elements. Implement functions and immediately rewrite our numbers:

the

(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) (f x Succ Null)) 
(define (Two f x) (f x Succ One))
(define (Three x f) (f x Succ Two))
(define (Four f x) (f x Succ Three))
(define (Five f x) (f x Succ Four)) 

The function of increasing the number of fairly straightforward, but reduction is more difficult. For the next number, we simply wrap the original another function call. To take the predecessor function is used, which transmits the first application of the functionality of the growth in the chain applying a function f.

It is obvious that in lambda calculus must exist arithmetic operations with natural numbers, otherwise it would not be numbers at all. Look at the Wikipedia page and copied:

the

(define (Plus m n) (lambda (f x) (m f (n f x))))
(define (Minus n m) (lambda (f x) ((n (lambda (t) (lambda (r s) (r s t Pred))) 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 n m) (IsZero (Minus m n)))

Plus applies a function n times first, then another m. Minus applies the function to the previous element to umershemu number (you can use currying to get a more readable entry: MinusC). The multiplication function m times repeats n applications of the function. Check for zero: IsZero returns its argument without applying the function, then you get True, and all numbers greater than ignore its argument and return False. Test for equality makes a subtraction and checks for zero (since we don't have negative numbers, you need the other side too to check). Division and exponentiation are also there, but we will not implement anything. They are on a page, try to write yourself. Now with the help of operations, we can define the numbers: tens and hundreds:

the

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

And draw a hundred sticks:

the

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

the

Couple

Let's continue by a pair of values. In lambda calculus a pair is a function that closes two arguments and "waiting" function, which can then be applied to these values. Obvious candidates for such functions is the capture of the first or second element:

the

(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

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

Using pairs we can implement many abstractions: for example, lists and tuples.

the

Lists

Lists the most commonly used and frequently studied collection in functional programming. In the already mentioned book SICP, lists discussed in great detail. He actually "LISP" stands for List Processing Language. So for them we come 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 (a pair we already have): the head element and tail, he is a continuation of the list. Wikipedia describes 3 ways to encode lists:
the

the
• with the use of a pair as an element. This allows you to store the first element of the pair indicates that the list is empty. This option is good in that the function elements are very simple – depending on the indicator of the void can be executed first or the second function;
the
• with the use of a single element and an empty list to store false. In that case, the list view has a shorter record, but work a little harder than in the first case;
the
• to define the list using right convolution. To us it is not suitable, because it is complicated.

We will choose the first option because it is the most visible. To output list items, use the Lisp function 'display' that displays its argument to the terminal. Additionally, we define an output function for numbers and sticks. Recall 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:

the

(define (NatToNumber m) (display (m PlusOne 0)))
(define (NatToString m) (display (Concat m "")))
; ...
(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 through the list, because we don't know how to do recursion. So all we can do is to manually loop through the elements and work with them. The ProcessList applies to the current head element of the passed function argument, or does nothing if the list is empty. It is worth noting that in the lambda calculus is used normal order. This means that the functions of the first wrap their arguments, and then executed. In Lisp it is used applicative order – function arguments are evaluated before to be transferred. In the body of the function ProcessList when checking with If we don't want to execute both branches simultaneously, so you'll have to transfer to branch the execution of a lambda and call that, which will be returned after verification. ConsZeroList creates a list of zeros required long and ConsRangeList creates a list of sequence numbers. They are based on the repeated application of natural number functions over the element. Check in the interpreter:

the

> (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)
>

the

Y-combinator

So, we've reached the climax of our article. In order to process the whole list, we need to iterate through it. At the moment we don't know how to do it. And this can be done using Y-combinator, he also Fixed-point combinator, he's a fixed point Combinator. To understand why it's called that, need to read lots of text. It is enough to know that if he transfer function, the first argument of the function it will give the very same yourself. Using this we can recursively perform operations on objects (such as lists).
Y-Combinator is very well explained in the article Mike veigné. Wikipedia has an accurate definition of the Combinator. In the above article there is code in Lisp. We need a function for applicative order. Just rewrite. There peeped a function to compute the factorial, which we can rewrite under our natural numbers:

the

(define (Y f) ((lambda (x) (x x)) (lambda (x) (f (lambda (y) ((x x) y))))))

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

Will check the result. The factorial of ten, in consequence of the fact that our function creates nearly 4 million lambdas, and then performs them, is calculated for a long time:

the

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

Now take the lists. With the help of Y-Combinator, we realize everyone's favorite trio of functions for processing lists: Map, Filter, and Reduce; and a function for output:

the

;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 f l)
((Y 
(lambda (r)
(lambda (m)
((If (IsNil m)
Nil
(lambda () (Cons (f (Head m)) (r (Tail m))))))))) l))

(define (Filter f l)
((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 f l 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 article, so I will not be a lot to tell. Better apply them in practice:

the

> (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

the

epilogue

So, using only the functions we were able to implement everything you need ordinary functionality for programming. I hope that the material I liked. Lambda calculus deserves at least to read it. For 30 years, functional languages are predicting the murder of OOP and imperative languages. But today, more and more is created multiparadigmatic programming language. Perhaps this is why, Haskell never became widespread.

However, the mathematical beauty inherent in lambda calculus have many decades will attract programmers of all disciplines.

The entire code can be viewed/download at github.

UPD: IN comments mapron remembered similar publication code in Javascript.

Article based on information from habrahabr.ru