For anyone coming from a background of working with imperative programming languages, the experience of programming using a functional programming language can feel surreal. With no recourse to familiar looping constructs like for and while loops, with the glaring absence of assignment statements and familiar data structures, the learning curve consists of not just learning new syntax but also learning a new way of thinking. While the precise syntax and the details depend on the particular functional language being learned, the crucial underlying way of thinking is common across the board for all functional languages. This way of thinking is essentially the lambda calculus.

Lambda calculus was invented by Alonzo Church in the 1930s, who, as part of his inquiry into the foundational questions in mathematics, explored the idea of representing computation using functions. In fact, lambda calculus is equivalent to Turing machinesAn abstract model of computation invented by Alan Turing, who later went on to become Church’s PhD student. in the sense that everything that can be computed can also be expressed through lambda calculus, and everything that can be expressed through lambda calculus can be computed.

This blog discusses some of the essential elements in lambda calculus, and highlights how the symbolic expressions in lambda calculus can be used for computing. In particular, we show how such expressions can be used for implementing data types, as well as for representing arithmetic, logical, and relational operators.

If you’d like to learn more about functional programming, this course is a really good starting point.

Lambda expressions#

The fundamental building blocks of lambda calculus are known as lambda expressions. A lambda expression can be one of the following three things:

1. A variable: A variable is just a name. For example, $x$, $y$, and $z$ can serve as variables.

2. A function abstraction: A function abstraction is a function that has no name and takes in a single parameter. The general form of a function abstraction is

   $$\lambda x. B$$

   Here, the symbol $\lambda$ means the start of an anonymous function. The name that follows $\lambda$ is the parameter. The dot symbol $( . )$ indicates that the function body is about to begin. The function body $B$ consists of a lambda expression.

   For convenience, we occasionally use the term lambda function to mean a function abstraction.

3. A function application: A function application consists of any two lambda expressions, $E_1$ and $E_2$, placed side by side. In a function application such as

   $$(E_1E_2)$$

   , the expression $E_2$ can be thought of as an argument passed to $E_1$.

Examples: Function abstraction#

• $\lambda x.\ x$ is the identity function. It returns whatever it receives.

• $\lambda x.\ y$ is an abstraction that takes a lambda expression $x$, ignores it completely, and returns some other lambda expression $y$. For this reason, it can be thought of as the constant function.

• $\lambda y.\ y y$ is an abstraction that takes a lambda expression and applies it to itself.

Convention on spaces: When variable names consist of a single letter, as in the context of this blog, they need not be separated by spaces.

Binding#

• The variable that appears right after a $\lambda$ is said to be bound in the body of that abstraction. All other variables are said to be free.

  • In $\lambda x.\ x$, the variable $x$ is bound.
  • In $\lambda x.\ y$, the variable $x$ is bound but the variable $y$ is free.
  • In $\lambda y.\ zy$, the variable $y$ is bound, but the variable $z$ is free.

Associativity#

• Function application is left-associative. If there are three expressions listed as $E_1E_2E_3$, then

$$E_1E_2E_3 \quad \text{ means } \quad(E_1E_2)E_3$$

Scope#

• The body or the scope of a lambda function goes as far to the right as possible. For example, the underbraces show the scope of $\lambda y$ and $\lambda x$ in the following lambda expression:

$$(\lambda y.\ \underbrace{y (yy )}) (\lambda x. \underbrace{xz})$$

Convention on parenthesization: Do note that the parentheses are part of the syntax to help with the grouping of the function applications. They can’t always be omitted without loss of meaning, but we do make some exceptions to avoid clutter:

• We omit the outermost parentheses around a standalone lambda expression.
• We omit the parenthesis surrounding two variables.
• We omit parentheses that enforce associativity.

Functions on more variables#

Unlike mathematical functions, each lambda function has only one associated variable bound to its scope. To express the idea of a function on more than one variable, the lambda functions can be nested. For example, the function $\lambda x.\ \lambda y.\ xy$ can be seen as a function that takes a parameter $x$ and returns a function of $y$ that applies $x$ to $y$. This is easier to see with parentheses in place:

$$(\lambda x.\ (\lambda y.\ xy))$$

The following visualization of a lambda expression may help internalize this idea:

Often, a lambda expression such as $\lambda x.\ \lambda y.\ \lambda z.\ E$ is written in shorthand by gathering all variables against a single $\lambda$ as shown:

$$\lambda xyz.\ E$$

How to do computations using lambda expressions#

