---
title: 'Introducing Lambda Calculus: Spilling the HoTT'
source: 'https://youtube.com/watch?v=wZp0sB1rBE4'
video_id: 'wZp0sB1rBE4'
date: 2026-07-31
duration_sec: 1729
---

# Introducing Lambda Calculus: Spilling the HoTT

> Source: [Introducing Lambda Calculus: Spilling the HoTT](https://youtube.com/watch?v=wZp0sB1rBE4)

## Summary

This video introduces lambda calculus as the central model of computation behind ideas like Lawvere's fixed point theorem, homotopy type theory, and computable reals. It walks through the notation, beta reduction, alpha conversion, currying, Church encodings of numbers and booleans, recursion with the Y combinator, and the limitations of the untyped lambda calculus.

### Key Points

- **Lawvere's fixed point theorem** [00:14] — A single theorem that unifies Cantor's theorem, Gödel's incompleteness theorem, the undecidability of the halting problem, Kleene's recursion theorem, Roger's fixed point theorem, and Curry's paradox.
- **HoTT and type theory as foundations** [01:14] — Homotopy type theory is a new field proposing type theory as an alternative foundation to ZFC set theory, with strong connections to computer-based theorem provers and compiler engineering. It depends on lambda calculus.
- **Lambda calculus as the root** [03:40] — Since lambda calculus underlies all these ideas, this video will be the root of a tree of future videos exploring each application.
- **Why CS needs a simplified model** [04:06] — Science uses simplified models (frictionless balls, ball-and-stick molecules, spherical Earth). Computer science needs a universal mathematical model of computation that works regardless of hardware.
- **Two models: Turing machines vs lambda calculus** [05:52] — Turing machines are a bottom-up, hardware-oriented model using a finite-state automaton with an infinite tape. Lambda calculus is a top-down, abstract model where computation is text substitution.
- **Lambda notation and anonymous functions** [08:07] — A lambda expression uses the λ symbol, a variable name, a dot, and the body template. This acts like an unnamed function declaration, which is why such functions are called anonymous functions.
- **Beta reduction and canonical form** [09:22] — Applying a function to a value by substitution is beta reduction. Repeatedly reducing until no more reductions are possible yields the canonical form — and this process is computation.
- **Alpha conversion and lexical scope** [10:05] — Alpha conversion renames bound variables consistently to avoid name collisions. Variables have lexical scope, bind to the closest declaration in the parse tree, and new declarations shadow outer ones.
- **Currying for multiple arguments** [11:02] — Nested lambda expressions allow functions with multiple arguments. This technique is currying, and expressions are left-associative unless bracketed.
- **Church numerals** [12:42] — A number n is encoded as a function that takes a function f and an argument x, then applies f to x exactly n times. Zero returns x unchanged.
- **Church booleans and logic** [16:58] — True is a function of two arguments that returns the first; False returns the second. These can implement NOT, AND, and predicates like is_zero.
- **The Y combinator enables recursion** [20:37] — The fixed-point combinator Y transforms a function into a self-referential loop, enabling general recursion. This is demonstrated by implementing factorial with a base case and a recursive step.
- **Building data structures and universality** [25:20] — Pairs, whole numbers, rationals, and lists can be built from nested pairs and Church numerals; strings via Unicode. Lambda calculus can emulate Turing machines and perform any algorithm.
- **Untyped lambda calculus limits** [28:02] — Untyped lambda calculus has no type safety — you can pass a number to a boolean function — and non-terminating expressions make it unsuitable as a foundation for mathematics. Typed lambda calculus is next.

### Conclusion

Lambda calculus is a deceptively simple system of substitution rules that can encode numbers, logic, data structures, and all of computation. Its exact expressive power is also what makes it unsuitable as a mathematical foundation, motivating the shift to typed lambda calculus in the next video.

## Transcript

you've just watched an awesome scene from an anime read a great passage from from an anime read a great passage from a book or enjoyed a particular Meme and then when you go to talk about it with your friends you realize that without
all the context that moment just won't land then you have to explain the entire backstory for it to make sense for me that's a laville fixed Point theorem an awesome mathematical concept that unifies Cano's theorem go Bell's
incompleteness theorem and the undecidability of the halting problem that's right you get three I say three of the most important results in mathematics all for the price of one but what's more if you order now you also
get keen's recursion theorem Roger fixo theorem and Curry's Paradox absolutely theorem and Curry's Paradox absolutely free I'm sorry something just overcame me however to do lille's fix Point theorem Justice I would need a model of
computing most likely Lambda calculus because I'm a functional programming hipster type I guess I'll have to do hipster type I guess I'll have to do explaining L Val's fix Point theorem
sometime later I know that there's a new field of mathematics right on The field of mathematics right on The Cutting Edge called homotopy type Theory a part of mathematics where new discoveries and theorems are being made
homotopy type Theory it's a real mouthful to say so let's contract that mouthful to say so let's contract that to hot tea which isn't such a mouthful since you tend to sip it most of current mathematics sits a top a foundation
mathematics sits a top a foundation based on zfc set theory or at least it based on zfc set theory or at least it pretends to type theory is an alternative foundation for mathematics it has the advantage that computer-based
it has the advantage that computer-based theorem provs are very well suited for type based systems and Mathematics can leverage all the great work that computer scientists and compiler Engineers have done as well the
mathematicians can contribute their own expertise to the field of computer science and compiler engineering it's so new and shiny that we don't even know if
hot tea will be the type theory that becomes the foremost type Theory type becomes the foremost type Theory type Theory and hot tea also depend on Lambda calculus while we are discussing using computers and Mathematics there is also
the computable reals a way to have most of the useful properties of the of the useful properties of the so-called real numbers but without the numbers having an infinite information density and ex and imploding your brain
into a black hole what your brain hasn't been imploded into a black hole perhaps that was because you actually using computable reels and just pretending that they were the complete ordered field computable reels are a useful
field computable reels are a useful subset of the reels that avoids most of the weird paradoxes you get with them by replacing them with a whole lot of other weird properties to do computable reels Justice again I'm going to need a model
of computing so Lambda calculus or something equivalent yeah I think I'm going to have to do Lambda calculus Lambda calculus isn't a boring meal that you have to eat in order to get dessert It's a Wonderful enlightening subject
all to itself so here is what I'm going to do since Lambda calculus is the root of all of these ideas this video will be the root of a tree of videos each
exploring an application of Lambda calculus
oversimplified mathematical models of reality and honestly is it even a real science if you don't have a mathematical model yes of course it is but having a chauvinistic disdain towards less mathematical stem subjects is both
mathematical stem subjects is both slightly humorous and also perpetuates a slightly humorous and also perpetuates a deeply toxic interdistance ten rivalry to the overall detriment of society in Newtonian physics you have
frictionless balls engaging in elastic collisions in a vacuum in chemistry you have the ball and stick models of molecules and in geoscience the earth is
often simplified into a sphere rather than the oblake spheroid that it really is have you ever noticed that science seems overly obsessed with ball in computer science we want to be able
in computer science we want to be able to reason about computers comp size to reason about computers comp size needs a simple mathematical model that allows us to work with computer science that can apply to all computers
regardless of Hardware it would be kind of a hassle if we had to reinvent all of computer science every time somebody invented a new bit of Hardware it should
be Universal the only time computer scientists go into Hardware based details as if it would result in a great idea for a paper or a conference talk or
idea for a paper or a conference talk or if they're really lucky a startup in mature Fields the mathematical models you use are pretty settled however you use are pretty settled however compai is a very young field so there
are many competing models you have probably heard of touring machines conceived by the great Alan touring in order to solve the halting problem that I casually mentioned before a touring machine is basically a finite State
automata strapped to a real tooreal tape machine if you want to learn more about finite State automata I've got a great video for that this way of modeling Computing is a very bottom up Hardware oriented model of computing you can
build physical models of touring machines well at least in theory the mathematically ideal touring machine has an infinite long tape which is kind of
an infinite long tape which is kind of Impractical however there is also a topdown model of computing for those who are really into abstraction in Lambda are really into abstraction in Lambda calculus all Computing is simulated as a
calculus all Computing is simulated as a system of text substitution rules now I am sure you have received a document like this dear title first name last name you have not paid your bill of amount to not a scam Incorporated please
send payment before we start legal actions yours not a scam Incorporated actions yours not a scam Incorporated where the title first name Etc have been replaced with scraped copies of something resembling your personal D
details times you can even get letters like this from legitimate business like this from legitimate business even if you have been fortunate never to receive a bill in your life you are watching this on YouTube Modern websites
like YouTube basically work on this principle of substitution as well you have a basic template of what the web page looks like and then the details for page looks like and then the details for each page are substituted based on
entries in a database there are two Styles these templates can be rep Styles these templates can be rep presented in Lambda calculus Lambda name presented in Lambda calculus Lambda name the Lambda symbol made famous by
halflife 2 followed by the name of the variable that will be substituted a period as a separator and then the string the text will be copied into there is an alternative more compact way
of writing this where you have the variable name introduced the barred Arrow to indicate map to and what follows is the template to substitute into now if you have done some programming you might recognize this as
being a little bit like a function declaration although it doesn't give the function a name that's why in some places these Lambda expressions are also
called Anonymous functions an anonymous function of course is just a fancy name for a masquerade ball but e even more technically Lambda expressions are not always really functions but they act a lot like functions and I just call them
functions anyway the reason why they are not functions is a bit of a spoiler for later in the video in this system you can apply this function by
concatenating a value after it the brackets are there to remove any ambiguity from where the body of the function ends and the value I will be substituting in starts this type of substitution is
starts this type of substitution is called beta reduction if we apply beta reduction until we can reduce no more then we get what is called the canonical then we get what is called the canonical form it might sound strange but this
repeated beta reduction is all you need to do computation there's also Al a process called Alpha conversion that we can change the name of a variable to
another name as long as we change all of the variables that are bound together the variables that are bound together Alpha conversion is done to ensure that variables that coincidentally have the same name won't Collide this is to
ensure that the variable has a thing called lexical scope if you want to PA the Lambda expressioned into its grammatical components it will create a
PA tree and the variables will be bound to the Declaration that it is directly under in the pass tree a new variable being introduced with the same name Will
being introduced with the same name Will Shadow or mask the variables above it in the tree don't worry we're going to do some examples and that should help we can Nest the Lambda expression to create create a function that has multiple
create a function that has multiple arguments the arrows and the shading should show you how the variable Mark the variables abound and the scope of each variable again if we pause this into a tree you can see how the scoping
of the variable and the PA tree lines up a new variable name is introduced in the abstraction node and has scope to everything below it application node
noes are where the functions are called and variable nodes are places where on application the input parameters will be replaced this style of tree is called an
replaced this style of tree is called an abstract syntax tree this trick of using abstract syntax tree this trick of using nested Expressions to have multiple arguments is called currying and is one of the most spicy aspects of Lambda
of the most spicy aspects of Lambda calculus to make this trick work cleanly it's also handy to have Lambda Expressions work as being left Expressions work as being left associative that is the leftmost pairs
are evaluated first so if we have an expression like this the pair of on the expression like this the pair of on the left will be evaluated first then the next one across and then the final one you can force a different order by
making use of bracketing but I said these Expressions could be used for these Expressions could be used for computing so how is that
video then you might already have heard about church encoding in passing so how do we represent numbers as functions you use a number function that applies
use a number function that applies another that applies another function another that applies another function some number of times oh that colon three line thing is defined as in this version of Lambda calculus it's just an easy
of Lambda calculus it's just an easy nickname to simplify complex formation also to keep them separated from also to keep them separated from variable names these aliases will start
variable names these aliases will start with a capital letter we can read this as one takes the function f and an argument for that function X then applies that function to the argument once we are just getting
started so let's do two to get the hang of it two takes a function f and an argument for that function X applies that function f to the argument F then
applies the function again to what was just returned in other words it applies the same function twice and what is a number system without a zero something
number system without a zero something positively medy eval zero just Returns positively medy eval zero just Returns the argument without applying the function so zero takes the function and does nothing with it returning the
original argument unchanged of course having numbers isn't very useful unless we can do something with those numbers let's start with addition for addition we going are going to need a function that takes two addin
to need a function that takes two addin we also know that returns a number which we also know that returns a number which takes two arguments then we can apply takes two arguments then we can apply the function f m times and then take the
the function f m times and then take the return value of that and apply it n return value of that and apply it n times let's try that out right
and we have successfully shown that 1 + 1 equal 2 in much less than 360 Pages now that might have been a little difficult to follow so let's do it again difficult to follow so let's do it again this time using an abstract syntax tree
obvious whenever we have an application node whose left child is an abstraction we replace every instance of that variable it's also Poss possible to
variable it's also Poss possible to Define expressions for successor multiplication and the predecessor function I'm not going to go over all of those in detail because this is meant to be an introduction to Lambda calculus I
suggest you look up church encodings for them on a resource like Wikipedia them on a resource like Wikipedia numbers and basic operations on numbers aren't really enough to do Computing we also need logic and that's what we have
also need logic and that's what we have have the church booleans for named for have the church booleans for named for George Bull and his wife and editor Mary Everest bull here are the functions that act as bullin true takes two functions
and Returns the first argument and false takes two functions and Returns the second these basically act a little bit like an if then statement with the true
Bing returning the then part and the false Bing returning the else part for false Bing returning the else part for example you could Implement not as this
you can see if we call this with the true argument it will return false and if pass a false argument it will return true also you might have noticed that
true also you might have noticed that false looks exactly like zero this sort of coincidence might end up being a symptom of a problem that comes up later on these are fun so far let's Implement logical and the operator that is true if
logical and the operator that is true if both inputs are true and false in all both inputs are true and false in all other situations we can simply translate that truth table into a Lambda expression there are a few easy ways to
expression there are a few easy ways to simplify this further with and and not you can implement every other logical operation for logic to be useful though
we need a way to probe the rest of the universe and bring data Into The Logical universe and bring data Into The Logical realm we need predicates is zero is one realm we need predicates is zero is one of the easiest predicates to do in
Lambda calculus this takes a number and returns true if the number is zero and returns true if the number is zero and false otherwise we basically use the property of zero it always returns the second argument unchanged so for zero
true will be returned and when we use any other value false will be returned any other value false will be returned we have almost everything we need to do Computing we have logic we have numbers we have operations on numbers we even
we have operations on numbers we even have a way to do Loop operations a set number of times we just use the number as it as a function what we don't have as it as a function what we don't have is a way of doing a loop until some
condition is satisfied in order to do that we have to make use of one of the that we have to make use of one of the most powerful tools mathematics has recursion the ability of a function to call itself General recursion is a
prerequisite for computing the power of General recursion unfortunately makes General recursion unfortunately makes this Lambda calculus unsuitable to act as a foundation for mathematics this isn't an this is not an accident or
coincidence there exists thresholds of expressive power which when crossed become incomplete in predict unpredictable and even un sound however
that is a topic of a future video as I'll be saying it quite a few times at this point all I have is explain how you can turn Lambda inside out with Y the
can turn Lambda inside out with Y the fixed point combinator if we feed the Y combinator uh dummy function first we expand out Y into its canonical form then we apply beta reduction replacing all the fs with G's we then apply beta
reduction again this time replacing all all the x's in the first Clause with the all the x's in the first Clause with the second Clause now if you look at the argument to G here you will notice that it looks exactly like the second line
which we have already shown is equal to YG so we can replace that with YG and we have ourself a selfing fixed point and a restaurant for
selfing fixed point and a restaurant for your Mexican style food your Mexican style food you can see how it ends up with G being you can see how it ends up with G being passed into G this is a type of fixed
point where the function going in is the same as the function going out I always same as the function going out I always find examples to be helpful so let's try find examples to be helpful so let's try and implement the factorial so how would
you implement this the easiest way is to make use of what I call the recursive algorithm algorithm this method allows you to work out how to create a recursive algorithm for even the most complex of tasks in this method first
you try to solve the simplest case this is your base case then you work out a way to take a step towards your base case this is your recursive or inductive
step so for factorial we will need to start with some basic boiler plate since it's recursive we know it's going to use the Y combinator and the function we
will that we will pass into the Y combinator is going to receive itself as the first argument with factorial we know the next argument will be the number we will be factorial liing now the base case of factorial is
zero which is one since we have the zero predicate it's quite easy to do this for the true branch of the Boolean we return one for
the recursive step we have to start with the N value and then we reduce it down the N value and then we reduce it down to the n n - one case for factorial this
to the n n - one case for factorial this is the n * nus factorial in our Lambda is the n * nus factorial in our Lambda calculus implementation we multiply M with the results of our recursive step so let's try this with three
[Applause] [Music]
we can Define pairs once we have pairs of values we can Define whole numbers as pairs of the counting numbers that we've constructed using Church numerals then constructed using Church numerals then we can have rational numbers as pairs of
whole numbers the numerator and the denominator we can also Define lists as denominator we can also Define lists as nested pairs defining real numbers is a little bit more complicated and will be the topic of its own video we can also
the topic of its own video we can also treat numbers as characters using treat numbers as characters using Unicode and if we have a list of characters that allows us to make strings it's even possible for these
strings to be the string repres representation of Lambda Expressions we could even go super meta we can write a Lambda expression that will take a string pause it evaluate the lamb
string pause it evaluate the lamb expression and return that expression's expression and return that expression's canonical form we you could even write a Lambda expression that when reduced will totally emulate a touring machine
basically Lambda Expressions can perform any algorithm that a computer can perform and any computer given sufficient time and memory can emulate
sufficient time and memory can emulate any Lambda Lambda expressions are not really functions well functions are supposed to
be total this means for every input there is a corresponding output however you can make a Lambda expression like this one which will run forever and this one which will run forever and never ever settle down to a real value
never ever settle down to a real value this is unfortunately true for every this is unfortunately true for every model of computing you can't build an uncrashable computer being a able to crash is simply an inherent part of
being a computer this is something that unfortunately makes Lambda calculus inappropriate as a foundation for mathematics as any architect will tell
you a collapsable Foundation is bad for building there is another problem that building there is another problem that makes this style of Lambda calculus mathematical perspect perspective and as a computer language I
talked about functions taking numbers as inputs or booing or even strings however this is just enforced by convention there is nothing to stop us passing a
number into a function meant for a bulling or for us to try and add two bulling or for us to try and add two bulling together it is trivially easy to bulling together it is trivially easy to write programs that are total nonsense
this is the limitation of of this style of Lambda calculus called the untyped Lambda calculus untyped should not be confused with fake type which is a Japanese electro swing band but if this is untyped Lambda calculus can we have a
is untyped Lambda calculus can we have a typed Lambda calculus yes and that will typed Lambda calculus yes and that will be our next video