\chapter{Functional Constructs}
\newcommand*{\FunctionalConstructsPath}{../Functional-Constructs-WFB}

\begin{multicols}{2}\raggedcolumns

\section{Turing Machine}

... ... ... Turing (1936) ... ... ... Hilbert's Entscheidungsproblem

\SectionBreak

\section{The Lambda Calculus}

The $\lambda$\textit{-calculus}, introduced by Alonzo Church in the 1930s, is a formal system for defining, applying, and reasoning about functions. It is in many ways equivalent to a Turing machine, and achieves Turing completeness with only three syntactic forms. Lambda calculus forms the theoretical foundation of many functional programming languages (i.e., Haskell, Scheme, ML).

\subsection{Syntax}

In the \textit{untyped} $\lambda$-calculus, every term is built from three constructs: variables, abstractions, and applications.

\subsubsection*{Variables}

Variables are symbols representing parameters or placeholders for expressions. For instance: $$x, \quad y, \quad f, \quad z_1, \quad \mathit{foo}$$ 

\subsubsection*{Abstraction}

A function that takes input $x$ and returns $M$ is written $$\lambda x. \: M$$ where $x$ is the \textit{bound variable} (the function's parameter), and $M$ is the \textit{body} of the function.

Abstraction is the only way to create functions in $\lambda$-calculus. Comparing to other regimes, $\lambda x. \: M$ is like the `maps to' notation $x \mapsto M$ in mathematics, or \verb|x => M| in JavaScript arrow functions.

\subsubsection*{Application}

Function application is written by simply placing two terms side by side:$$M \: N$$ This means `apply function $M$ to argument $N$.'

\subsubsection*{Associativity}

Application is \textit{left-associative}, thus $$M \: N \: P = \left(M \: N\right) P$$ means `apply $M$ to $N$ first, then apply the result to $P$.' The application $$\left(\lambda x. \: M\right) N$$ means: `call the function $\lambda x. \: M$ with $N$ as the argument.'

\subsubsection*{Scope}

\begin{itemize}
    \item A variable $x$ in $\lambda x. \: M$ is \textit{bound} within $M$.
    \item A variable that is not bound is \textit{free}.
\end{itemize}

For example, if we have $\lambda x. \left(x \: y\right)$, then $x$ is bound and $y$ is free. Whether a variable is bound or free is a matter of its \textit{scope}.

\subsection{Special Functions}

Using variables, abstraction, and application, we can construct a handful of tools that will be used ubiquitously throughout $\lambda$-calculus and its derivatives. It's worth memorizing the following special functions:

\subsubsection*{Identity}

The application $$I = \lambda x. \: x$$ is called the \textit{identity function}, and simply returns its argument unchanged: $$I \: a  = \left(\lambda x. \: x\right) a \rightarrow a$$

\subsubsection*{Constant}

The application $$K = \lambda x.\lambda y. \: x$$ is called the \textit{constant function}, which returns the first of its its arguments while ignoring the second: $$K \: a \: b \rightarrow a$$

\subsubsection*{Substitution}

The application $$S = \lambda x.\lambda y.\lambda z. \: x \:z \left(y \: z\right)$$ is called \textit{substitution}, which takes three arguments $a \: b \: c$, and produces the combination $a \: c \: \left(b \: c\right)$. That is: $$S \: a \: b \: c \rightarrow a \: c \: \left(b \: c\right)$$

\subsection{Special Operations}

\subsubsection*{Beta Reduction}

Beta-reduction captures the idea of applying a function to an argument:$$(\lambda x. M)\: N \:\rightarrow_{\beta}\: M[x = N]$$
The term $M[x = N]$ denotes substituting $N$ for every occurrence of $x$ in $M$. In practice, $\beta$-reduction always gets rid of the left-most $\lambda$.

\subsubsection*{Alpha Conversion}

Two $\lambda$-expressions are equivalent up to renaming of bound variables: $$\lambda x. \: x =_{\alpha} \lambda y. \: y$$ This avoids variable name collisions. In mathematics, this is equivalent to a change of dummy variable or integration variable.

\subsubsection*{Eta Conversion}

Eta-conversion expresses functional equivalence $$\lambda x. \left(f \: x\right) =_{\eta} f$$
when $x$ does not occur as free in $f$.

\subsubsection*{Church Encoding}

Data structures and numbers can be represented purely as functions. For example: \begin{align*}0 &= \lambda f.\lambda x.\, x \\ 1 &= \lambda f.\lambda x.\, f\,x \\ 2 &= \lambda f.\lambda x.\, f(f\,x)\end{align*}

These \textit{Church numerals} allow arithmetic to be expressed without primitive numbers.

\subsection{Minimal Set}

As rock bottom as the $S$, $K$ functions may appear, these do not form a minimal set. 
Instead, we'll show that there exists a single entity $\iota$ (Greek \textit{iota}) that bringjustifess $S$ and $K$ simultaneously.

To begin, consider two (as yet unnamed) functions $A$ and $B$. Take $\iota$ as a primitive with the sole rewrite $$\iota(x) \rightarrow \left( (x)(A) \right)(B) \:,$$ and remember application is left-associative; we will nevertheless keep all parentheses explicit.

\subsubsection*{Identity}

Next we propose the identity term $$I = \left( \iota \left( \iota \right) \right) \:,$$ and test $I$ on an arbitrary argument $\left( X \right)$ using the rewrite rule alone:

\begin{align*}\left( I \left( X \right) \right) &= \left( \left( \iota \left( \iota \right) \right) \left( X \right) \right) \\ &\rightarrow \left( \left( \left( \iota \right) \left( A \right) \right) \left( B \right) \left( X \right) \right) \\ &\rightarrow \left( \left( \left( \left( \left( A \right) \left( A \right) \right) \left( B \right) \right) \left( B \right) \right) \left( X \right) \right)\end{align*} Looking at the inner part, it suffices to check whether $$J = \left( \left( \left( A \left( A \right) \right) \left( B \right) \right) \left( B \right) \right)$$ does the job of the identity function such that: $$\left(J\left(X\right)\right) = \left(I\left(X\right)\right)$$

As formally \textit{opaque} objects, we're stuck without knowing anything about $A$, $B$. To proceed, we embed the rewrite system in the $\lambda$-calculus notation such that: $$\iota = \lambda f. \: f \: A \: B$$ This lets us take advantage of $\beta$-reduction instead of staying purely at the rewrite-rule level. In this frame, we propose the forms: \begin{align*}A &= \lambda x. \lambda y. \lambda z. \: \left(x\left(z\right)\right)\left(y\left(z\right)\right) \\ B &= \lambda x. \lambda y. \: x\end{align*} If $A$, $B$ look suspiciously like $S$, $K$, you wouldn't be wrong. The motive here is to prove that the pair $A$, $B$ behaves exactly like $S$, $K$ without using $S$, $K$ as combinators.

To make sure the rewrite rule stays intact in the $\lambda$-notation, we calculate $$\iota\left(x\right) = \left(\lambda f. \: f \: A \: B\right) x \;\rightarrow_\beta\; x \: A \: B \:,$$ or, using left-associativity, $$\iota\left(x\right) = \left(\left(x\right)\left(A\right)\right)\left(B\right) \:,$$ which agrees with the first thing we wrote about $\iota$.

Now return to the matter of the identity function $$J = \left( \left( \left( A \left( A \right) \right) \left( B \right) \right) \left( B \right) \right) \:.$$ Computing this from the inside-out, we have no choice but to invoke the structure of $A$ explicitly: \begin{align*}\left(A \left(A\right)\right) &= \left(A \: A\right) \\ &= \left(\lambda x. \lambda y. \lambda z. \: \left(x\left(z\right)\right)\left(y\left(z\right)\right)\right) A \\ &\rightarrow_\beta\; \lambda y.\lambda z. \: A \: z\left(y \: z\right) \\ \left(\left(A \left(A\right)\right) \left(B\right)\right) &= \left(\left(A \: A\right)B\right) \\ &= \left(\lambda y.\lambda z. \: A \: z\left(y \: z\right)\right) B \\ &\rightarrow_\beta\; \lambda z. \: A \: z \left( B \: z\right) \\ \left( \left( \left( A \left( A \right) \right) \left( B \right) \right) \left( B \right) \right) &= \left(\left(\left(A \: A\right)B\right)B\right) \\ &= \left(\lambda z. \: A \: z \left( B \: z\right)\right) B \\ J &\rightarrow_\beta\; A \: B \left(B \: B\right)\end{align*}

Comparing $A \: B \left( B \: B\right)$ to the expression that got us here, one has to wonder where the extra $B$ came from and why there is only one $A$ on the left. This is not the result of an error - we must acknowledge that the perservation of symbol count is \textit{not} maintained in beta reduction.

To handle $\left(A \: B\right)$, we note that \begin{align*}A \: B &= \left(\lambda a.\lambda b.\lambda c. \: \left(a\left(c\right)\right)\left(b\left(c\right)\right)\right) B \\ &\rightarrow_\beta\; \left(\lambda b.\lambda c. \: \left(B\left(c\right)\right)\left(b\left(c\right)\right)\right)\end{align*} Calculating $\left(B \: B\right)$, we further find: \begin{align*}\left(B \: B\right) &= \left(\lambda x.\lambda y. \: x\right) B \\ &\rightarrow_\beta\; \left(\lambda y. \: B\right) \end{align*}

We're now in position to establish $J$ as equivalent to the identity $I$. Testing on an arbitrary variable $x$, we start with \begin{align*}J \left(x\right) &= \left(A \: B \left(B \: B\right)\right) \left(x\right) \\ &= \left(\left(A \: B\right) \left(B \: B\right)\right)\left(x\right) \:,\end{align*} and substitute $A \: B$ to have \begin{align*}J\left(x\right) &= \left(\left(\lambda b.\lambda c. \: \left(B\left(c\right)\right)\left(b\left(c\right)\right)\right) \left(B \: B\right)\right)\left(x\right) \\ &\rightarrow_\beta\; \left(\lambda c. \: \left(B\left(c\right)\right)\left(\left(B \: B\right)\left(c\right)\right) \right)\left(x\right) \\ &\rightarrow_\beta\; \left(B\left(x\right)\right)\left(\left(B \: B\right)\left(x\right)\right) \\ &= \left(B\left(x\right)\right) \left(\left(\lambda y. \: B\right)\left(x\right)\right) \\ &\rightarrow_\beta\; B \left(x\right) B\end{align*}

Utilizing $B$'s exact structure for the first time, continue with $$J\left(x\right) = \left( \left(\lambda u.\lambda v. \: u\right) \left(x\right) \right) \left(B\right)$$ (where we have $\alpha$-renamed the bound variables of $B$ to $u,v$ to avoid clash with the meta-variable $x$). Now finish by two $\beta$-reductions: $$\left( (\lambda u.\,\lambda v.\,u)\,(x) \right)\,(B) \;\rightarrow_\beta\; (\lambda v.\,x)\,(B) \;\rightarrow_\beta\; x.$$ Thus $J(x)=x$ for all $x$, i.e.\ $J$ is extensionally the identity $I$.

\subsubsection*{Deriving S, K}

To continue, define three more $\iota$-derived terms (indirectly) involving $S$, $K$: \begin{align*}C &= \left( \iota \left( I \right) \right) \\ K &= \left( \iota \left( C \right) \right) \\ S &= \left( \iota \left( K \right) \right)\end{align*} Use $\iota = \lambda f. \: f \: A \: B$ to expand $C$: $$C = \left(\lambda f. \: f \: A \: B\right) I \;\rightarrow_\beta\; I \: A \: B = A \: B$$ Then, by the rewrite rule $\iota(x) \rightarrow \left( (x)(A) \right)(B)$ we have: \begin{align*}K &\rightarrow \left( \left( C \right) \left( A \right) \right)\left( B \right) \\ &= C \: A \: B = \left(A \: B\right)A \: B\end{align*}

The quantity on the right needs to be worked out manually. We already worked out $\left(A \: B\right)$, namely: $$\left(A  \: B\right) \;\rightarrow_\beta\; \lambda b.\lambda c. \: B \: c\left(b \: c\right)$$ Append $A$ to the right and keep simplifying: \begin{align*}\left(A \: B\right) A &= \left(\lambda b.\lambda c. \: B \: c\left(b \: c\right)\right) A \\ &\rightarrow_\beta\; \lambda c. \: B \: c\left(A \: c\right)\end{align*} Append $B$ to the right and turn the crank again to find: \begin{align*}\left(A \: B\right) A \: B &= \left(\lambda c. \: B \: c\left(A \: c\right)\right) B \\ &\rightarrow_\beta\;B \: B\left(A \: B\right) \\ K^ &= B \: B\left(A \: B\right)\end{align*}

The $B \:B$-term was also previously worked out, so we continue with $$K = \left(\lambda y. \: B\right) \left(A \: B\right) \;\rightarrow_\beta\; B \:,$$ leaving just $B$. Replacing $B$ with its equivalent $\lambda$-expression, we conclude: $$K = B = \lambda x.\lambda y. \: x$$

Finally we work out how $S$ fits in. Start with \begin{align*}S &\rightarrow \left( \left( K \right) \left( A \right) \right)\left( B \right) \\ &= K \: A \: B = \left(\lambda x.\lambda y. \: x\right)A \: B \\ &\rightarrow_\beta\; A \:,\end{align*} and immedietly conclude $S$ is equivalent to $A$: $$S = A = \lambda x.\lambda y.\lambda z. \: x \: z \left(y \: z\right)$$

In summary, we find that $\iota$ contains $S$, $K$ such that: $$\iota = \lambda f. \: f \: S \: K$$

\SectionBreak

\section{The SK Calculus}

Central to the $\lambda$-calculus are two functions $S$ and $K$. These, along with other players such as iota ($\iota$) and the identity ($I$), are formally called \textit{combinators}. In particular:

\begin{center}
\begin{tabular}{|c|c|c|}
\hline
\text{Combinator} & \text{Symbol} & \text{Expression} \\ \hline
\text{Identity} & I & \lambda x. \: x \\
\text{Substitution} & S & \lambda x.\lambda y.\lambda z. \: x \: z \left(y \: z\right) \\ 
\text{Constant} & K & \lambda x.\lambda y. \: x \\ 
\text{iota} & \iota & \lambda f. \: f \: S \: K \\ \hline
\end{tabular}
\end{center}

As it turns out, we can use the pair $S$, $K$ as a basis to do any possible computation \textit{without} explicit use of variable storage. These are equivalent in expressive power to the untyped $\lambda$-calculus and serve as a foundation for certain minimalist functional programming languages.

\subsubsection*{Notation}

Using a slightly more transparent notation, the $S$, $K$ combinators read: $$S[x][y][z] = x[z][y[z]]$$ $$K[x][y] = x$$ The square brackets can help the eye and the computer's input parser sift through statements. Like training wheels though, we can get rid of most of the brackets without ambiguity: $$S \:x \: y \: z = x \: z\left(y \: z\right)$$ $$K \: x\: y = x$$

\subsubsection*{Identity}

Some introductions to $SK$-calculus actually call it $SKI$ calculus, where $I$ stands for `identity', which is it itself a combinator that can be expressed in terms of $S$, $K$. This is established by writing: $$I = S[K][K]$$ For a test, the quantity $I[a]$ must reduce to $a$, which is indeed the case: \begin{align*}I[a] &= S[K][K][a] \\ &= K[a][K[a]] \\ &= a\end{align*} Or, in the streamlined notation: $$Ia = SKKa = Ka(Ka) = a$$ As an aside, the identity can be more generally written $I = S[K][Z]$, where $Z$ stands for any symbol at all.

\subsubsection*{What are Combinators?}

The $S$ and $K$ combinators, along with any other combinators we encounter, are named for what they do operationally. A combinator simply takes inputs and recombines them as outputs. In the context of $\lambda$-calculus, however, combinators aren't simply rearranging symbols; rather these result in new variables, abstractions, and applications. The claim is we can calculate anything this way.

For a modest example, suppose we are handed the data $[a][b][c]$, and are assigned to produce the target expression $a[b[a][c]]$ using a so-far unknown operator $O$: $$O\left(\left\{S,K\right\}\right) [a][b][c] = a[b[a][c]]$$ To go about finding $O$ in typical `left to right' fashion amounts to guessing what to put before $[a][b][c]$, which is unfeasible by hand, perhaps not for a computer.

Rather, it's more straightforward to begin with the target expression and work backwards through $\lambda$-calculus. For the example on hand, one might capture the output by writing: $$F = \lambda a. \lambda b. \lambda c. \: a \left(b\left(a \: c\right)\right)$$ The goal then is to systematically convert the $\lambda$-notation back to the $SK$-notation, and the operator $O$ should be evident.

\subsection{Elimination Rules}

Consider two arbitrary terms $M$, $N$ standing for any $\lambda$-expressions. The following \textit{elimination rules} describe how $\lambda$-abstractions can be systematically expressed using only the $S$ and $K$ combinators:

If the body is exactly the variable itself, this is the identity: $$\lambda x. \: x = I = S \: K \: K$$

If $x$ is not free in $M$, i.e. the body doesn't mention the bound variable, then $\lambda x. \: M$ is the constant function $K \: M$: $$\lambda x. \: M = K \: M$$

To decompose an abstraction of an application into two smaller applications, handled recursively, one writes: $$\lambda x. \left(M \: N\right) = S \left(\lambda x. \: M\right) \left(\lambda x. \: N\right)$$ This rule is a subtle one. To see this explicitly, we note $$S \: f \: g \: x = f \: x\left(g \: x\right) \:,$$ and then let \begin{align*}f &= \left(\lambda x. \: M\right) \\ g &= \left(\lambda x. \: N\right)\end{align*} so that: $$S \: f \: g = \lambda x. \: f \: x\left(g \: x\right) = \lambda x. \left(M \: N\right)$$

Together, these rules allow any $\lambda$-expression to be \textit{eliminated} in favor of $S$ and $K$ alone.

\subsubsection*{Applied Elimination}

Returning to the example problem $$F = \lambda a. \lambda b. \lambda c. \: a \left(b\left(a \: c\right)\right) \:,$$ attack the innermost term $\lambda c. \: a \left(b\left(a \: c\right)\right)$ as follows, treating $a$, $b$ as constants with respect to $c$: \begin{align*}\lambda c. \: a \left(b\left(a \: c\right)\right) &= S \underbrace{\left(\lambda c. \: a\right)}_{K \: a} \underbrace{\left(\lambda c. \: b\left(a \: c\right)\right)}_{\text{expand}} \\ \left(\lambda c. \: b\left(a \: c\right)\right) &= S \underbrace{\left(\lambda c. \: b\right)}_{K \: b}  \underbrace{\left(\lambda c . \: a \: c\right)}_{S (K \: a) I} \\ &= S\left(K \: b\right) \left(S \left(K \: a\right) I\right)\end{align*} Thus, the result of eliminating $\lambda c$ is $$G = S\left(K \: a\right) \left(S\left(K \: b\right) \left(S \left(K \: a\right) I\right)\right) \:.$$

Now we get rid of the $\lambda b$ term by treating $a$ as constant with respect to $b$ to write: \begin{align*}\lambda b. \: G &= \lambda b. \left(\underbrace{S\left(K \: a\right)}_{\text{no }b}\right) \left(\underbrace{S\left(K \: b\right) \left(S \left(K \: a\right) I\right)}_{\text{depends on }b}\right)\end{align*} Going term by term, we have $$\lambda b. \: S\left(K \: a\right) = K \left(S\left(K \: a\right)\right)$$ and \begin{align*}\lambda b. \: S\left(K \: b\right) & \left(S \left(K \: a\right) I\right) \\ &= S \left(\underbrace{\lambda b. \: S\left(K \: b\right)}_{\text{expand}}\right) \left(\underbrace{\lambda b . \: S \left(K \: a\right) I}_{K (S ( K \: a)I)}\right) \:.\end{align*} Expanding the first term gives $$\lambda b. \: S\left(K \: b\right) = S \left(\underbrace{\lambda b . \: S}_{K \: S}\right) \left(\underbrace{\lambda b . \: K \: b}_{\text{application}}\right) \:.$$ and the final application expands as: $$\lambda b . \: K \: b = S \left(\underbrace{\lambda b . \: K}_{K \: K}\right) \left(\underbrace{\lambda b . \: b}_{I}\right) = S \left(K \: K\right) I$$ Thus, the result of eliminating $\lambda b$ yields: \begin{align*}H &= S\left(K\left(S\left(K \: a\right)\right)\right) \\ & \quad \quad S\left(S \left(K \: S\right)\left(S \left(K \: K\right)I\right)\right) \left(K \left(S \left(k \: a\right)I\right)\right)\end{align*}

By now the pattern is evident as as we finally eliminate the $\lambda a$ term from $F$. This amounts to applying the same rules, and only terms directly involving $a$ require expansion. That is, whenever $a$ appears inside $K\left( \cdots \right)$, then $a$ is not free. Occurrences nested as $\left(K \: a\right)$ inside applications trigger the $S$ rule locally. The final result can depend on how this is done, but all should be equivalent. Carrying these steps forward, one finds: \begin{align*}F &= S\left(S\left(K \: S\right) \left(S \left(K \: K\right)\right) \left(S \left(K \: S\right)K\right)\right) \\ & \quad \quad \left(S \left(K \left(S\left(S\left(K\right)K\right)\right)\right)K\right)\end{align*}

Recall that $F$ is the operator that is supposed to perform as $$O\left(\left\{S,K\right\}\right) [a][b][c] = a[b[a][c]] \:.$$ In the square bracket notation, we have: \begin{align*}O &= s[s[k[s]][s[k[k]][s[k[s]][k]]]] \\ & \quad \quad [s[k[s[s[k][k]]]][k]]\end{align*} Running the calculation forward, either by hand or machine, yields the folowing progression:

\end{multicols}

\begin{tcolorbox}
\small
\begin{verbatim}
s[s[k[s]][s[k[k]][s[k[s]][k]]]][s[k[s[s[k][k]]]][k]][a][b][c]
s[k[s]][s[k[k]][s[k[s]][k]]][a][s[k[s[s[k][k]]]][k][a]][b][c]
k[s][a][s[k[k]][s[k[s]][k]][a]][s[k[s[s[k][k]]]][k][a]][b][c]
s[s[k[k]][s[k[s]][k]][a]][s[k[s[s[k][k]]]][k][a]][b][c]
s[k[k]][s[k[s]][k]][a][b][s[k[s[s[k][k]]]][k][a][b]][c]
k[k][a][s[k[s]][k][a]][b][s[k[s[s[k][k]]]][k][a][b]][c]
k[s[k[s]][k][a]][b][s[k[s[s[k][k]]]][k][a][b]][c]
s[k[s]][k][a][s[k[s[s[k][k]]]][k][a][b]][c]
k[s][a][k[a]][s[k[s[s[k][k]]]][k][a][b]][c]
s[k[a]][s[k[s[s[k][k]]]][k][a][b]][c]
k[a][c][s[k[s[s[k][k]]]][k][a][b][c]]
a[s[k[s[s[k][k]]]][k][a][b][c]]
a[k[s[s[k][k]]][a][k[a]][b][c]]
a[s[s[k][k]][k[a]][b][c]]
a[s[k][k][b][k[a][b]][c]]
a[k[b][k[b]][k[a][b]][c]]
a[b[k[a][b]][c]]
a[b[a][c]]
\end{verbatim}
\end{tcolorbox}

\begin{multicols}{2}

The final line, namely $a[b[a][c]]$ is the target expression.

\subsection{Numbers and Arithmetic}

\subsubsection*{Whole Numbers}

Much like the Church encoding for numbers, the $S$, $K$ combinators can be layered to capture the whole numbers. One way to do so is by the following pattern: \begin{align*}0 &= K \\ 1 &= S[K] \\ 2 &= S[S[K]] \\ 3 &= S[S[S[K]]]\end{align*}

Building the case intuitively, consider the progression: $$S[K][S][K] \rightarrow K[K][S[K]] \rightarrow K$$ Since we're associating $K$ with the integer $0$, we can rewrite $0$ as a prefix $S[K]$ acting on a suffix $[S][K]$: $$0 = S[K][S][K]$$

Now we need some operation to increment $0 \rightarrow 1$, and use the same procedure on $1$ to yield $2$, and so on. Do this by proposing an operator $P$ that effectively adds one to its argument \begin{align*}1 &= P[S[K]][S][K] \\ 2 &= P[P[S[K]]][S][K] \\ 3 &= P[P[P[S[K]]]][S][K] \:,\end{align*} or: $$n = P^n S[K][S][K]$$

Note that each of these is written as a unique prefix $P[P[\cdots[S[K]]]]$ and a universal suffix $[S][K]$. With the universal suffix $\left(S\right)\left(K\right)$, the whole numbers are the prefixes $Q$ such that $$Q \left(S\right)\left(K\right) \rightarrow S^n \: K \:.$$ Here, $S^n \: K$ means $n$ left-nested copies of $S$ applied to $K$.

To go from $n$ to $n+1$, the operator $P$ must satisfy: $$\left(P \: Q\right)\left(S\right)\left(K\right) = S\left(Q\left(S\right)\left(K\right)\right)$$ A $\lambda$-term that does exactly this is: $$P = \lambda q. \lambda r. \lambda y. \: r\left(\left(q \: r\right)y\right)$$ This threads the fresh argument $r$ to both positions, then combines with $y$. Translating with the $SK$ elimination rules gives the point-free $SK$ form $$P = S\left(S\left(K \: S\right) K\right) \:,$$ or in the square bracket notation: $$P = S[S[K[S]][K]]$$

To verify that $P$ acts as the increment operator, compute for arbitrary $q,r,y$:
\begin{align*}\left(P \: q \right) r \: y &= \left(S\left(S\left(K \: S\right) K\right)q\right)r \: y \\ &= \left(\left(S \left(K \: S\right)K \: r\right)\left(q \: r\right)\right) y \\ &= \left(K \: r \: y\right) \left(\left(q \: r\right) y\right) \\ &= r \left(\left(q \: r\right) y\right)\end{align*} as required. For another sanity check, apply $P$ to $0 = S[K][S][K]$ to get $$P[S[K]][S][K] \rightarrow S[K] \:,$$ which we identify as $1$. Applying $P$ again, $$P[P[S[K]]][S][K] \rightarrow S[S[K]] \:,$$ which is $2$. Continuing in this way establishes the pattern we originally posed: $$n = S^n[K]$$

\subsubsection*{Addition Operator}

Recall the increment operator \begin{align*} P &= \lambda q.\lambda r.\lambda y.\; r \left(\left(q \: r\right) y\right) \\ &= S[S[K[S]][K]] \end{align*} that satisfies $$\left(P \: q\right) r \: y = r\left(\left(q \: r\right) y\right) \:.$$

Define the $m$-fold iterate of $P$ by \begin{align*} P^{0} \: n &= n \\ P^{m+1} \: n &= P\left(P^{m} \: n\right) \end{align*} We claim that for all prefixes $m,n$ and all $r,y$: $$\left(P^{m} \: n\right) r \: y = m \: r \left(n \: r \: y\right) \:.$$ That is, $P^{m}$ applies the step $q \rightarrow r\left(\left(q \: r\right) y\right)$ exactly $m$ times.

We prove this by induction on $m$. For $m=0$, we have $$\left(P^{0} \: n\right) r \: y = n \: r \: y$$ while $$0 \: r \left(n \: r \: y\right) = n \: r \: y \:,$$ so the base case holds. For all other $m$, we write:\begin{align*}\left(P^{m+1} \: n\right) r \: y &= \left(P\left(P^{m} \: n\right)\right) r \: y \\ &= \left(\left(\lambda q.\lambda r.\lambda y. \: r\left(\left(q \:r\right) y\right)\right) \left(P^m \: n\right)\right) r \: y \\ &\rightarrow_\beta\; \left(\lambda r.\lambda y.\: r\left(\left(\left(P^m \: n\right) r\right) y\right)\right) r \: y \\ &\rightarrow_\beta\; \left(\lambda y. r\left(\left(\left(P^m \: n\right) r\right) y\right)\right) y \\ &\rightarrow_\beta\; r\left(\left(\left(P^m \: n\right) r\right) y\right) \:.\end{align*} Now apply the induction hypothesis $$\left(P^m \:n\right) r \: y = m \: r \left(n \: r \: y\right) \:,$$ so that: $$\left(P^{m+1} \: n\right) r \: y = r\left(m \: r \left(n \: r \: y\right)\right) = (m+1) r \left(n \: r \: y\right)$$ This matches the numeral law $$(m+1) r \: z = r\left(m \: r \: z\right)$$ and the induction is complete.

With the above, we define the addition operator: $$\texttt{add} = \lambda m.\lambda n.\lambda r.\lambda y.\; m \: r \left(n \: r \: y\right)$$ Then, for the universal suffix $r = S$, $y = K$, we obtain \begin{align*} \left(\texttt{add} \: m \: n\right) S \: K &= m \: S \left(n \: S \: K\right) \\ &= S^m \left(S^n K\right) \\ &= S^{m+n} K \:,\end{align*} and so: $$\texttt{add} \: m \: n = P^m \: n$$

Finally, we need to express the addition operator in pure $SK$-notation. The details for this get quite wooly, so we'll breeze over the derivation while showing key steps. Begin by treating $m$, $r$, $n$ as constants with respect to $y$, and use the application rule \begin{align*}\lambda y. \: m \: r \left(n \: r \: y\right) &= S \left(\lambda y. \: m \: r\right) \left(\lambda y. \: n \: r \: y\right) \\ &= S \left(K \left(m \: r\right)\right) \left( S \left(K (n \: r)\right) I \right) \:.\end{align*} Next apply the rule again to the whole result. After routine expansions using $I = S K K$ and $S\left(K \: K\right)I = I$, along with the identity $$S\left(KS\right)X = \lambda z. \: S \: z \left(X \: z\right) \:,$$ one obtains the simplified form: \begin{align*}\lambda r. &\left( S (K \: S)(K \: m) \right) \left( S (K \: S)(K \: n) \right) = \\ & \quad S \left( S (K \: S) (K \: m) \right)\left( S (K \: S) (K \: n) \right)\end{align*} Abstracting $n$ and then $m$ from the expression above (omitting only routine $S/K$ bookkeeping and the use of $S(KK)I=I$) yields the point-free $SK$ term:$$\texttt{add} = S[K[S]]\left[S[K[S[K[S]]]][S[K[K]]]\right]$$

\begin{center}\line(1,0){150}\end{center}

Given two whole numbers $a,b$, represented by their $SK$ prefixes, the addition operator combines them as $$a + b = (\texttt{add})[a\:\texttt{prefix}][b\:\texttt{prefix}][S][K] \:.$$ Here the universal suffix $[S][K]$ ensures reduction to the canonical numeral form: \begin{align*}\left(\texttt{add} \: a \: b\right) S \: K &= a \: S \left(b \: S \: K\right) \\ &= S^a \left(S^b \: K\right) \\ &= S^{a+b} \: K \:.\end{align*} Thus the addition operator really implements $a+b$ within the $SK$-calculus.

\begin{center}\line(1,0){150}\end{center}

For an example, consider the sum $1 + 2 = 3$. To express this in the $SK$-calculus, we list: \begin{align*}\texttt{add} &= S[K[S]]\left[S[K[S[K[S]]]][S[K[K]]]\right] \\ 1 \texttt{ prefix} &= [S[S[K[S]][K]][S[K]]] \\ 2 \texttt{ prefix} &= [S[S[K[S]][K]] \\ & \quad \quad [S[S[K[S]][K]][S[K]]]] \\ \texttt{suffix} &= [S][K]\end{align*} Then, we append the operator, both prefixes, and the universal suffix into a single entity and simplify like crazy. To keep the notation a little simpler, let \begin{align*}f &= K[S] \\ g &= S[K[S[K[S]]]][S[K[K]]] \\ h &= S[S[K[S]][K]][S[K]]\:,\end{align*} and the calculation proceeds over thiry steps:

\end{multicols}

\begin{tcolorbox}
\small
\begin{verbatim}
s[f][g][h][s[s[f][k]][h]][s][k]
f[h][g[h]][s[s[f][k]][h]][s][k]
s[g[h]][s[s[f][k]][h]][s][k]
g[h][s][s[s[f][k]][h][s]][k]
k[s[f]][h][s[k[k]][h]][s][s[s[f][k]][h][s]][k]
s[f][s[k[k]][h]][s][s[s[f][k]][h][s]][k]
f[s][s[k[k]][h][s]][s[s[f][k]][h][s]][k]
s[s[k[k]][h][s]][s[s[f][k]][h][s]][k]
s[k[k]][h][s][k][s[s[f][k]][h][s][k]]
k[k][s][h[s]][k][s[s[f][k]][h][s][k]]
k[h[s]][k][s[s[f][k]][h][s][k]]
h[s][s[s[f][k]][h][s][k]]
s[f][k][s][s[k][s]][s[s[f][k]][h][s][k]]
f[s][f][s[k][s]][s[s[f][k]][h][s][k]]
s[f][s[k][s]][s[s[f][k]][h][s][k]]
f[s[s[f][k]][h][s][k]][s[k][s][s[s[f][k]][h][s][k]]]
s[s[k][s][s[s[f][k]][h][s][k]]]
s[k[s[s[f][k]][h][s][k]][s[s[s[f][k]][h][s][k]]]]
s[s[s[f][k]][h][s][k]]
s[s[f][k][s][h[s]][k]]
s[f[s][f][h[s]][k]]
s[s[f][h[s]][k]]
s[f[k][h[s][k]]]
s[s[h[s][k]]]
s[s[s[f][k][s][s[k][s]][k]]]
s[s[f[s][f][s[k][s]][k]]]
s[s[s[f][s[k][s]][k]]]
s[s[f[k][s[k][s][k]]]]
s[s[s[s[k][s][k]]]]
s[s[s[k[k][s[k]]]]]
s[s[s[k]]]
\end{verbatim}
\end{tcolorbox}

\begin{multicols}{2}

Perhaps not surprisingly, the final result is the representation of $3$ in the $SK$ numerals we developed. I promise to not show so much scratchwork again. If you're crunching through $SK$-calculus by hand or writing a program to do so, the above could be a useful milestone. Playing with more addition, it turns out that evaluating $3+4 = 7$ takes $50$ steps, and $30+40=70$ requires $365$ steps.

\subsubsection*{Multiplication Operator}

We may take $$\texttt{mul} = S[K[S]][K] \;,$$ also known as the composition combinator $B$, which satisfies: $$B \: x \:y \: z \rightarrow x\left(y \:z \right)$$ For a quick check on $B$, we write \begin{align*}
S\left(K \: S\right)K \: x \: y \: z &= \left(\left(\left(K \: S\right) \: x\right)\left(K \: x\right)\right) y \: z \\ &= S \left(K \: x\right) \: y \: z \\ &= \left(K \: x \: z\right)\left(y \: z\right) \\ &= x \left(y \: z\right) \:.\end{align*}

Applied to numeral prefixes $m,n$ and the universal suffix $[S][K]$ we get \begin{align*}\left(\texttt{mul} \: m \: n\right) S \: K &= \left(B \: m \: n\right) S \: K \\ &\rightarrow m \left(n \: S\right) K \\ &= \left(n \: S\right)^{m} \: K = S^{mn} \: K \:,\end{align*} so $\texttt{mul}$ indeed computes ordinary multiplication in this encoding.

Multiplication of two numbers is structurally similar to addition, with the only change being a swap of operators. The structure with prefixes and the suffix remains intact: $$a \times b = (\texttt{mul})[a\:\texttt{prefix}][b\:\texttt{prefix}][S][K] \:.$$

Despite the relative simplicity of the multiplication operator, getting final answers takes plenty of work. For instance, computing $2 \times 3 = 6$  requires $50$ steps. To frame this, one starts with \begin{align*}P &= S[S[K[S]][K]] \\ 2 &= P[P[S[K]]] \\ 3 &= P[P[P[S[K]]]] \:,\end{align*} so then: $$(\texttt{mul})[P[P[S[K]]]][P[P[P[S[K]]]]][S][K] \rightarrow S^{6}K$$

\subsubsection*{Exponent Operator}

We may take $$\texttt{exp} = S[K[S[S[K][K]]]][K] \:,$$ which acts as an operator for exponentiation of our SK-encoded numerals.  

To check the behavior, note that \begin{align*}\texttt{exp} \: m \: n \: S \: K &= \left(S[K[S[S[K][K]]]] \: m \: n \right) S \: K \\ & \rightarrow m \left( \left(n \: S \: K\right) \right) K \\ &= m \left( \left(S^{n} \:K\right) \right) K \\ &= \left(S^{n} \: K\right)^{m} \:,\end{align*} so $\texttt{exp}$ indeed computes exponentiation in this encoding: $m^n$.

Just as with addition and multiplication, exponentiation fits the general pattern
$$a^{b} = (\texttt{exp})[a\:\texttt{prefix}][b\:\texttt{prefix}][S][K] \:.$$

For example, beginning with \begin{align*}P &= S[S[K[S]][K]] \\ 2 &= P[P[S[K]]] \\ 3 &= P[P[P[S[K]]]] \:,\end{align*} we may compute $$(\texttt{exp})[P[P[S[K]]]][P[P[P[S[K]]]]][S][K] \rightarrow S^{8}K \:,$$ which corresponds to $2^3 = 8$. Or in $116$ steps, one can verify $3^2 = 9$.

\subsection{Combinatory Operations}

For a quick review of what we know of $SK$-calculus, we take the $S$, $K$ combinators \begin{align*}S \:x \: y \: z &= x \: z\left(y \: z\right) \\ K \: x\: y &= x\end{align*} as a basis for all computation. Not even the identity is fundamental, as $S \: K \: K \: x$ always returns $x$: $$I = S \: K \: K$$

\subsubsection*{Review of Arithmetic}

For arithmetic operations, we use the numerals $n = S^n K$, or in the prefix-suffix notation $$n = P^n \: S \: K \: S \: K \:,$$ where $P$ is the increment operator $$\texttt{increment} = P = S\left(S\left(K \: S\right)K\right) \:.$$ Then, numerals are written as $$n \texttt{ prefix} = P^n S \: K$$ with: $$\texttt{suffix} = S \: K$$

We take $\tilde{O}$ as the addition, multiplication, or exponent operator for whole numbers, represented by \texttt{O}. Arithmetic operations are constructed via $$a \: \tilde{O} \: b = (\texttt{O})[a\:\texttt{prefix}][b\:\texttt{prefix}][S][K] \:.$$ For a list of operators, we found: \begin{align*}\texttt{add} &= S\left(KS\right)\left(S\left(K\left(S \: K \: S\right)\right)I\right) \\ \texttt{mul} &= S \left(K \: S\right) K \\ \texttt{exp} &= S\left(K\left(S \: I\right)\right)K\end{align*}

\subsubsection*{Self-Apply}

One of the most fundamental non-arithmetic operations in $SK$-calculus is forcing an object to act on itself. Given some $x$, how do we calculate $x \: x$? (Recall that in our streamlined notation, $x \: x$ also means $x[x]$.)  

The answer is the \texttt{self} operator: $$\texttt{self} = S \: I \: I \:,$$ where $I = S \: K \: K$ is the identity. For a quick check, one writes \begin{align*}S \: I \: I \: x &= I \: x \left(I \: x\right) \\ &= x \left(I \: x\right) \\ &= x \: x\end{align*} Thus $S \: I \: I$ is the unique combinator that enforces self-application. Self-application is the simplest non-trivial operation in combinatory logic. While arithmetical operators like $\texttt{add}$ or $\texttt{mul}$ encode finite algebra, the \texttt{self} operator opens the door to infinite structures and recursion.

Restoring the full bracketed notation, the evaluation begins and ends as: $$S[S[K][K]][S[K][K]][x] \rightarrow x[x] \:.$$
 
\subsubsection*{Cyclic Expression}

As with any programming tool, it is possible to create an infinite loop in $SK$-calculus. In this setting, an `infinite loop' corresponds to a combinatory expression that eventually reproduces itself after some number of reductions. Once this happens, the computation no longer progresses but cycles forever.  

One of the simplest such expressions is built from the self-apply operator: $$\texttt{loop} = \left(S \: I \: I\right)\left(S \: I \: I\right) \:.$$

Let us unroll this step by step. Beginning in streamlined notation:
\begin{align*}\left(S \: I \: I\right)\left(S \: I \: I\right) &= I\left(S \: I \: I\right)\left(I\left(S \: I \: I\right)\right) \\ &= \left(S \: I \: I\right)\left(I\left(S \: I \: I\right)\right) \\ &= \left(S \: I \: I\right)\left(S \: I \: I\right) \:.\end{align*}

By the third step the expression has returned to its original form. The evaluation never halts: each attempt to simplify merely reproduces the starting point. This is a genuine cyclic expression. Restoring full bracketed notation, the loop is written: $$\texttt{loop} = S[S[K][K]][S[K][K]]$$ such that \begin{align*}\texttt{loop} [\texttt{loop}] \rightarrow \texttt{loop} [\texttt{loop}] \:.\end{align*}

\subsubsection*{Swap}

Another natural question in combinatory logic is whether we can reverse the order of two objects. Given a compound expression $x \: y$, can we produce $y \: x$? The combinator that accomplishes this is the \texttt{swap} operator: $$\texttt{swap} = S\left(K(S \:I)\right)\left(S\left(K \: K\right)I\right) \:,$$ where $I = S \: K \: K$ is the identity.

Testing the definition shows that it indeed flips the order: \begin{align*}S\left(K\left(S \:I\right)\right) & \left(S\left(K \:K\right)I\right) \: x \: y \\ &= \left(K\left(S \: I\right) \: x\right)\left(S\left(K \: K\right)I \: x\right) \: y \\ &= \left(S \: I\right)\left(S\left(K \: K\right)I \: x\right) \: y \\ &= I \: y \left(x \: y\right) \\ &= y \: x\end{align*}

The final result is clear: $\texttt{swap}$ faithfully exchanges the two arguments. This confirms that $SK$-calculus is not limited to building and combining terms, but also permits us to rearrange their order - a subtle but important structural operation thjat embodies symmetry within combinatory logic. In the full bracketed notation, the transformation begins and ends as: \begin{align*}S[K[S[S[K][K]]]][S[K[K]][S[K][K]]] & [x][y] \\ & \rightarrow y[x]\end{align*}

\subsubsection*{Self-Reference}

We now arrive at one of the most profound constructions in $SK$-calculus: self-reference. Unlike \texttt{self}, which forces an object to act upon itself, self-reference ties an object's behavior to its own description, opening the door to recursion and conditional recursion.  

Consider the curious combination $$R = S \left(K \:x\right)\left(S \:I \: I\right) \:,$$ where $x$ is some as-yet unspecified object. Let us allow $R$ to act on an argument $y$: \begin{align*}S\left(K \: x\right)\left(S \: I\: I\right) y &= \left(K \: x \: y\right)\left(S \: I \: I \: y\right) \\ &= x \left(S \: I \: I \: y\right) \\ &= x \left(I \: y\left(I \: y\right)\right) \\ &= x \left(y \: y\right) \:.\end{align*} In other words, $R$ transforms $y$ into two consecutive copies of itself before passing them into $x$. In full bracketed notation, the process reads $$S[K[x]][S[S[K][K]][S[K][K]]][y] \rightarrow x[y[y]] \:.$$

The real depth of this construction emerges when we let $R$ act on itself: \begin{align*} R\left(R\right) &= S\left(K \: x\right)\left(S \: I \: I\right)\left(S\left(K \: x\right)\left(S \: I \: I\right)\right) \\ &= x\left(\left(S \: I \: I\right)\left(S\left(K \: x\right)\left(S \: I \: I\right)\right)\right) \\ &= x\left(S \: I \: I\left(S\left(K \: x\right)\left(S \: I \: I\right)\right)\right) \\ &= x\left(S\left(K \: x\right)\left(S \: I \: I\right)\left(S\left(K \: x\right)\left(S \: I \: I\right)\right)\right) \\ &= x\left(R\left(R\right)\right)\end{align*} The final step shows that we have returned to the original form, but now wrapped once more in $x$. This establishes a \textit{self-reproducing loop}: $R$ applied to itself yields $x$ applied to $R\left(R\right)$, which in turn expands in the same way, indefinitely.

By constructing $R$, we see that $SK$-calculus is capable not only of finite computation but also of infinite recursion and self-sustaining definitions. The pattern foreshadows the famous fixed-point combinators (such as Curry's $Y$ combinator) that allow functions to reference themselves without explicit naming.  

\SectionBreak

\section{Functions}

\subsection{Functions in Mathematics}

In mathematics, a \textit{function} is a mapping from a set of \textit{inputs} (the \textit{domain}) to a set of \textit{outputs} (the \textit{range}), with the rule that each input is associated with exactly one output.

To define a function, one formally one writes: \begin{align*}f : X &\to Y \\ x &\mapsto f(x)\end{align*} Such a definition contains two pieces of information. By writing $$f : X \to Y \:,$$ one speaks of `a function from $X$ to $Y$', where $X$ is the set of allowed inputs (domain), and $Y$ is the set of allowed outputs (range). The statement $$\quad x \mapsto f(x)$$ means `from $X$, take an element $x$ and send it to $f$ to return $f\left(x\right)$'.

To summarize the definition of a mathematical function, we could say: Define $f$ as a rule that assigns to each element $x$ in $X$ exactly one element $f\left(x\right)$ in $Y$.

A function is often defined by an explicit formula, a table, or an algorithm. Examples include: \begin{align*}f\left(x\right) &= x^2 \\ g\left(x\right) &= \sin\left(x\right)\end{align*}

The mathematical function is \textit{deterministic} - the same input always produces the same output - and has no notion of `memory' or \textit{state}. This purity is what later inspires \textit{pure functions} in programming.

\subsection{Functions in Programming}

In programming, a function is a named (or anonymous) block of code that takes arguments and produces a result. The general form is: $$f\left(\texttt{arguments}\right) \rightarrow \texttt{result}$$

Note the above is much less strict than the mathematical definition of a function. For this reason, programming functions may:

\begin{itemize}
\item Calculate a value from their inputs (\textit{pure functions})
\item Perform actions such as printing to the screen or modifying data in memory (\textit{impure functions})
\item Capture variables from surrounding scopes (\textit{closures})
\end{itemize}

Unlike mathematical functions, programming functions can have \textit{side effects} and may depend on or change state.

\subsubsection*{Purity and State}

A function is \textit{pure} if:

\begin{enumerate}
\item Its output depends solely on its input arguments.
\item It has no observable side effects.
\end{enumerate}

Pure functions are \textit{referentially transparent}, meaning they can be replaced by their output without changing program behavior.

An \textit{impure} function interacts with state - variables, files, networks, user interfaces - or produces effects beyond returning a value.

\subsubsection*{Side Effects}

Side effects include:

\begin{itemize}
\item Modifying global or static variables
\item Writing to files or databases
\item Printing or logging
\item Changing object properties
\end{itemize}

While often necessary, side effects reduce predictability and testability.

\subsection{Functional Programming}

\subsubsection*{Higher-Order Functions}

A \textit{higher-order function} is any function that takes another function as an argument, returns a function as its result, or both.  
They are the building blocks of functional programming, allowing control structures, data transformations, and abstractions to be expressed as reusable operations.

Examples in $\lambda$-calculus: \begin{align*}\texttt{map} &= \lambda f.\lambda x \: s \cdots \\ \texttt{compose} &= \lambda f.\lambda g.\lambda x. \: f\left(g\:x\right)\end{align*}

\subsubsection*{Function Composition}

Function composition combines two or more functions to produce a new one: $$\left(h \circ g\right)\left(x\right) = h\left(g\left(x\right)\right)$$ That is, if \begin{align*}g &: X \to Y \\ h &: Y \to Z\end{align*} then $$h \circ g : X \to Z \:.$$ Composition allows the creation of pipelines where data flows through transformations step by step.

Composition is \textit{associative}, i.e. $$f \circ \left(g \circ h\right) = \left(f \circ g\right) \circ h \:,$$ so grouping does not matter, only the order of application.

\subsubsection*{Currying}

\textit{Currying} transforms a multi-argument function into a chain of single-argument functions. In $\lambda$-calculus: $$\lambda \left(x, y\right). \: f\left(x, y\right) \quad\rightarrow\quad \lambda x.\lambda y.\: f\left(x, y\right)$$ Named after logician Haskell Curry, currying makes partial application straightforward and supports \textit{point-free} style programming.

For an example accessible to many programming languages, consider: $$\texttt{add} = \lambda x. \left(\lambda y.\: x + y\right)$$ A curried version of this is built by the concatenation of \texttt{add} and one input argument, say $3$, to make $\texttt{add3}$. The purpose of $\texttt{add3}$ is to add $3$ to the single argument sent to the function. We build such a function as follows: \begin{align*}\texttt{add3} &= \left(\lambda x.\lambda y. \: x+y\right)3 \\ &\rightarrow_\beta\; \lambda y. \: 3+y\end{align*} Then, the expression $\texttt{add3}\left(5\right)$ returns $8$.

\subsubsection*{Partial Application}

Currying immediately implies the notion of \textit{partial application}, which is the process of fixing some arguments of a function to create a new function with fewer arguments. We just witnessed the partial application $$\texttt{add3} = \texttt{add}(3)$$ to produce a function that increments its argument by $3$.

\subsubsection*{Point-Free Style}

\textit{Point-free} (or tacit) style expresses a function without explicitly mentioning its arguments.

Example: $$\texttt{squaresum} = \texttt{sum} \circ \texttt{map}(\texttt{square})$$ instead of: $$\texttt{squaresum} \: x \: s = \texttt{sum}\left(\texttt{map}\left(\texttt{square}, x \: s\right)\right)$$

This style works naturally in a curried and compositional setting, but can reduce readability if overused.

\subsubsection*{Recursion}

Functional programming languages without built-in named recursion can express it using \textit{fixed-point combinators}.  
The most famous, the $Y$ combinator, allows a function to call itself indirectly:
\[
Y\,f = f\,(Y\,f)
\]

In lazy languages like Haskell, $Y$ can be used directly; in strict languages, a variant such as the $Z$ combinator avoids immediate infinite application.

\subsubsection*{Laziness and Strictness}

\textit{Lazy evaluation} delays computation until a result is needed.  
\textit{Strict evaluation} computes arguments before applying a function.

Many combinator patterns, especially those involving infinite data structures or fixed-point combinators, work naturally in lazy evaluation but require care in strict settings.

\subsection{Combinators}

In the broadest sense, a \textit{combinator} is a higher-order function with no free variables - it is defined entirely in terms of its arguments and function application.  
In $\lambda$-calculus notation, every variable in a combinator's body is bound by a preceding $\lambda$.

Combinators are the building blocks of \textit{combinatory logic}, a variable-free alternative to the $\lambda$-calculus.

\subsubsection*{General vs. Specialised Combinators}

We can classify combinators into several overlapping categories:

\begin{enumerate}
    \item \textbf{Basic combinators:}  
    The simplest combinators that perform minimal transformations:
    \[
    I = \lambda x. \: x \quad\text{(Identity)}
    \]
    \[
    K = \lambda x. \lambda y. x \: \quad\text{(Constant)}
    \]
    \[
    S = \lambda x. \lambda y. \lambda z. \: x \:z \left(y\:z\right) \quad\text{(Substitution)}
    \]
    Many combinatory systems take these as primitives.

    \item \textbf{Derived combinators:}  
    Any combinator that can be expressed in terms of the basic set.  
    For example, the identity $I$ can be expressed in SK calculus as:
    \[
    I = S\,K\,K
    \]
    Even complex recursion-supporting combinators can be reduced to S and K.

    \item \textbf{Fixed-point combinators:}  
    A combinator $F$ is a \textit{fixed-point combinator} if:
    \[
    F\,f = f\,(F\,f)
    \]
    This means $F$ produces a fixed point of its argument function $f$.  
    The most famous example is the \textbf{Y combinator}:
    \[
    Y = \lambda f.\, (\lambda x. f\,(x\,x))\,(\lambda x. f\,(x\,x))
    \]
    Every fixed-point combinator is a combinator in the general sense, but not every combinator is a fixed-point combinator.

    \item \textbf{Special-purpose combinators:}  
    These are designed for specific behaviors, such as:
    \[
    \Omega = (\lambda x. x\,x) (\lambda x. x\,x)
    \]
    which loops indefinitely (non-terminating self-application).  
    $\Omega$ is not a fixed-point combinator - it never produces a usable fixed point - but it is still a combinator.

\end{enumerate}

\SectionBreak

\section{Automata}

\subsection{Wolfram}

\subsection{Conway}










\end{multicols}