To do computations with lambda expressions we need to be able to evaluate them, or reduce them to simpler forms. The primary way to express the evaluation of a function is through a rule called $\beta$-reduction.

This represents the idea of passing $E_2$ as an argument to an actual function call and returning the result.

Let’s look at some examples of function applications that are beta reducible:

• Example 1: The identity function applied to a free variable reduces to that free variable (since the identity function returns its argument.)

$$\begin{align*} &(\lambda x. x)y \\ \stackrel{\beta}{\implies} & y \end{align*}$$

• Example 2: The identity function applied to itself reduces to the identity function.

  $$\begin{align*} &(\lambda x. x)(\lambda x. x) \\ \stackrel{\beta}{\implies} & \lambda x. x \end{align*}$$

• Example 3: A function that applies its argument to itself, when applied to the identity function $\beta$-reduces to the identity function.

  $$\begin{align*} & \qquad (\lambda y.\ y y)(\lambda x.\ x)\\ \stackrel{\beta}{\implies} &\qquad (\lambda x.\ x)(\lambda x.\ x) \qquad \lambda y\text{ is removed and }y\text{ is substituted by }\lambda x. x \\ \stackrel{\beta}{\implies} & \qquad \lambda x.\ x \qquad \qquad \ \ \ \quad \text{ by Example 1} \end{align*}$$

• Example 4: We can keep applying $\beta$-reductions to the following expression, but the computation does not terminate.

$$\begin{align*} & \qquad (\lambda y.\ yy) (\lambda y.\ yy)\\ \stackrel{\beta}{\implies} &\qquad (\lambda y.\ yy) (\lambda y.\ yy)\\ \stackrel{\beta}{\implies} &\qquad (\lambda y.\ yy) (\lambda y.\ yy)\\ & \qquad \qquad \qquad \vdots \\ \end{align*}$$

• Example 5: We illustrate the application of a nested function abstraction through the following set of slides.

Notation: We use the notation $\stackrel{\beta^*}{\implies}$ to express zero or more beta reductions.

For example,

$$((\lambda x.\ x) (\lambda y.\ yy))(\lambda w.\ w) \stackrel{\beta^*}{\implies} \lambda w.\ w$$

Note that when a lambda expression can’t be $\beta$-reduced any further, it’s said to be in normal form. A non-terminating function application that keeps reducing to itself has no normal form. If the normal form of a lambda expression exists, then reducing the leftmost, outermost lambda application is guaranteed to lead to a unique normal form. This reduction strategy is called a normal order reduction.

Alpha conversion#

It doesn’t matter what name we give to a bound variable in a function as long as we do so consistently for all occurrences of the variable in the scope of that abstraction. So $\lambda x.\ x$ is the same abstraction as $\lambda y.\ y$.

Now, consider the following expression. The variable $y$ within the lambda abstraction is a bound variable, but the variable $y$ to which the abstraction applies is a free variable. They’re not the same.

$$(\lambda xy.\ x y) y$$

After a $\beta$-reduction is attempted, the variable passed in as the argument becomes a bound variable.

$$\begin{align*} & (\lambda xy.\ x y) y \\ \stackrel{\stackrel{\text{attempted}}{\beta}}{\implies}& \lambda y.\ y y \end{align*}$$

This is called capturing a free variable. Notice how this capturing of $y$ inadvertently changed the meaning of the lambda expression to a self-application—which is other than what was intended.

For the lambda expression from above, if we rename the bound variable $y$ as $z$, we get:

$$\begin{align*} & (\lambda x\red{y}.\ x \red{y}) y \\ \stackrel{\alpha}{\implies}& (\lambda x\red{z}.\ x \red{z}) y \\ \stackrel{\beta}{\implies}& \lambda z.\ y z \end{align*}$$

This now says what was intended: Apply the free variable $y$ to the argument of the lambda function.

Note: We used $\stackrel{\alpha}{\implies}$ to explicitly indicate an alpha conversion, but these are usually done implicitly, as needed before applying $\beta$-reductions.

Before going into exactly what that means, we adopt a small notational convenience to keep ourselves from drowning in a frenzy of symbols:

Notation: We give a name to an abstraction. When naming an abstraction, we use the word define before the name given to it.

Let’s begin by defining two boolean values

Representing boolean values#

We name the following two function abstractions as $\text{True}$ and $\text{False}$.

If we look at the semantics of these abstractions, $\text{True}$ takes two parameters and returns the first. Whereas $\text{False}$ takes two parameters and returns the second.

