Lambda Calculus#
Lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics
Lambda calculus is a formal language
The expressions of the language are called lambda terms
Everything is a function, there are no literals
In lambda calculus, we write (f x)
instead of the more traditional f(x)
.
Many real-world programming languages can be regarded as extensions of the lambda calculus. This is true for all functional programming languages, a class that includes Lisp, Scheme, Haskell, and ML (OCaml, F#).
Lambda calculus in Python#
identity = lambda x: x
zero = lambda f: identity
one = lambda f: lambda x: f(x)
two = lambda f: lambda x: f(f(x))
three = lambda f: lambda x: f(f(f(x)))
# Don't repeat yourself (DRY)
succ = lambda numeral: lambda f: lambda x: f(numeral(f)(x))
two = succ(one)
three = succ(two)
three(lambda x: x+1)(0)
Tools of lambda calculus#
Substitution rules of programming
α-conversion: changing bound variables (alpha);
β-reduction: applying functions to their arguments (beta);
η-conversion: which captures a notion of extensionality (eta).
Alpha Conversion#
Alpha-conversion is about renaming of bound variables
(lambda x: x)(42) == (lambda y: y)(42) # Renaming
Beta Reduction#
A beta reduction (also written β reduction) is the process of calculating a result from the application of a function to an expression.
((λn.n×2) 7) → 7×2.
(lambda n: n*2)(7) == 7*2
Eta-conversion#
An eta conversion (also written η-conversion) is adding, or dropping an abstraction over a function.
# Eta-conversion
# λx.(f x) and f
f = lambda x: x
(lambda x: f(x)) == f
Extensive use of η-reduction can lead to what’s called point-free programming.
Extensive use of point-free programming can lead to point-less programming.
from functools import reduce
xs = reduce(lambda acc, x: max(acc, x), range(10))
print(xs)
xs = reduce(max, range(10))
print(xs)
Do we need to know about lambda calculus?#
You usually do not need to know about lambda calculus. But look out for point-free programming which may both simplify or over complicate your code. Lambda calculus is a must-have knowledge when dealing with compilers and expression trees (ASTs).