Lambda Calculus - Represent in Clojure
Tags: clojure, lambdacalculus, functional
Published: 2023-11-12 15:56:24

Recently, I've been spending my free time learning functional programming. To understand comprehensively about functional programming, it is need to mention Lambda Calculus - a completed computation model for functional programming. 

I am a developer and didn't have Lambda Calculus academic training, so at the beginning, I was very confused about some concepts. From my perspective, trying to implement it in a specific programming language makes it much easier to understand and explain to someone else. I chose Clojure for this purpose because it is a Lisp dialect language and has coherence and elegance of design.
This post just focuses on representing λ-calculus in Clojure. I suppose that you have basic knowledge about λ-calculus, if not, try to read [Lambda Calculus theory](https://eecs390.github.io/notes/theory.html) or search on Wikipedia.

## Some basic λ expressions
**Function abstraction**: All functions of the lambda calculus are anonymous and only take one parameter.   
For example: `λx.e` function accepts an argument x and returns the value of y. In Clojure, we'd write this as:
``` clojure
(fn [x] y)
```
**Function application**:   `(f e)` means the applied function f to e.  It has a similar form in Clojure:
``` clojure
(f e)
```
Let's explore some other λ expressions:
- `λx.x` called the identity function.
``` clojure
(fn [x] x)
```
- Applied identity function above to `a` we have `(λx.x a)`:
```clojure
((fn [x] x) a)
```
- `(λ f. λ x. f x)` equivalent to:
```clojure
(fn [f] (fn [x] (f x))
```


**Function composition**
This function takes 2 functions as arguments and returns a function that is the composition of those.
```clojure
comp = λg. λf. λx. g (f x)
```
Now we'll write Clojure code to represent `comp` function and define 2 functions `add` and `subtract` for testing. In Clojure:
```clojure
(def comp
  (fn [f g]
    (fn [x] (f (g x)))))

(def add (fn [n] (+ n 2)))
(def subtract (fn [n] (- n 4)))

((comp add subtract) 8)
;; => 6
```
In the next part, I'll introduce Church encoding - a tool for representing numbers, booleans, conditionals, and data structures in Lambda Calculus

## Church encoding
Church encoding, in Lambda calculus, is a way to encode data and operators using only a combination of anonymous functions.

### Booleans
Let's define an abstraction for the booleans.
```
true = λx. λy. x
false = λx. λy. y
```
These functions receive two arguments and, If `true`, the first argument is returned. If `false`, the second argument is returned.
``` clojure
(def fst (fn [x y] x))
(def snd (fn [x y] y))
```
### Pair
```
pair = λx. λy. λf. f xy
```
The **pair** function takes two arguments x and y and returns a function that contains x and y in its body.  
In Clojure, this term is equivalent to:
```clojure
(def pair (fn [x t]
  (fn [func] (func x t))))
```
Given a pair, we can extract the first and second items using selection functions - these functions with similar form to boolean functions above.
Clojure code:
```clojure
(def fst (fn [a b] a))
(def snd (fn [a b] b))

((pair 3 5) fst))  ;; => 3
((pair 3 5) snd))  ;; => 5
```

## Numerals
A Church numeral applies its first argument to its second argument n times. For example, the definition of numbers from 0-3 in λ-Calculus:
```
0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))
```
In summary, the definition of the numeral n is the application of a given function f n times to a given value.
``` clojure
;; 0
(def zero (fn [f] (fn [x] x)))
;; 1
(def one (fn [f] (fn [x] (f x))))
;; 2
(def two (fn [f] (fn [x] (f (f x)))))
```
We can define a `succ` function, which takes a Church numeral n and returns n + 1 by applying f to x one more time than the original number
```
succ = λn.λf.λx.f (n f x)
```
We'll try the function by applying function `two` defined before and check the result:
```clojure
(def succ (fn [n]
            (fn [f]
              (fn [x]
                (f ((n f) x))))))

;; helper function to-int helps us check numerals
(def to-int  (fn [n]
               ((n (fn [i]
                     (+ i 1))) 0)))
(to-int (succ two)) ;; => 3
(to-int (succ (succ two))) ;; => 4
```

There are more exercises in Church encoding, how to express conditional expressions, arithmetic operations, lists, etc and you can define them by yourself.

## More resources
- Henri Borges'article [Functions Describe the World
](https://dev.to/hnrbs/functions-describe-the-world-2cj)
- Lambda calculus represented in both Clojure and Elixir: https://hungle00.github.io/content.html?id=15
- [Matthew Might's work](https://matt.might.net/articles/implementing-a-programming-language/) on FP and Lambda calculus is amazing.