Note: We could have defined these differently, but it’s easier to go with how it’s typically done.

• Now, let’s think about how to represent an and operator.

  $$\begin{align*} \textbf{define}\quad \text{And} &= \lambda a b.\ a\ b \ \text{False}\\ &= \lambda a b.\ a\ b \ (\lambda xy.y)\\ \end{align*}$$

  If $\text{And}$ is applied to $\text{True} \ \text{False}$, the expression reduces to $\text{False}$ as expected:

  $$\begin{align*} &\text{And}\ \text{True}\ \text{False}\\ \equiv \ \ \ \ &(\lambda ab.\ a\ b\ (\lambda xy.\ y))\ (\lambda rs.\ r)\ (\lambda tu.\ u)\\ \stackrel{\beta^*}{\implies} \ & (\lambda rs.\ r)\ (\lambda tu.\ u)\ (\lambda xy.\ y) \\ \stackrel{\beta^*}{\implies} \ & \lambda tu.\ u\\ \equiv \ \ \ & \text{False} \end{align*}$$

  Similarly, when applied to any other combination of $\text{True}$ and $\text{False}$, the outcome would be as expected:

  $$\begin{align*} &\text{And}\ \text{True}\ \text{True} \stackrel{\beta^*}{\implies} \text{True} \\ &\text{And}\ \text{False}\ \text{True} \stackrel{\beta^*}{\implies} \text{False}\\ &\text{And}\ \text{True}\ \text{False} \stackrel{\beta^*}{\implies} \text{False} \end{align*}$$

• We can define $\text{Or}$ using a similar idea:

  $$\begin{align*} \textbf{define}\quad \text{Or} &= \lambda a b.\ a\ \text{True}\ b \\ &= \lambda a b.\ a\ (\lambda xy.\ x)\ b\\ \end{align*}$$

  Just as before, the outcome of applying the $\text{Or}$ operator can be verified to behave as expected:

  $$\begin{align*} &\text{Or}\ \text{True}\ \text{True} \stackrel{\beta^*}{\implies} \text{True}\\ &\text{Or}\ \text{True}\ \text{False} \stackrel{\beta^*}{\implies} \text{True}\\ &\text{Or}\ \text{False}\ \text{True} \stackrel{\beta^*}{\implies} \text{True}\\ &\text{Or}\ \text{False}\ \text{False}\stackrel{\beta^*}{\implies} \text{False} \end{align*}$$

A conditional statement#

The following expression is intended to serve as an if-else expression, where the branching depends on a condition $c$:

define $\text{IfElse} = \lambda cxy.\ cxy$

Church numerals#

We saw above how boolean values can be encoded as function abstractions. The set of non-negative integers can also be encoded similarly. First, a function is defined and is given the name $0$. A successor function applied to $0$ is called a $1$. The successor is applied to $1$ and is called a $2$, and so on.

• define $0 = \lambda sz.\ z$

  If $z$ is a variable representing zero and $s$ is a successor function, ignore $s$ and return $z$.

• define $1 = \lambda sz.\ sz$

  Apply the successor function $s$ on $z$.

• define $2 = \lambda sz.\ s(sz)$

  First, apply the successor function $s$ on $z$ to get $sz$, and then apply $s$ on $sz$ a second time.

• define $3 = \lambda sz.\ s(s(s z))$

• define $n = \lambda sz.\ \underbrace{s\ (\ldots(s ( s }_{n\ \text{times}}z)))$

Encodings defined this way are called Church numerals.

Terminology note: When referring to a lambda expression representation of a number $n$ as a Church numeral, we call it the numeral $n$.

Repetition#

Suppose we want to apply a lambda abstraction $f$ repeatedly to another function $g$ a total of $n$ times, where $n$ is known in advance. How would we do this? Repetitions of this kind can be achieved through the application of the following abstraction:

define $\text{Repeat} = \lambda nxy.\ nxy$

We use the variable name $n$ to help remember that the function expects the Church numeral $n$.

If $\text{Repeat}$ is applied to a Church numeral $n$ and the expressions $f$ and $g$, we see that $f$ is applied to $g$ repeatedly:

