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

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

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

More resources

• Henri Borges'article Functions Describe the World
• Lambda calculus represented in both Clojure and Elixir: https://hungle00.github.io/content.html?id=15
• Matthew Might's work on FP and Lambda calculus is amazing.