## DEV Community

hungle00

Posted on • Updated on

# Lambda Calculus - Represent in Clojure

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

``````(fn [x] y)
``````

Function application: `(f e)` means the applied function f to e. It has a similar form in Clojure:

``````(f e)
``````

Let's explore some other λ expressions:

• `λx.x` called the identity function.
``````(fn [x] x)
``````
• Applied identity function above to `a` we have `(λx.x a)`:
``````((fn [x] x) a)
``````
• `(λ f. λ x. f x)` equivalent to:
``````(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.

``````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:

``````(def comp
(fn [f g]
(fn [x] (f (g x)))))

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

;; => 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.

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

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

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

``````;; 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:

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