Exploring Lambda Calculus, Part 1

Posted on July 5, 2017
Tags: lambda calculus, functional programming, elixir, haskell, python

Contents

Motivation

I’ve been reading through Greg Michaelson’s An Introduction to Functional Programming Through Lambda Calculus 1 off and on for the better part of a year now. Prior to starting the book, I’d picked up pieces of lambda calculus ad hoc, but I wanted to really take a step back and learn about lambda calculus from first principles.

This post, and a few to come, are from notes and examples put together while reading the book. To help synthesize the concepts and make them easier to understand, I’ve written the examples using lambda calculus syntax along with translations to Elixir, Haskell, and Python. This in the hope that seeing the ideas in a few familiar languages should help make them easier to follow and understand.

Note: the contents of the post are fairly terse and example driven. For more detailed information and background, there are a lot of great references including Michaelson, The Haskell Book2, and Wikipedia3

Introduction to λ Calculus

Lambda (λ) calculus was discovered by Alonzo Church in 1936. It is a universal model of computation that is equivalent to the Turing machine and Gödel’s general recursive functions (the Church-Turing Thesis).

λ Expressions

The λ calculus is a system for manipulating λ expressions. – Michaelson 2011, p. 21

A λ expression can be either a name, function, or function application.

Names

A name is used to refer to a λ expression.

Functions

A function is an abstraction over a λ expression that takes the form:

fn := λ<name>.<body>

Function application

Function application is the application of one lambda expression, fn, on a second, arg.

application := (fn arg)

First Example Expressions

For each example, I’ll give the λ expression along with examples in Elixir, Haskell, and Python to help explain/build an intuition for what is happening and explore how various programming languages handle anonymous functions.

Identity

The simplest function we can look at is the identity function:

λx.x
fn x -> x end         #  Elixir
\x -> x              -- Haskell
lambda x: x           #  Python

Applying the function to an argument returns the argument:

(λx.x 5)
5
(fn x -> x end).(5)   #  Elixir
5
(\x -> x) 5           -- Haskell
5
(lambda x: x)(5)      #  Python
5

Aside - Naming expressions

We can name expressions to make it easier to refer to them in other expressions. I’ll use <name> := <expression> to name expressions in λ calculus. For Elixir, Haskell, and Python, I’ll use language appropriate assignment.

We can name identity as follows:

identity := λx.x
identity = fn x -> x end
let identity = \x -> x
identity = lambda x: x

I’ll name expressions the first time they appear in the following examples to make it easier to reuse them in the future

Self-application

The self-application function is a function that calls itself with itself as the argument:

self_apply := λs.(s s)
self_apply = fn s -> s.(s) end      #  Elixir
let self_apply = \s -> (s s)        -- Haskell
self_apply = lambda s: s(s)         #  Python

Applying the self-application function to the identity function results in the identity function:

(λs.(s s) λx.x)
(λx.x λx.x)
λx.x
#  Elixir
(fn s -> s.(s) end).(fn x -> x end)
(fn x -> x end).(fn x -> x end)
fn x -> x end
-- Haskell
(\s -> (s s)) (\x -> x)
(\x -> x) (\x -> x)
\x -> x
#  Python
(lambda s: s(s))(lambda x: x)
(lambda x: x)(lambda x: x)
lambda x: x

Applying the self-application function to itself causes an infinite loop of self-application – the first step towards building recursive functions:

(λs.(s s) λs.(s s))
(λs.(s s) λs.(s s))
.
.
.

The argument, λs.(s s) is bound in the function λs.(s s), where it replaces the bound variable, s, in the function application (s s).

Apply

Apply binds a function, f, to an expression that binds an argument, arg, in an application of f to arg.

apply := λf.λarg.(f arg)
apply = fn f -> fn arg -> f.(arg) end end
let apply = \f -> \arg -> f arg
apply = lambda f: lambda arg: f(arg)

Applying identity to identity results in the identity function:

(apply identity identity) =>
((λf.λarg.(f arg) λx.x) λx.x) =>
(λarg.(λx.x arg) λx.x) =>
(λx.x λx.x) =>
λx.x

First and Second

We can construct expressions that take two arguments and return either the first or second:

first  := λfirst.λsecond.first       # First
second := λfirst.λsecond.second      # Second
# Elixir
first  = fn first -> fn second -> first end end
second = fn first -> fn second -> second end end
-- Haskell
let first  = \first -> \second -> first
let second = \first -> \second -> second
#  Python
first  = lambda first: lambda second: first
second = lambda first: lambda second: second

Make Pair

We can construct functions that take multiple arguments (n) by first building expressions that have n + 1 arguments:

  1. A function f takes an argument x and binds x in another function, g
  2. g takes an argument y and binds y in a function h that takes a function as an argument, z
  3. z is applied to x and the result of (z x) is applied to y
  4. This effectively results in z(x, y)
make_pair := λx.λy.λz.((z x) y)
# Elixir
make_pair = fn x -> fn y -> fn z -> z.(x).(y) end end end
-- Haskell
let make_pair = \x -> \y -> \z -> z x y
-- ap (1) (2) (\x y -> x > y)
#  Python
make_pair = lambda x: lambda y: lambda z: z(x)(y)

What’s next?

This post introduced the some basics of lambda calculus by example. We looked at the three types of lambda expressions: names, functions, and function application. We also started building and evaluating lambda expressions with additional examples using Elixir, Haskell, and Python.

The next post will cover free and bound variables, formal rules behind evaluating lambda expressions, and conditional logic in lambda calculus.

Footnotes


  1. Michaelson, Greg. An Introduction to Functional Programming Through Lambda Calculus. Dover, 2011.

  2. Allen and Moronuki, Haskell Programming from first principles

  3. Lambda calculus - https://en.wikipedia.org/wiki/Lambda_calculus