Formalism 101
Escaping local optima on a random walk through life.

1.1 An alphabet $\mathrm{\Sigma }$ is a finite set, it’s elements are called symbols.

1.2 Words over an alphabet $\mathrm{\Sigma }$ are sequences of symbols in $\mathrm{\Sigma }$, so a word is a function $w:\{i|i\in {\mathbb{N}}_0,i<n\}\to \mathrm{\Sigma }$, where $n:=|w|$ is the length of the word.

1.3 The empty word $ϵ$ is the sequence that doesn’t contain any symbol, so $ϵ:\mathrm{\varnothing }\to \mathrm{\Sigma }$.

1.4 Concatenating two words over $\mathrm{\Sigma }$ is the operation that joins those two words end-to-end:

$$\cdot :\{i|i\in {\mathbb{N}}_0,i<n+m\}\to \mathrm{\Sigma }.$$

1.5 The Kleene star $\ast$, also known as the free monoid construction, is a unary operation on an alphabet and we write ${\mathrm{\Sigma }}^{\ast }$ for the Kleene star applied on $\mathrm{\Sigma }$.

${\mathrm{\Sigma }}^{\ast }$ is the smallest superset of $\mathrm{\Sigma }$ that contains the empty string $ϵ$ and is closed under concatenation.

We define it inductively:

If

• ${\mathrm{\Sigma }}^0:=\{ϵ\}$ and
• $\mathrm{\forall }i\ge 0:{\mathrm{\Sigma }}^{i+1}:=\{wv|w\in {\mathrm{\Sigma }}^i,v\in \mathrm{\Sigma }\}$,

then ${\mathrm{\Sigma }}^{\ast }:=\bigcup _{i\ge 0}{\mathrm{\Sigma }}^i$.

The elements $w\in {\mathrm{\Sigma }}^{\ast }$ are exactly the words over $\mathrm{\Sigma }$.

1.6 A formal language $L\subseteq {\mathrm{\Sigma }}^{\ast }$ over an alphabet $\mathrm{\Sigma }$ is a set of words over that alphabet.

2.1 A grammar $G=(N,\mathrm{\Sigma },P,S)$ is nefined as follows:

• $N$ is an alphabet of nonterminal symbols,
• $\mathrm{\Sigma }$ is an alphabet of terminal symbols,
• $P$ is a finite set of production rules, which are elements $(p,q)\in (\mathrm{\Sigma }\cup N{)}^{\ast }N(\mathrm{\Sigma }\cup N{)}^{\ast }\times (\mathrm{\Sigma }\cup N{)}^{\ast }\text{, but we usually write }p\to q\text{ for }(p,q)$ and $p\to q_1|q_2$ for $(p,q_1),(p,q_2)$.
• $S\in N$ is the start symbol.

Note that $N\cap \mathrm{\Sigma }=\mathrm{\varnothing }$ is required, as each symbol is either nonterminal or terminal.

2.2 Every grammar $G$ defines a formal language $L(G)$ as follows:

The binary relation ${\Rightarrow }_G\subseteq (\mathrm{\Sigma }\cup N{)}^{\ast }\times (\mathrm{\Sigma }\cup N{)}^{\ast }$, called $G$ derives in one step, is defined as $$x{\Rightarrow }_{G}y⟺\mathrm{\exists }u,v,p,q\in (\mathrm{\Sigma }\cup N{)}^{\ast }:(x=upv)\wedge (y=uqv)\wedge (p\to q\in P)\text{.}$$ The binary relation ${\Rightarrow }_G^{\ast }$, called $G$ derives in zero or more steps, is the reflexive transitive closure of ${\Rightarrow }_G$. The grammar $G$ thus defines a formal language $L(G):=\{w\in {\mathrm{\Sigma }}^{\ast }|S{\Rightarrow }_G^{\ast }w\text{ in finitely many steps}\}$.

3.1 A formal system $F=(\mathrm{\Sigma },G,A,R)$ consists of