$$\begin{align*} &\text{Repeat} \ (\lambda sz.\ \underbrace{s(\ldots s(s}_{n\ \text{times}}z)))\ f\ g\\ \equiv \ \ \ &(\lambda nxy.\ nxy) \ (\lambda sz.\ \underbrace{s(\ldots s(s}_{n\ \text{times}}z)))\ f\ g\\ \stackrel{\beta}{\implies} &(\lambda xy.\ (\lambda sz.\ \underbrace{s(\ldots s(s}_{n\ \text{times}}z)))\ x\ y)\ f\ g \\ \stackrel{\beta}{\implies} &(\lambda y.\ (\lambda sz.\ \underbrace{s (\ldots s(s}_{n\ \text{times}}z)))\ f\ y)\ g \\ \stackrel{\beta}{\implies} &(\lambda sz.\ \underbrace{s(\ldots s(s}_{n\ \text{times}}z)))\ f\ g\\ \stackrel{\beta}{\implies} &(\lambda z.\ \underbrace{f(\ldots \ f(f}_{n\ \text{times}} z)))\ g\\ \stackrel{\beta}{\implies}& \underbrace{f(\ldots f ( f}_{n\ \text{times}} g) \end{align*}$$

Arithmetic#

How does one add two Church numerals? Let’s first encode something simpler: an increment of one.

• define $\text{Inc} = \lambda nsz.\ s(nsz)$

  The key idea is that the expression passed in $s$ is applied $n$ times to $z$ and then one more time again to get the Church numeral $n+1$.

  Let’s apply $\text{Inc}$ on $2$ to get $3$:

  $$\begin{align*} &\text{Inc}\ \red{2}\\ \equiv \ \ \ & (\lambda nsz.\ s(nsz)) \ \red{(\lambda tx.\ t(tx))}\\ \stackrel{\beta}{\implies}& (\lambda sz.\ s(\red{(\lambda tx.\ t(tx))}sz) \\ \stackrel{\beta}{\implies}& (\lambda sz.\ s( \red{(\lambda x.}\ s(s\red{x})\red{)}z) \qquad \text{$\lambda t$ is reduced next as it's the leftmost function application}\\ \stackrel{\beta}{\implies}& (\lambda sz.\ s( s(sz))) \qquad \text{$\lambda x$ is reduced next since it's the leftmost lambda application}\\ \equiv \ \ \ & 3 \end{align*}$$

• To represent adding two numbers $n$ and $m$, we apply $\text{Inc}$ on the Church numeral $m$ a total of $n$ times:

  define $\text{Add} = \lambda n m. n\ \text{Inc}\ m$

  When applied to a Church numeral $n$, the numeral takes $\text{Inc}$ as the successor function and $m$ as the expression on which $\text{Inc}$ is to be applied $n$ times. So in fact, such an application would reduce to the following:

  $$\lambda m.\ \underbrace{\text{Inc}\ ( \ldots \text{Inc}\ (\text{Inc}}_{n\ \text{times}}\ m))$$

  Let’s see this in action applied to $2$ and $2$:

$$\begin{align*} &\text{Add} \ 2\ 2\\ \equiv \ \ \ &(\lambda nm.\ n\ \text{Inc}\ m) \ 2\ 2\ \\ \stackrel{\beta^*}{\implies}&2\ \text{Inc}\ 2\ \\ \stackrel{\beta^*}{\implies}&\ \text{Inc}\ (\text{Inc}\ 2)\ \\ \stackrel{\beta^*}{\implies}&\ (\lambda abc.\ b(abc))\ \ (\text{Inc}\ 2)\ \\ \stackrel{\beta^*}{\implies}&\ \lambda bc.\ b((\text{Inc}\ 2)\ bc) \ \\ \stackrel{\beta^*}{\implies}&\ \lambda bc.\ b(3\ b\ c) \ \\ \stackrel{\beta^*}{\implies}&\ \lambda bc.\ b(b(b(bc)))\\ \equiv\ \ \ & 4 \ \\ \end{align*}$$

If you’d like to get practice verifying this in symbolic form by hand, we include the reductions here for assistance:

• To represent the multiplication of two numbers $n$ and $m$, we want to add $m$ a total number of $n$ times to $0$.

  define $\text{Mult} = \lambda n m.\ n\ (\text{Add}\ m)\ 0$

  Essentially, when applied to a Church numeral $n$, this is equivalent to:

  $$\lambda m.\ \underbrace{\gray{(}\text{Add}\ m\gray{)}(\ldots \gray{(}\text{Add}\ m\gray{)}\ (\gray{(}\text{Add}\ \ m\gray{)}}_{n\ \text{times}}\ 0))$$

  For example, when $\text{Mult}$ is applied to $3$ and $2$, it is equivalent to:

  $$\text{Mult}\ 3\ 2 \equiv \gray{(}\text{Add}\ 2\gray{)}\ (\gray{(}\underbrace{\text{Add}\ 2\gray{)}\ \underbrace{(\gray{(}\text{Add}\ 2\gray{)}\ 0)}})$$

Note: The names given to the abstraction must be replaced by the abstractions before applying beta reductions.

Predecessor#

Previously, we defined $\text{Inc}$ to get the successor of a numeral. It’s not so easy how we would get a predecessor of a numeral $n$. Consider a numeral such as

$$n = \lambda sz.\ \underbrace{s(\ldots s(s}_{n\ \text{times}}z))$$

How do we strip an $s$ to get the following?

$$n-1 = \lambda sz.\ \underbrace{s(\ldots s(s}_{n-1\ \text{times}}z))$$

Intuition: The way around this is to incrementally construct pairs of numbers $(k, k-1)$ where $k$ increases in steps of one, and then once we have the pair $(n, n-1)$, the second element of the pair is returned to get the predecessor of $n$.

define $\text{Pair} = \lambda xyb.\ bxy$

The role of the third variable $b$ envisioned here is to return one of the two elements in the $(x, y)$ pair. This can be seen by passing $\text{True}$ or $\text{False}$ as an argument to $b$:

• The expression ($\text{Pair}\ 1\ 0\ \text{True}$) returns $1$.
• The expression ($\text{Pair} \ 1\ 0\ \text{False}$) returns $0$.

Examples of encoded pairs#

Using the definition of $\text{Pair}$, we can encode pairs of consecutive integers.

• So for example, the $(0,0)$ pair is codified as the following expression:

  define $(0,0) = (\lambda xyb.\ bxy)\ 0\ 0$ $\stackrel{\beta}{\implies} \lambda b.\ b\ 0\ 0$

• Similarly, we can encode other pairs as lambda expressions:

  define $(1,0) = (\lambda xyb.\ bxy)\ 1\ 0$ $\stackrel{\beta}{\implies} \lambda b.\ b\ 1\ 0$

  define $(2,1) = (\lambda xyb.\ bxy)\ 2\ 1$ $\stackrel{\beta}{\implies} \lambda b.\ b\ 2\ 1$

Given a pair represented by $p$, we can get the successive pair by using the $\text{Inc}$ abstraction (defined earlier for incrementing):

define $\text{NextPair} = \lambda p.\ \text{Pair}\ \underbrace{(\text{Inc}\ (p\ \text{True}))}_{ 1^{st} \text{argument} } \ \underbrace{(p\ \text{True})}_{2^{nd} \text{argument}}$

Here, the pair $p$ applied to $\text{True}$ selects the first element in the pair $p$. This selected element is used twice in order to construct the next pair. For example, the abstraction $\text{NextPair}$ applied to $(0,0)$ gives us the encoding for $(1,0)$:

$$\begin{align*} &\text{NextPair}\ \underbrace{(\lambda b.\ b\ 0\ 0)}_{(0, 0)}\\ \stackrel{\beta^*}{\implies}& \lambda b.\ b\ 1\ 0 \end{align*}$$

We’d like to apply the NextPair abstraction $n$ times starting with the pair $(0,0)$.

Note: In starting with $(0, 0)$, we assume (for convenience) that the predecessor of $0$ is $0$.

We apply the abstraction $\text{NextPair}$ $n$ times as follows:

$$\begin{align*} &\lambda n.\ n\ \text{NextPair}\ (\lambda b.\ b\ 0\ 0)\\ \equiv \ &(n, n-1) \end{align*}$$

Finally, to select the second element in a pair, we apply that pair to $\text{False}$:

define $\text{Second} = \lambda p.\ p\ \text{False}$

For example, let’s apply $\text{Second}$ on $(2,1)$ to see how this works:

$$\begin{align*} &(\lambda p.\ p\ \text{False}) ((\lambda nmb.\ bnm) \ 2 \ 1)\\ \stackrel{\beta}{\implies}& (((\lambda nmb.\ bnm) \ 2 \ 1)\ \text{False})\\ \stackrel{\beta}{\implies}& (((\lambda mb.\ b\ 2\ m) \ 1)\ \text{False})\\ \stackrel{\beta}{\implies}& ((\lambda b.\ b\ 2\ 1)\ \text{False})\\ \stackrel{\beta}{\implies}& (\lambda xy.\ y)\ 2\ 1 \\ \stackrel{\beta}{\implies}& 1 \end{align*}$$

We can finally use $\text{Second}$ to return the predecessor of a numeral $n$ by selecting the second element of the pair $(n, n-1)$:

define $\text{Pred} = (\lambda n.\ \text{Second} \ n\ \text{NextPair}\ (\lambda b.\ b\ 0\ 0))$

Relational operators#

Finally, we look at how relational operators such as $=$, $\leq$, $\geq$, $<$, $>$ (for expressing equality and inequality) are expressed in lambda calculus.

For example, to check if $m \leq n$, we can perform the subtraction $m-n$ and see if the outcome is a $0$. Testing for $0$ suffices since we defined the predecessor of $0$ to be $0$.

We define the abstraction $\text{TestZero}$ as follows to check for equality of the input with $0$. Later, we’ll use this abstraction to define other operators.

define $\text{TestZero} = \lambda n.\ n\ (\lambda w.\ \text{False})\ \text{True}$

Recall that the numeral $0$ is defined as $\lambda sz.\ z$, which is exactly the definition of $\text{False}$. So when $\text{TestZero}$ is applied to $0$, it returns $\text{True}$ as shown below:

$$\begin{align*} &(\lambda n.\ n\ (\lambda w.\ \text{False})\ \text{True}) \ 0\\ \equiv \quad & (\lambda n.\ n\ (\lambda wrt.\ t)\ (\lambda xy.\ x)) (\lambda sz.\ z)\\ \stackrel{\beta}{\implies}& (\lambda sz. z)\ (\lambda wrt.\ t)\ (\lambda xy.\ x) \\ \stackrel{\beta}{\implies}& (\lambda z.\ z) (\lambda xy.\ x) \\ \stackrel{\beta}{\implies}& (\lambda xy.\ x) \\ \end{align*}$$

When it is applied to a numeral other than $0$, it returns $\text{False}$. Let’s see this for the numeral $2$.

$$\begin{align*} &(\lambda n.\ n\ (\lambda w.\ \text{False})\ \text{True}) \ 2\\ \equiv \quad & (\lambda n.\ n\ (\lambda wrt.\ t)\ (\lambda xy.\ x)) \ (\lambda sz.\ s(sz))\\ \stackrel{\beta}{\implies}& (\lambda sz.\ s(sz))\ (\lambda wrt.\ t)\ (\lambda xy.\ x) \\ \stackrel{\beta}{\implies}& (\lambda z.\ (\lambda wrt.\ t)((\lambda wrt.\ t)z))\ (\lambda xy.\ x) \\ \stackrel{\beta}{\implies}& (\lambda wrt.\ t)((\lambda wrt.\ t)(\lambda xy.\ x)) \\ \stackrel{\beta}{\implies}& (\lambda rt.\ t) \\ \end{align*}$$

Note that the effect of applying $\text{TestZero}$ to a numeral other than $0$ means that $(\lambda w.\ \text{False})$ is repeatedly applied to $\text{True}$. The repeated applications always return $\text{False}$.

Greater than or equal to#

To implement $m \geq n$, we need to test $n-m$ and see whether it’s $0$. The subtraction $n-m$ is performed by using the predecessor expression $\text{Pred}$ on the numeral $n$ repeatedly ($m$ times):

define $\text{GE} = \lambda m n.\ \text{TestZero}\ (m\ \text{Pred} \ n)$

If $m$ is strictly less than $n$, then $n-m$ is not $0$. Otherwise it is $0$.

Similarly, we can construct a lambda expression, say $\text{LE}$, to implement the less than or equal to operator $(\leq)$.

Equality#

For any two numbers $n$ and $m$, if $n \geq m$ and $n \leq m$, it implies that $n = m$. So we can check for equality between two numerals through the lambda expression:

define $\text{Equal} = \lambda nm.\ \text{And}\ (\text{GE}\ nm) (\text{LE}\ nm)$

Similarly, to check that $n \neq m$, we can use the lambda expression:

define $\text{NE} = \lambda nm.\ \text{Not}\ (\text{Equal}\ nm)$

Strict inequality#

Checking for strict inequality can be done using other operators. For example, we can check if $n$ is strictly greater than $m$ through the following lambda expression:

define $\text{GT} = \lambda nm.\ \text{And}\ (\text{GE}\ nm)\ (\text{NE}\ nm)$

We can check for strictly less than in a similar way.

define $\text{LT} = \lambda nm.\ \text{And}\ (\text{LE}\ nm)\ (\text{NE}\ nm)$

We hope that this was fun for you and that it continues to be useful to you as you learn and grow!