I'm going to teach you the basics of Lambda Calculus really quickly.
Lambda Calculus is deep. But I'm covering only the fundamentals here.
What is Lambda Calculus?
Lambda Calculus (LC) is a model to describe computations.
LC describes the syntax and semantics.
Syntax
A lambda expression (also known as lambda term) can be one of the following three things:
 Variable
 Application
 Abstraction
Variable
A variable is just a string. For example:

Traditional:
x

Programmerfriendly
company_id
Application
Application (aka function application) is applying one term to another.
To introduce an application, simply separate two terms by a space (and use parentheses appropriately).
An application can be simple:

Traditional:
f x

Programmerfriendly
employees_of company_id
Or more involved

Traditional:
f (g x) (h x)

Programmerfriendly
find_by_id (get map (entry key)) (hash id)
⚠️ Parentheses matter!
f (g x)
is not the same as(f g) x
!
Abstraction
Abstraction (aka anonymous function) is a way to introduce functions in Lambda Calculus.
To introduce an abstraction, write the Greek letter λ
followed by the variable name, a dot .
and a body of a function.
The variable after λ is known to be bound.

Traditional:
λx.f x

Programmerfriendly
λcompany_id.employees_of company_id
Abstractions can be nested:

Traditional:
λx.λy.f x y

Programmerfriendly
λcompany_id.λcount.has_at_least (employees_of company_id) count
Semantics
LC is not just about a fancy way to write functions and their arguments. It also attaches semantics to terms. Specifically:
 Rename a bound variable (known as αconversion)
 Apply a function to its arguments (known as βreduction)
Renaming (αconversion)
The idea is simple. If you rename a local variable of a function, the behaviour of this function doesn't change.
Terms on both sides of =
are equal in the following examples:

Traditional:
λx.f (g x) (h x) = λy.f (g y) (h y)

Programmerfriendly
λcompany_id.size company_id = λcompanyId.size companyId
Applying (βreduction)
Function application takes an abstraction and applies it to its argument by replacing a bound variable with the argument.
It's implemented as a simple string searchandreplace. Evaluating a function has never been simpler!
I'm using the =>
operator here with the meaning reduces to.

Traditional:
(λx.f x) y => f y

Programmerfriendly
(λcompany_id.size company_id) bloomberg => size bloomberg
⚠️ You can see that parentheses matter here as well!
λx.f x y
is not the same as(λx.f x) y
!💎 Bonus! One lambda term is especially popular, it even has its own name Ωcombinator
(λx.x x) (λx.x x)
It represents infinite recursion because betareducing this term returns the term itself.
As you can see, the basics of Lambda Calculus are pretty simple but turns out, they're powerful enough to describe any possible computation. Although, it might not provide the most efficient way to compute things.
Practice
Now that we learned the theory, it's time to do some practice!
The following sections provide exercises for you to implement a simple program to work with LC. Solutions in OCaml are provided as well.
⚠️ Implementing the following exercises may take longer than 10 minutes, so don't worry!
Modeling Lambda Calculus
First of all, let's define a type to model a term in Lambda Calculus. Remember, it can be either a variable name, an application of two terms or a lambdaabstraction.
Exercise 1. Create a data type to describe a term in Lambda Calculus.
Solution in OCaml
This is nicely modelled with sum types:
type expr =
 Var of string
 App of expr * expr
 Lam of string * expr
Example of terms in both LC and OCaml:
Lambda Calculus  OCaml 

x  Var "x" 
f x  App (Var "f", Var "x") 
λx.f x  Lam ("x", App (Var "f", Var "x")) 
Prettyprinting
Now that we have a type, let's implement a function to display a value of our type nicely.
Exercise 2. Implement a prettyprinting function for Lambda Calculus.
Solution in OCaml
A simple solution in OCaml (that may produce some redundant parentheses) uses just pattern matching,
printf
and recursion.let rec pretty = function
 Var x > x
 App (l, r) > Printf.sprintf "(%s) (%s)" (pretty l) (pretty r)
 Lam (x, body) > Printf.sprintf "λ%s.(%s)" x (pretty body)
Parsing
And the most difficult part (that made me ignore FP for 3 (!) years when I first tried to implement it).
Can we go backwards? Can we parse a string to a value of our type?
Exercise 3. Implement a parser for Lambda Calculus.
Solution in OCaml
Here I'm using the Parser Combinators approach provided by the wonderful angstrom OCaml library.
Parser Combinators deserve a separate blog post, so here I'm just presenting the full code without comments.
open Angstrom
let parens_p p = char '(' *> p <* char ')'
let name_p =
take_while1 (function 'a' .. 'z' > true  _ > false)
let var_p = name_p >> (fun name > Var name)
let app_p expr_p =
let ( let* ) = (>>=) in
let* l = parens_p expr_p in
let* _ = char ' ' in
let* r = parens_p expr_p in
return (App (l, r))
let lam_p expr_p =
let ( let* ) = (>>=) in
let* _ = string "λ" in
let* var = name_p in
let* _ = char '.' in
let* body = parens_p expr_p in
return (Lam (var, body))
let expr_p: expr t =
fix (fun expr_p >
var_p <> app_p expr_p <> lam_p expr_p <> parens_p expr_p
)
let parse str =
match parse_string ~consume:All expr_p str with
 Ok expr > Printf.printf "Success: %s\n%!" (pretty expr)
 Error msg > failwith msg
The full working OCaml code can be found here:
What's next?
I hope this blog post helped you to learn the basics of Lambda Calculus!
At least now, when you hear these words, you'll know their meaning.
If you feel like you want to take on some challenge, you can try to implement αconversion and βreduction for your simple Lambda Calculus language!
And most importantly, have fun!
If you liked this blog post, consider following me on YouTube, X (formerly known as Twitter) or sponsoring my work on GitHub
Top comments (7)
And with
rectypes
it's the (eager) untyped lambda calculus.Sounds like too advanced OCaml feature for an intro blog post 😅
Excellent post helped me a lot, decide to solve the challenge in rust
github.com/z4nder/lambdacalculus
Really nice solution!
exciting! but you need to read it several times to understand the material
Thanks! It makes sense. Getting familiar is one thing but fully understanding the concept to the level of being able to explain it to someone else is another.
Do Calculus parameters and formulas have to be
so cryptic. They really do model programming
Languages.