• an alphabet $\mathrm{\Sigma }$, which is a finite set of symbols,
• a grammar $G$ over $\mathrm{\Sigma }$, which describes how valid formulas can be built from the symbols in the alphabet ($L(G)$ is the set of valid formulas),
• a set of axioms and axiom schemata $A\subseteq L(G)$, which are valid formulas that are assumed to be true, and
• a set of inference rules $R\subseteq L(G)\times L(G)$ for inferring theorems from the axioms and one another.

Schemata are formulas in the metalanguage of the system that generalize formulas in that systems language and thus allow the formulation of an infinite amount of axioms of the same structure. A good example is the induction schema of the Peano axioms for the natural numbers.

Within such a system, we can use its grammar to build valid formulas from the symbols contained in its alphabet and we can use its inference rules to derive theorems from its axioms and thus prove them.

4.1 The lambda calculus is a formal system for expressing computation. Like Turing machines, it’s a universal model for doing so, i.e. the lambda calculus is turing complete. However, it’s a lot simpler and in my opinion also more elegant than the bulky Turing machines. It’s also the fundament to functional programming languages, like Haskell.

We can now use the basic concepts defined above to define the untyped lambda calculus. The untyped lambda calculus is the formal system $F_{\lambda }=({\mathrm{\Sigma }}_{\lambda },G_{\lambda },A_{\lambda },R_{\lambda })$, where

• ${\mathrm{\Sigma }}_{\lambda }=\{\lambda ,.,v,{}_0,{}_1,\dots ,{}_9,(,)\}$,
• $G_{\lambda }=\{N_{\lambda },{\mathrm{\Sigma }}_{\lambda },P_{\lambda },S_{\lambda }\}$, defined inductively,
• $A_{\lambda }=\{\mathrm{\forall }t.t=t\}$,
• $R_{\lambda }$, as defined below.

${\mathrm{\Sigma }}_{\lambda }$ contains the abstraction symbols $\lambda$ and ., the parentheses ( and ) and symbols to build variables $v_0,v_1,\dots$ from. One can define the grammar $G_{\lambda }$ by listing all productions, but we will do so inductively in the definition of lambda expressions below.

5.1 We’re writing $\mathrm{\Lambda }:=L(G_{\lambda })$ for the set of all valid lambda expressions. Here, we’re defining $\mathrm{\Lambda }$ inductively:

• Variables: All variables $v_0,v_1,\dots$ are lambda expressions, so $\mathrm{\forall }i\in {\mathbb{N}}_0:v_i\in \mathrm{\Lambda }$.
• Abstraction: For every variable $v\in \mathrm{\Lambda }$ and every $M\in \mathrm{\Lambda }$, we have $(\lambda v.M)\in \mathrm{\Lambda }$ as well.
• Application: For every $M,N\in \mathrm{\Lambda }$, we also have $(MN)\in \mathrm{\Lambda }$.

Sometimes the $v_i$’s are hard to distinguish, so we’re allowing $a,b,c,\dots$ as names for variables as well. One can easily formalize this correctly by simply adding them to ${\mathrm{\Sigma }}_{\lambda }$ and $G_{\lambda }$.

We can also define $G_{\lambda }=\{N_{\lambda },{\mathrm{\Sigma }}_{\lambda },P_{\lambda },S_{\lambda }\}$ in the ordinary way. Let $N_{\lambda }=\{S_{\lambda },V,D,D^{\prime }\}$, and let $$P_{\lambda }=\{S_{\lambda }\to V|(\lambda V.S_{\lambda })|(S_{\lambda }{S}_{\lambda }),$$ $$V\to vD,$$ $$D\to {}_0|{}_1{D}^{\prime }|\dots |{}_9{D}^{\prime },$$ $$\begin{gathered} D^{\prime }\to ϵ|{}_0{D}^{\prime }|{}_1{D}^{\prime }|\dots |{}_9{D}^{\prime } \\ \}. \end{gathered}$$