The Universality of the Lambda Calculus

In this post, I will demonstrate that the lambda calculus can simulate any Turing machine.

Turing Machines

Turing machines are a model of computation representing an abstract machine.

Conceptually, a Turing machine consists of a tape of unlimited extent that is divided into discrete cells (where each cell is either blank or populated with an abstract symbol), a head that is positioned adjacent to a single cell, and a state that is an abstract symbol selected from a finite set of symbols.

The contents of the tape, head position, and the current state comprise a configuration of the machine. Each machine begins with an initial configuration.

The operation of the machine is specified by a finite set of transition rules that indicates how to transition from the current configuration to the next configuration. There is at most one transition rule per combination of current state and current head symbol (i.e., the machine is deterministic). Each transition updates the configuration by overwriting the symbol in the cell adjacent to the head, moving the head one cell to the left or right, and updating the current state. If no rule matches the current configuration, then the machine halts. If the machine halts in an accepting state (or final state), the machine accepts its input, otherwise it rejects its input. The transition rules can be depicted by a transition diagram as in the following figure.

We now state the formal definitions of Turing machines and their configurations. First, we make a few preliminary definitions.

Options

We will make use of optional values, so we make the following definition:

\[\mathrm{Option}(A) = A \sqcup \{\bot\} = \{\mathrm{some}(a) \mid a \in A\} \cup \{\mathrm{none}\}.\]

We write left tag of the disjoint union as \(\mathrm{some}(a)\) and we write the right tag of the disjoint union as \(\mathrm{none}\).

Lists

We will make use of lists (i.e., finite sequences) of symbols, so we define lists as follows.

Definition (List). A list of symbols over an alphabet \(A\) is an element of the set \(A^*\) defined inductively as follows:

• \(\varepsilon \in A^*\) (the empty list is included);
• \(h \cdot t \in A^*\) whenever \(h \in A\) and \(t \in A^*\) (the construction of a list from a head symbol \(h\) and a tail list \(t\) is included).

More formally, we define an ambient set \(U\) as the set of all finite sequences over the alphabet \(A\), i.e.,

\[U = \{f : n \rightarrow A \mid n \in \mathbb{N}\}\]

where the set \(\mathbb{N}\) is taken as the set of all von Neumann numerals. We then define a monotone operator on the powerset lattice \((\mathcal{P}(U), \subseteq)\) as follows:

\[F_{A^*}(L) = \{\varepsilon\} \cup \{h \cdot t \mid h \in A, t \in L\}\]

where \(\varepsilon = \emptyset \in A^0\) is the unique empty list and, for any element \(h \in A\) and finite sequence \(t\) of length \(n\), \(h \cdot t\) is the finite sequence of length \(n+1\) defined for \(0 \le i \lt n\) as

• \((h \cdot t)_0 = h,\)
• \((h \cdot t)_{i+1} = t_i.\)

The set of all lists is then defined as the least fixed point of this operator:

\[A^* = \mu F_{A^*}.\]

In fact, \(A^* = U\). The purpose of this definition is to make the inductive structure of finite sequences explicit. We will make use of lists of symbols (representing portions of the tape) and lists of rules (representing the transition function).

Association Lists

We also make use of a special case of lists called association lists which model finite partial functions. They are essentially lookup lists containing key-value pairs where each key is guaranteed to occur at most once within the list. The purpose of this definition is to impose a unique inductive structure on such partial functions and to mirror the corresponding lambda combinators.

Definition (Association List). An association list with keys in a set \(K\) and values in a set \(V\) is an element of the set \(K \rightharpoonup V\) defined inductively as follows:

• \(\varepsilon\in K \rightharpoonup V\) (the empty list is included);
• \((k,v) \cdot t \in K \rightharpoonup V\) whenever \((k,v) \in K \times V\) and \(t \in K \rightharpoonup V\) and \(k \notin \mathrm{keys}(t)\).

Here, \(\mathrm{keys}(t) = \pi_1(t)\), i.e., it is simply the first projection.

More formally, we define an ambient set \(U\) as the set of all finite sequences over the alphabet \(A = K \times V\), i.e.,

\[U = \{f : n \rightarrow A \mid n \in \mathbb{N}\}\]

where the set \(\mathbb{N}\) is taken as the set of all von Neumann numerals. We then define a monotone operator on the powerset lattice \((\mathcal{P}(U), \subseteq)\) as follows:

\[F_{ A \rightharpoonup B}(L) = \{\varepsilon\} \cup \{(k,v) \cdot t \mid (k,v) \in K \times V, t \in L, k \notin \mathrm{keys}(t)\}.\]

The set of all association lists is defined as the least fixed point of this operator:

\[K \rightharpoonup V = \mu F_{K \rightharpoonup V}.\]

We define the \(\mathrm{lookup} : (K \rightharpoonup V) \times K \rightarrow \mathrm{Option}(V)\) operation by structural recursion as follows:

• \(\mathrm{lookup}(\varepsilon, k') = \mathrm{none}\),
• \(\mathrm{lookup}((k,v) \cdot t, k') = \begin{cases}\mathrm{some}(k) & \text{if } k = k' \\ \mathrm{lookup}(t, k') & \text{otherwise},\end{cases}\)

Turing Machines

Definition (Turing Machine). A Turing machine is a \(7\)-tuple

\[\left(Q, \Gamma, b, \Sigma, \delta, q_0, F\right)\]

where

• \(Q\) is a finite, non-empty set of states;
• \(\Gamma\) is a finite, non-empty set of tape alphabet symbols;
• \(b \in \Gamma\) is a designated blank symbol;
• \(\Sigma \subseteq \Gamma \setminus \{b\}\) is a designated set of input symbols;
• \(\delta \in ((Q \setminus F) \times \Gamma) \rightharpoonup (Q \times \Gamma \times D)\) is an association list of rules, where \(D = \{L, R\}\) is the set of directions (left or right, respectively);
• \(q_0 \in Q\) is the initial state;
• \(F \subseteq Q\) is the set of final states.

Configurations

Definition (Configuration). A configuration of a Turing Machine is a triple

\[(q, l, r)\]

where

• \(q \in Q\) is the current state,
• \(l \in \Gamma^*\) is a list of tape symbols to the left of the current head position, where the head of this list represents the symbol immediately to the left of the machine head,
• \(r \in \Gamma^*\) is a list of tape symbols at and to the right of the current head position, where the symbol at the current head position is the head of this list.

Note that the head position is implicit in this representation. Though each portion of the tape is finite, there is no bound on the length of each sequence, so the tape is unlimited in extent.

The initial configuration is constrained as follows.

Definition (Initial Configuration). An initial configuration of a Turing Machine is a triple

\[(q_0, \varepsilon, r)\]

where \(\varepsilon\) is the empty sequence and \(r \in \Sigma^*\).

For any given Turing machine, we use the abbreviation \(\mathcal{C} = Q \times \Gamma^* \times \Gamma^*\).

Definition (Single Step Transition). The single step transition relation between a configurations \(C\) and \(C'\) is defined as

\[C \xrightarrow{\delta} C' \Leftrightarrow \mathrm{step}(\delta, C) = \mathrm{some}(C')\]

where

• \(\mathrm{step}(\delta, (q,l,\varepsilon)) = \mathrm{eval\_trans}(\delta, q, b, l, \varepsilon)\),
• \(\mathrm{step}(\delta, (q, l, h \cdot t)) = \mathrm{eval\_trans}(\delta, q, h, l, t)\),

and

\[\mathrm{eval\_trans}(\delta, q, s, l, r) = \begin{cases}\mathrm{none} & \text{if } \mathrm{lookup}(\delta, (q, s)) = \mathrm{none} \\ \mathrm{apply\_trans}(c', l, r) & \text{if } \mathrm{lookup}(\delta, (q, s)) = \mathrm{some}(c')\end{cases}\]

and

• \(\mathrm{apply\_trans}((q', s', L), l, r) = \mathrm{move\_left}(q', s', l, r)\),
• \(\mathrm{apply\_trans}((q', s', R), l, r) = \mathrm{move\_right}(q', s', l, r)\),

and

• \(\mathrm{move\_left}(q', s', \varepsilon, r) = (q', \varepsilon, b \cdot s' \cdot r)\),
• \(\mathrm{move\_left}(q', s', h \cdot t, r) = (q', t, h \cdot s' \cdot r)\),

and

\[\mathrm{move\_right}(q', s', l, r) = (q', s' \cdot l, r).\]

Data Types

Our goal is to simulate a Turing machine via an appropriately constructed lambda term. We will introduce the data types and combinators needed to define such a simulator. See this previous post for more information about encodings in the lambda calculus.

Booleans

data Bool = True | False

\[\text{TRUE} \equiv \lambda t . \lambda f . t,\]

\[\text{FALSE} \equiv \lambda t . \lambda f . t,\]

\[\text{IF} \equiv \lambda c . \lambda t . \lambda f . c ~ t ~ f.\]

\[\text{AND} \equiv \lambda a . \lambda b . a ~ (b ~ \text{TRUE} ~ \text{FALSE}) ~ \text{FALSE}.\]

Options

data Option A = None | Some A

\[\text{NONE} \equiv \lambda n . \lambda s . n,\]

\[\text{SOME} \equiv \lambda a . \lambda n . \lambda s . s~a.\]

Tuples

data Tuple2 A B = Pair A B
data Tuple3 A B C = Triple A B C

\[\text{PAIR} \equiv \lambda a . \lambda b . \lambda p . p ~ a ~ b,\]

\[\text{TRIPLE} \equiv \lambda a . \lambda b . \lambda c . \lambda t . t ~ a ~ b ~ c.\]

Finite Enumerations

data Enum = Variant1 | Variant2 | ... | VariantN

\[\text{VARIANT}_i \equiv \lambda v_1 . \dots \lambda v_i . \dots \lambda v_n . v_i.\]

\[\text{EQ} \equiv \lambda a . \lambda b . a ~ (b ~ \text{TRUE} \dots \text{FALSE}) \dots (b ~ \text{FALSE} \dots \text{TRUE}).\]

Lists

data List A = Empty | Cons A (List A)

\[\text{EMPTY} \equiv \lambda e . \lambda c . e,\]

\[\text{CONS} \equiv \lambda h . \lambda t . \lambda e . \lambda c . c ~ h ~ t.\]

Association Lists

An association list is a list of key-value pairs. It is used to model a function from a finite set to another set. The \(\text{LOOKUP}\) combinator models function evaluation.

lookup Empty eq key = None
lookup (Cons head tail) eq key = 
  let (key', value) = head in 
    if eq key key' 
    then (Some value) 
    else lookup eq key tail

\[\text{LOOKUP} \equiv \text{FIX}(\lambda r . \lambda l . \lambda e . \lambda k . l ~ \text{NONE} ~ (\lambda h . \lambda t . h ~ (\lambda k' . \lambda v . \text{IF} ~ (e ~ k ~ k') ~ (\text{SOME} ~ v) ~ (r ~ e ~ k ~ t))).\]

The Step Combinator

step rules config =
  let Triple state left right = config in
    match right with
      Empty        => eval_trans state blank left Empty
      (head, tail) => eval_trans state head left tail

\[\text{STEP} \equiv \lambda \delta . \lambda c . c ~ (\lambda q . \lambda l . \lambda r . r ~ (\text{EVAL-TRANS} ~ \delta ~ q ~ \text{BLANK} ~ l ~ \text{EMPTY}) ~ (\lambda h . \lambda t . \text{EVAL-TRANS} ~ \delta ~ q ~ h ~ l ~ t))\]

eq_state State1 State1 = True
...
eq_state _ _ = False

eq_symbol Symbol1 Symbol1 = True
...
eq_symbol _ _ = False

eq_pair eq_a eq_b (Pair a1 b1) (Pair a2 b2) = and (eq_a a1 a2) (eq_b b1 b2)

eq_key = eq_pair eq_state eq_symbol

\[\text{EQ-PAIR} \equiv \lambda e_1 . \lambda e_2 . \lambda p_1 . \lambda p_2 . p_1 (\lambda a_1 . \lambda b_1 . p_2 (\lambda a_2 . \lambda b_2 . \text{AND} ~ (e_1 a_1 a_2) ~ (e_1 b_1 b_2))).\]

\[\text{EQ-KEY} \equiv \text{EQ-PAIR} ~ \text{EQ-STATE} ~ \text{EQ-SYMBOL}.\]

eval_trans rules state symbol left right = 
  match lookup rules eq_key (Pair state symbol) with
    None        => None
    Some update => apply_trans update left right

\[\text{EVAL-TRANS} \equiv \lambda \delta . \lambda q . \lambda s . \lambda l . \lambda r . (\text{LOOKUP} ~ \delta ~ \text{EQ-KEY} ~ (\text{PAIR} ~ q ~ s) ) ~ \text{NONE} ~ (\lambda c' . \text{APPLY-TRANS} ~ c' ~ l ~ r).\]

apply_trans update left right = 
  let Triple state symbol direction = update in
    match d with
      Left  => move_left state symbol left right
      Right => move_right state symbol left right

\[\text{APPLY-TRANS} \equiv \lambda c . \lambda l . \lambda r . c ~ (\lambda q ' . \lambda s' . \lambda d . d ~ (\text{MOVE-LEFT} ~ q' ~ s' ~ l ~ r) ~ (\text{MOVE-RIGHT} ~ q' ~ s' ~ l ~ r))\]

move_left state symbol left right =
  match left with
    Empty            => Triple state Empty (Cons blank (Cons symbol right))
    (Cons head tail) => Triple state tail (Cons head (Cons symbol right))

\[\text{MOVE-LEFT} \equiv \lambda q' . \lambda s' . \lambda l . \lambda r . l ~ (\text{TRIPLE} ~ q' ~ \text{EMPTY} ~ (\text{CONS} ~ \text{BLANK} ~ (\text{CONS} ~ s' ~ r))) ~ (\lambda h. \lambda t . \text{TRIPLE} ~ q' ~ t ~ (\text{CONS} ~ h ~ (\text{CONS} ~ s' ~ r))).\]

move_right state symbol left right = Triple state (Cons symbol left) right

\[\text{MOVE-RIGHT} \equiv \lambda q' . \lambda s' . \lambda l . \lambda r . \text{TRIPLE} ~ q' ~ (\text{CONS} ~ s' ~ l) ~ r.\]

run rules config = 
  match step rules config with
  None => config
  Some config' => config'

\[\text{RUN} \equiv \text{FIX}(\lambda r . \lambda \delta . \lambda c . (\text{STEP} ~ \delta ~ c) ~ c ~ (\lambda c' . r ~ \delta ~ c')).\]

Interpretations

First, we define an operation \(\ulcorner \cdot \urcorner\) that maps various sets to lambda values (element of \(V(\emptyset)\)). The operation itself is defined over various sets, but we use a single notation for uniformity.

Options

\[\ulcorner \mathrm{none} \urcorner = \text{NONE},\]

\[\ulcorner \mathrm{some}(a) \urcorner = \text{SOME}~\ulcorner a \urcorner.\]

Lists

\[\ulcorner \varepsilon \urcorner = \text{EMPTY},\]

\[\ulcorner h \cdot t \urcorner = \text{CONS}~ \ulcorner h \urcorner ~ \ulcorner t \urcorner,\]

Association Lists

\[\ulcorner \varepsilon \urcorner = \text{EMPTY},\]

\[\ulcorner (k,v) \cdot t\urcorner = \text{CONS}~ (\text{PAIR} ~\ulcorner k \urcorner ~ \ulcorner v \urcorner) ~ \ulcorner t \urcorner,\]

Tuples

\[\ulcorner (k, v) \urcorner = \text{PAIR}~\ulcorner k \urcorner ~\ulcorner v \urcorner,\]

\[\ulcorner (q, l, r) \urcorner = \text{TRIPLE}~\ulcorner q \urcorner~\ulcorner l \urcorner~\ulcorner r \urcorner.\]

Enums

\[\ulcorner e \urcorner = \ulcorner \mathrm{variant}(e) \urcorner,\]

where, since \(e \in E\) and \(E\) is a finite, non-empty set, there exists a bijection \(f_E : E \rightarrow n+1\) for some natural number \(n \in \mathbb{N}\) and therefore

\[\mathrm{variant}(e) = (f_E(e), n),\]

and then, subsequently,

\[\ulcorner (i, 0) \urcorner = (\lambda v_0 . v_i),\]

\[\ulcorner (i, n+1) \urcorner = (\lambda v_{n+1} . \ulcorner (i, n) \urcorner).\]

Lemmas

We prove a few key lemmas.

Note that we exploit the fact that term equivalence (i.e., applicative bisimilarity) is a congruence. We also ensure that all arguments \(N\) to applications are values (elements of \(V(\emptyset)\)) so that it additionally holds by both the call-by-name and call-by-value variants of applicative bisimilarity that

\[M_1'[N/x] \sim_{\mathrm{s}} M_2'[N/x]\]

whenever

\[(\lambda x . M_1') \sim_{\mathrm{s}} (\lambda x . M_2').\]

This way, we can reason generically about both the call-by-name and call-by-value evaluation strategies without worrying about their operational differences.

Definition (Definability of Equality). A combinator \(\text{EQ} \in V(\emptyset)\) defines equality of elements in a set \(K\) if, for all \(k_1, k_2 \in K\),

\[k_1 = k_2 \Rightarrow \text{EQ}~\ulcorner k_1 \urcorner~\ulcorner k_2 \urcorner \sim_{\mathrm{s}} \text{TRUE}\]

and

\[k_1 \ne k_2 \Rightarrow \text{EQ}~\ulcorner k_1 \urcorner~\ulcorner k_2 \urcorner \sim_{\mathrm{s}} \text{FALSE}.\]

Lemma (Lookup). For any association list \(\delta \in K \rightharpoonup V\) over finite sets \(K\) and \(V\) and element \(k \in K\), if there exists a combinator \(\text{EQ}\) that defines equality for \(K\), then

\[(\text{LOOKUP}~\ulcorner \delta \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner) \sim_{\mathrm{s}} \ulcorner \mathrm{lookup}(\delta, k) \urcorner.\]

Proof. We proceed by structural induction on the association list \(\delta\).

Base Case \((\delta = \varepsilon)\). By definition, \(\mathrm{lookup}(\varepsilon, k) = \mathrm{none}\) and so

\[\ulcorner \mathrm{lookup}(\varepsilon, k) \urcorner = \ulcorner \mathrm{none} \urcorner = \text{NONE}.\]

Since \(\ulcorner \delta \urcorner = \ulcorner \varepsilon \urcorner = \text{EMPTY}\) and

\[\text{LOOKUP} \sim_{\mathrm{s}} \lambda l . \lambda e . \lambda k . l ~ \text{NONE} ~ (\lambda h . \lambda t . h ~ (\lambda k' . \lambda v . \text{IF} ~ (e ~ k ~ k') ~ (\text{SOME} ~ v) ~ (\text{LOOKUP}~ t ~ e ~ k)),\]

it follows that

\begin{align*}\text{LOOKUP}~\ulcorner \delta \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner &= \text{LOOKUP}~\text{EMPTY} ~ \text{EQ} ~ \ulcorner k \urcorner \\&\sim_{\mathrm{s}} \text{EMPTY}~ \text{NONE} ~ (\dots) \\& \sim_{\mathrm{s}} \text{NONE}.\end{align*}

Induction Step \((\delta = (k_0,v_0) \cdot t)\). Assume, as the inductive hypothesis, that

\[(\text{LOOKUP}~\ulcorner t \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner) \sim_{\mathrm{s}} \ulcorner \mathrm{lookup}(t, k) \urcorner.\]

Case 1 \((k=k_0)\). By definition, \(\mathrm{lookup}((k_0,v_0) \cdot t, k) = \mathrm{some}(v_0)\), so

\[\ulcorner \mathrm{lookup}((k_0,v_0) \cdot t) \urcorner = \ulcorner \mathrm{some}(v_0) \urcorner = \text{SOME} ~ \ulcorner v_0 \urcorner.\]

Since \(\ulcorner (k_0,v_0) \cdot t \urcorner = \text{CONS}~\ulcorner (k_0,v_0) \urcorner ~ \ulcorner t \urcorner\), it follows that

\begin{align*}\text{LOOKUP}~\ulcorner \delta \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner &= \text{LOOKUP} ~ (\text{CONS}~\ulcorner (k_0,v_0) \urcorner ~ \ulcorner t \urcorner)~ \text{EQ} ~ \ulcorner k \urcorner \\&\sim_{\mathrm{s}} (\text{CONS}~\ulcorner (k_0,v_0) \urcorner ~ \ulcorner t \urcorner)~ \text{NONE} ~ (\lambda h . \lambda t . h ~ (\lambda k' . \lambda v . \text{IF} ~ (\text{EQ} ~ \ulcorner k \urcorner ~ k') ~ (\text{SOME} ~ v) ~ (\text{LOOKUP}~ t ~ \text{EQ} ~ \ulcorner k \urcorner)) \\&\sim_{\mathrm{s}} (\text{PAIR} ~ \ulcorner k_0 \urcorner ~ \ulcorner v \urcorner) ~ (\lambda k' . \lambda v . \text{IF} ~ (\text{EQ} ~ \ulcorner k \urcorner ~ k') ~ (\text{SOME} ~ v) ~ (\text{LOOKUP}~ \ulcorner t \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner)) \\&\sim_{\mathrm{s}} \text{IF} ~ (\text{EQ} ~ \ulcorner k \urcorner ~ \ulcorner k_0 \urcorner) ~ (\text{SOME} ~ \ulcorner v_0 \urcorner) ~ (\text{LOOKUP}~ \ulcorner t \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner) \\&\sim_{\mathrm{s}} \text{IF} ~ \text{TRUE} ~ (\text{SOME} ~ \ulcorner v_0 \urcorner) ~ (\text{LOOKUP}~ \ulcorner t \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner) \\&\sim_{\mathrm{s}} \text{SOME} ~ \ulcorner v_0 \urcorner.\end{align*}

Case 2 \((k \ne k_0)\). By definition, \(\mathrm{lookup}((k_0, v_0) \cdot t, k) = \mathrm{lookup}(t, k)\), so

\[\ulcorner \mathrm{lookup}((k_0,v_0) \cdot t) \urcorner = \ulcorner \mathrm{lookup}(t, k) \urcorner.\]

Since \(\ulcorner (k_0,v_0) \cdot t \urcorner = \text{CONS}~\ulcorner (k_0,v_0) \urcorner ~ \ulcorner t \urcorner\), it follows that

\begin{align*}\text{LOOKUP}~\ulcorner \delta \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner &= \text{LOOKUP} ~ (\text{CONS}~\ulcorner (k_0,v_0) \urcorner ~ \ulcorner t \urcorner)~ \text{EQ} ~ \ulcorner k \urcorner \\&\sim_{\mathrm{s}} (\text{CONS}~\ulcorner (k_0,v_0) \urcorner ~ \ulcorner t \urcorner)~ \text{NONE} ~ (\lambda h . \lambda t . h ~ (\lambda k' . \lambda v . \text{IF} ~ (\text{EQ} ~ \ulcorner k \urcorner ~ k') ~ (\text{SOME} ~ v) ~ (\text{LOOKUP}~ t ~ \text{EQ} ~ \ulcorner k \urcorner)) \\&\sim_{\mathrm{s}} (\text{PAIR} ~ \ulcorner k_0 \urcorner ~ \ulcorner v \urcorner) ~ (\lambda k' . \lambda v . \text{IF} ~ (\text{EQ} ~ \ulcorner k \urcorner ~ k') ~ (\text{SOME} ~ v) ~ (\text{LOOKUP}~ \ulcorner t \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner)) \\&\sim_{\mathrm{s}} \text{IF} ~ (\text{EQ} ~ \ulcorner k \urcorner ~ \ulcorner k_0 \urcorner) ~ (\text{SOME} ~ \ulcorner v_0 \urcorner) ~ (\text{LOOKUP}~ \ulcorner t \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner) \\&\sim_{\mathrm{s}} \text{IF} ~ \text{FALSE} ~ (\text{SOME} ~ \ulcorner v_0 \urcorner) ~ (\text{LOOKUP}~ \ulcorner t \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner) \\&\sim_{\mathrm{s}} \text{LOOKUP}~ \ulcorner t \urcorner ~ \text{EQ} ~ \ulcorner k \urcorner.\end{align*}

\(\square\)

Lemma (Move Left). For any state \(q' \in Q\), symbol \(s' \in \Gamma\), and symbol lists \(l,r \in \Gamma^*\),

\[\ulcorner \mathrm{move\_left}(q', s', l, r) \urcorner \sim_{\mathrm{s}} \text{MOVE-LEFT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner.\]

Proof. We proceed by case analysis.

Case 1 \((l = \varepsilon)\). By definition, \(\mathrm{move\_left}(q', s', \varepsilon, r) = (q', \varepsilon, b \cdot s' \cdot r)\), so

\[\ulcorner \mathrm{move\_left}(q', s', \varepsilon, r) \urcorner = \ulcorner (q', \varepsilon, b \cdot s' \cdot r) \urcorner = \text{TRIPLE} ~ \ulcorner q' \urcorner ~ \text{EMPTY} ~ (\text{CONS} ~ \text{BLANK} ~ (\text{CONS} ~ \ulcorner s' \urcorner ~ \ulcorner r \urcorner)).\]

Observe that

\begin{align*}\text{MOVE-LEFT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \text{EMPTY} ~ \ulcorner r \urcorner &\sim_{\mathrm{s}} \text{EMPTY} ~ (\text{TRIPLE} ~ \ulcorner q' \urcorner ~ \text{EMPTY} ~ (\text{CONS} ~ \text{BLANK} ~ (\text{CONS} ~ \ulcorner s' \urcorner ~ \ulcorner r \urcorner))) ~ (\lambda h. \lambda t . \text{TRIPLE} ~ \ulcorner q' \urcorner ~ t ~ (\text{CONS} ~ h ~ (\text{CONS} ~ \ulcorner s' \urcorner ~ \ulcorner r \urcorner))) \\&\sim_{\mathrm{s}} \text{TRIPLE} ~ \ulcorner q' \urcorner ~ \text{EMPTY} ~ (\text{CONS} ~ \text{BLANK} ~ (\text{CONS} ~ \ulcorner s' \urcorner ~ \ulcorner r \urcorner))\end{align*}

Case 2 \((l = h \cdot t)\). By definition, \(\mathrm{move\_left}(q', s', h \cdot t, r) = (q', t, h \cdot s' \cdot r)\), so

\[\ulcorner \mathrm{move\_left}(q', s', h \cdot t, r) \urcorner = \ulcorner (q', t, h \cdot s' \cdot r) \urcorner = \text{TRIPLE} ~ \ulcorner q' \urcorner ~ \ulcorner t \urcorner ~ (\text{CONS} ~ \ulcorner h \urcorner ~ (\text{CONS} ~ \ulcorner s' \urcorner ~ \ulcorner r \urcorner)).\]

Observe that

\begin{align*}\text{MOVE-LEFT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ (\text{CONS} ~ \ulcorner h \urcorner ~ \ulcorner t \urcorner) ~ \ulcorner r \urcorner &\sim_{\mathrm{s}} (\text{CONS} ~ \ulcorner h \urcorner ~ \ulcorner t \urcorner) ~ (\text{TRIPLE} ~ \ulcorner q' \urcorner ~ \text{EMPTY} ~ (\text{CONS} ~ \text{BLANK} ~ (\text{CONS} ~ \ulcorner s' \urcorner ~ \ulcorner r \urcorner))) ~ (\lambda h. \lambda t . \text{TRIPLE} ~ \ulcorner q' \urcorner ~ t ~ (\text{CONS} ~ h ~ (\text{CONS} ~ \ulcorner s' \urcorner ~ \ulcorner r \urcorner))) \\&\sim_{\mathrm{s}} \text{TRIPLE} ~ \ulcorner q' \urcorner ~ \ulcorner t \urcorner ~ (\text{CONS} ~ \ulcorner h \urcorner ~ (\text{CONS} ~ \ulcorner s' \urcorner ~ \ulcorner r \urcorner).\end{align*}

\(\square\)

Lemma (Move Right). For any state \(q' \in Q\), symbol \(s' \in \Gamma\), and symbol lists \(l,r \in \Gamma^*\),

\[\ulcorner \mathrm{move\_right} (q', s', l, r) \urcorner \sim_{\mathrm{s}} ~ \text{MOVE-RIGHT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner.\]

Proof. By definition, \(\ulcorner \mathrm{move\_right} (q', s', l, r) \urcorner = (q', s' \cdot l, r)\), so

\[\ulcorner \mathrm{move\_right} (q', s', l, r) \urcorner = \ulcorner (q', s' \cdot l, r) \urcorner = \text{TRIPLE} ~ \ulcorner q' \urcorner ~ (\text{CONS} ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner) ~ \ulcorner r \ulcorner.\]

Observe that

\begin{align*}\text{MOVE-RIGHT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner &\sim_{\mathrm{s}} \text{TRIPLE} ~ \ulcorner q' \urcorner ~ (\text{CONS} ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner) ~ \ulcorner r \urcorner.\end{align*}

\(\square\)

Lemma (Apply Transition). For any transition \(u \in Q \times \Gamma \times D\) and symbol lists \(l,r \in \Gamma^*\),

\[\ulcorner \mathrm{apply\_trans}(u, l, r) \urcorner \sim_{\mathrm{s}} \text{APPLY-TRANS} ~ \ulcorner u \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner.\]

Proof. We proceed by case analysis.

Case 1 \((u = (q', s', L))\). By definition, \(\mathrm{apply\_trans}((q', s', L), l, r) = \mathrm{move\_left}(q', s', l, r)\). By the Move Left Lemma, it follows that

\[\ulcorner \mathrm{apply\_trans}((q', s', L), l, r) \urcorner \sim_{\mathrm{s}} \text{MOVE-LEFT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner.\]

Observe the following:

\begin{align*}\text{APPLY-TRANS} ~ \ulcorner u \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner &=\text{APPLY-TRANS} ~ (\text{TRIPLE} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \text{LEFT}) ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner \\&\sim_{\mathrm{s}} (\text{TRIPLE} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \text{LEFT}) ~ (\lambda q ' . \lambda s' . \lambda d . d ~ (\text{MOVE-LEFT} ~ q' ~ s' ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner) ~ (\text{MOVE-RIGHT} ~ q' ~ s' ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner)) \\&\sim_{\mathrm{s}} \text{LEFT} ~ (\text{MOVE-LEFT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner) ~ (\text{MOVE-RIGHT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner) \\&\sim_{\mathrm{s}} \text{MOVE-LEFT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner.\end{align*}

Case 2 \((u = (q', s', R))\). By definition, \(\mathrm{apply\_trans}((q', s', R), l, r) = \mathrm{move\_right}(q', s', l, r)\). By the Move Right Lemma, it follows that

\[\ulcorner \mathrm{apply\_trans}((q', s', R), l, r) \urcorner \sim_{\mathrm{s}} \text{MOVE-RIGHT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner.\]

Observe the following:

\begin{align*}\text{APPLY-TRANS} ~ \ulcorner u \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner &=\text{APPLY-TRANS} ~ (\text{TRIPLE} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \text{RIGHT}) ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner \\&\sim_{\mathrm{s}} (\text{TRIPLE} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \text{RIGHT}) ~ (\lambda q ' . \lambda s' . \lambda d . d ~ (\text{MOVE-LEFT} ~ q' ~ s' ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner) ~ (\text{MOVE-RIGHT} ~ q' ~ s' ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner)) \\&\sim_{\mathrm{s}} \text{RIGHT} ~ (\text{MOVE-LEFT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner) ~ (\text{MOVE-RIGHT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner) \\&\sim_{\mathrm{s}} \text{MOVE-RIGHT} ~ \ulcorner q' \urcorner ~ \ulcorner s' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner.\end{align*}

\(\square\)

Lemma (Evaluate Transition). For any association list \(\delta \in (Q \times \Gamma) \rightharpoonup (Q \times S \times D)\) of transition rules, state \(q \in Q\), symbol \(s \in \Gamma\), and symbols lists \(l,r \in \Gamma^*\),

\[\ulcorner \mathrm{eval\_trans}(\delta, q, s, l , r) \urcorner \sim_{\mathrm{s}} \text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner.\]

Proof. We proceed by case analysis.

Case 1 \((\mathrm{lookup}(\delta, (q, s)) = \mathrm{none})\). By definition, \(\mathrm{eval\_trans}(\delta, q, s, l, r) = \mathrm{none}\).

Observe that

\begin{align*}\text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner &\sim_{\mathrm{s}} \text{LOOKUP} ~ \ulcorner \delta \urcorner ~ \text{EQ-KEY} ~ (\text{PAIR} ~ \ulcorner q \urcorner ~ \ulcorner s \urcorner) ) ~ \text{NONE} ~ (\lambda c' . \text{APPLY-TRANS} ~ c' ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner) \\&\sim_{\mathrm{s}} \text{NONE} ~ \text{NONE} ~ (\lambda c' . \text{APPLY-TRANS} ~ c' ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner) \\&\sim_{\mathrm{s}} \text{NONE}.\end{align*}

Case 2 \((\mathrm{lookup}(\delta, (q, s)) = \mathrm{some}(c'))\). By definition, \(\mathrm{eval\_trans}(\delta, q, s, l, r) = \mathrm{apply\_trans}(c', l, r)\). By the Apply Transition Lemma, it follows that

\[\ulcorner \mathrm{eval\_trans}(\delta, q, s, l, r) \urcorner \sim_{\mathrm{s}} \text{APPLY-TRANS} ~ \ulcorner c' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner.\]

By the Lookup Lemma,

\[\text{LOOKUP} ~ \ulcorner \delta \urcorner ~ \text{EQ-KEY} ~ (\text{PAIR} ~ \ulcorner q \urcorner ~ \ulcorner s \urcorner) \sim_{\mathrm{s}} \ulcorner \mathrm{lookup}(\delta, (q, s)) \urcorner = \text{SOME}~\ulcorner c' \urcorner.\]

Observe that

\begin{align*}\text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner &\sim_{\mathrm{s}} \text{LOOKUP} ~ \ulcorner \delta \urcorner ~ \text{EQ-KEY} ~ (\text{PAIR} ~ \ulcorner q \urcorner ~ \ulcorner s \urcorner) ~ \text{NONE} ~ (\lambda c' . \text{APPLY-TRANS} ~ c' ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner) \\&\sim_{\mathrm{s}} (\text{SOME} ~ \ulcorner c' \urcorner) ~ \text{NONE} ~ (\lambda c' . \text{APPLY-TRANS} ~ c' ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner) \\&\sim_{\mathrm{s}} \text{APPLY-TRANS} ~ \ulcorner c' \urcorner ~ \ulcorner l \urcorner ~ \ulcorner r \urcorner.\end{align*}

\(\square\)

Lemma (Step). For any configurations \(C, C' \in \mathcal{C}\),

\[C \xrightarrow{\delta} C' \Rightarrow (\text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner) \sim_{\mathrm{s}} \text{SOME} ~ \ulcorner C' \urcorner.\]

Proof. Suppose \(C \xrightarrow{\delta} C'\). Then, by definition, \(\mathrm{step}(\delta, C) = \mathrm{some}(C')\). We proceed by case analysis.

Case 1 \((C = (q, l, \varepsilon))\). By definition, \(\mathrm{step}(\delta, (q, l, \varepsilon)) = \mathrm{eval\_trans}(\delta, q, b, l, \varepsilon)\). By the Evaluate Transition Lemma, it follows that

\[\ulcorner \mathrm{step}(\delta, (q, l, \varepsilon)) \urcorner \sim_{\mathrm{s}} \text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ \text{BLANK} ~ \ulcorner l \urcorner ~ \text{EMPTY}.\]

Observe that

\begin{align*}\text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner (q, l, \varepsilon) \urcorner &= \text{STEP} ~ \ulcorner \delta \urcorner ~ (\text{TRIPLE} ~ \ulcorner q \urcorner ~ \ulcorner l \urcorner ~ \text{EMPTY}) \\&\sim_{\mathrm{s}} (\text{TRIPLE} ~ \ulcorner q \urcorner ~ \ulcorner l \urcorner ~ \text{EMPTY}) ~ (\lambda q . \lambda l . \lambda r . r ~ (\text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ q ~ \text{BLANK} ~ l ~ \text{EMPTY}) ~ (\lambda h . \lambda t . \text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ q ~ h ~ l ~ t)) \\&\sim_{\mathrm{s}} \text{EMPTY} ~ (\text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ \text{BLANK} ~ \ulcorner l \urcorner ~ \text{EMPTY}) ~ (\lambda h . \lambda t . \text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ h ~ \ulcorner l \urcorner ~ t) \\&\sim_{\mathrm{s}} \text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ \text{BLANK} ~ \ulcorner l \urcorner ~ \text{EMPTY} \\&\sim_{\mathrm{s}} \ulcorner \mathrm{step}(\delta, C) \urcorner \\&\sim_{\mathrm{s}} \text{SOME} ~ \ulcorner C' \urcorner.\end{align*}

Case 2 \((C = (q, l, h \cdot t))\). By definition, \(\mathrm{step}(\delta, (q, l, \varepsilon)) = \mathrm{eval\_trans}(\delta, q, h, l, t)\). By the Evaluate Transition Lemma, it follows that

\[\ulcorner \mathrm{step}(\delta, (q, l, h \cdot t)) \urcorner \sim_{\mathrm{s}} \text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ \ulcorner h \urcorner ~ \ulcorner l \urcorner ~ \ulcorner t \urcorner.\]

Observe that

\begin{align*}\text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner (q, l, h \cdot t) \urcorner &= \text{STEP} ~ \ulcorner \delta \urcorner ~ (\text{TRIPLE} ~ \ulcorner q \urcorner ~ \ulcorner l \urcorner ~ (\text{CONS} ~ \ulcorner h \urcorner ~ \ulcorner t \urcorner)) \\&\sim_{\mathrm{s}} (\text{TRIPLE} ~ \ulcorner q \urcorner ~ \ulcorner l \urcorner ~ (\text{CONS} ~ \ulcorner h \urcorner ~ \ulcorner t \urcorner)) ~ (\lambda q . \lambda l . \lambda r . r ~ (\text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ q ~ \text{BLANK} ~ l ~ \text{EMPTY}) ~ (\lambda h . \lambda t . \text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ q ~ h ~ l ~ t)) \\&\sim_{\mathrm{s}} (\text{CONS} ~ \ulcorner h \urcorner ~ \ulcorner t \urcorner) ~ (\text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ \text{BLANK} ~ \ulcorner l \urcorner ~ \text{EMPTY}) ~ (\lambda h . \lambda t . \text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ h ~ \ulcorner l \urcorner ~ t) \\&\sim_{\mathrm{s}} \text{EVAL-TRANS} ~ \ulcorner \delta \urcorner ~ \ulcorner q \urcorner ~ \ulcorner h \urcorner ~ \ulcorner l \urcorner ~ \ulcorner t \urcorner \\&\sim_{\mathrm{s}} \ulcorner \mathrm{step}(\delta, C) \urcorner \\&\sim_{\mathrm{s}} \text{SOME} ~ \ulcorner C' \urcorner.\end{align*}

\(\square\)

The Main Theorem

Up to this point, all functions that we have defined (e.g., \(\mathrm{step}\), etc.) have been total by design. Thus, the interpretation (e.g., \(\ulcorner \mathrm{step}(\delta, C) \urcorner\)) is likewise well-defined, and the definition of simulation is clear (e.g., \(\ulcorner \mathrm{step}(\delta, C) \urcorner \sim_{\mathrm{s}} \text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner\)).

However, running a Turing machine is inherently a partial operation since the machine might never halt. Therefore, we cannot use this same definition since we cannot define the interpretation of an undefined expression.

We consider two cases: convergence and divergence.

Convergence

We make an inductive definition of convergence for Turing machine configurations. The relation \(C \Downarrow_{\delta} C'\) is interpreted as asserting that a Turing machine with transition rules \(\delta\) that starts with configuration \(C\) will halt in configuration \(C'\).

Schematically, we write the following rules:

\[\frac{\mathrm{Halting}(C)}{C \Downarrow C} \quad (\text{Base}),\]

\[\frac{C \xrightarrow{\delta} C', C' \Downarrow_{\delta} C^*}{C \Downarrow_{\delta} C^*} \quad (\text{Step}),\]

where

\[\mathrm{Halting}(\delta, C) \equiv \mathrm{step}(\delta, C) = \mathrm{none}.\]

Explicitly, this defines a relation as follows. First, we define a monotone operator on the powerset lattice \(\mathcal{P}(\mathcal{C} \times \mathcal{C})\) as follows:

\[F_{\mathrm{conv}}(R) = \{(C, C) \mid \mathrm{Halting}(C)\} \cup \{(C, C^*) \mid \exists C' \in \mathcal{C}(C \xrightarrow{\delta} C' \land C' \mathrel{R} C^*)\}.\]

We define the relation \(\Downarrow_{\delta}\) as the least fixed point of this operator:

\[\Downarrow_{\delta} = \mu F_{\mathrm{conv}}.\]

This definition permits proofs by structural induction. We now proceed to prove the following result.

Theorem (Convergence). If \(C \Downarrow_{\delta} C^*\), then \(\text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \sim_{\mathrm{s}} \ulcorner C^* \urcorner\).

Proof. We prove the following proposition by structural induction:

\[P(C, C^*) \equiv C \Downarrow_{\delta} C^* \Rightarrow \text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \sim_{\mathrm{s}} \ulcorner C^* \urcorner.\]

Base Case (Base Rule). Suppose \(\mathrm{Halting}(C)\) holds and \(C \Downarrow C\). By definition, this means that \(\mathrm{step}(\delta, C) = \mathrm{none}\). By the Step Lemma, this means that \(\text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \sim_{\mathrm{s}} \text{NONE}\). Observe the following:

\begin{align*}\text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner &\sim_{\mathrm{s}} (\text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner) ~ \ulcorner C \urcorner ~ (\lambda c' . \text{RUN} ~ \ulcorner \delta \urcorner ~ c') \\& \sim_{\mathrm{s}} \text{NONE} ~ \ulcorner C \urcorner ~ (\lambda c' . \text{RUN} ~ \ulcorner \delta \urcorner ~ c') \\& \sim_{\mathrm{s}} \ulcorner C \urcorner.\end{align*}

Induction Step (Step Rule). Suppose \(C \xrightarrow{\delta} C'\), \(C' \Downarrow_{\delta} C^*\), and \(C \Downarrow_{\delta} C^*\). By the inductive hypothesis, we assume that \(C' \Downarrow_{\delta} C^*\) implies \(\text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C '\urcorner \sim_{\mathrm{s}} \ulcorner C^* \urcorner\). By the Step Lemma, \(C \xrightarrow{\delta} C'\) implies that \(\text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \sim_{\mathrm{s}} \text{SOME} ~ \ulcorner C' \urcorner\). Observe the following:

\begin{align*}\text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner &\sim_{\mathrm{s}} (\text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner) ~ \ulcorner C \urcorner ~ (\lambda c' . \text{RUN} ~ \ulcorner \delta \urcorner ~ c') \\&\sim_{\mathrm{s}} (\text{SOME} ~ \ulcorner C' \urcorner) ~ \ulcorner C \urcorner ~ (\lambda c' . \text{RUN} ~ \ulcorner \delta \urcorner ~ c') \\&\sim_{\mathrm{s}} \text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C' \urcorner \\&\sim_{\mathrm{s}} \ulcorner C^* \urcorner.\end{align*}

\(\square\)

Divergence

We make a coinductive definition of divergence (non-halting) for Turing machines configurations. The relation \(C \Uparrow_{\delta}\) is interpreted as asserting that a Turing machine with transition rules \(\delta\) will not halt if it begins with configuration \(C\).

Schematically, we write the following rule:

\[\frac{C \xrightarrow{\delta} C', C' \Uparrow_{\delta}}{C \Uparrow_{\delta}} \quad (\text{Divergence}).\]

Explicitly, this defines a relation as follows. First, we define the following monotone operator on the powerset lattice \(\mathcal{P}(\mathcal{C})\):

\[F_{\mathrm{div}}(P) = \{C \in \mathcal{C} \mid \exists C' \in \mathcal{C}(C \xrightarrow{\delta} C' \land C' \in P)\}.\]

We define the predicate \(\Uparrow_{\delta}\) as the greatest fixed point of this operator:

\[\Uparrow_{\delta} = \nu F_{\mathrm{div}}.\]

We define the following schematic rules that characterize lambda term divergence under the call-by-name evaluation strategy:

\[\frac{M \Uparrow_{\mathrm{n}}}{(MN) \Uparrow_{\mathrm{n}}} \quad (\text{App Left}),\]

\[\frac{M \Downarrow_{\mathrm{n}} (\lambda x . M'), M'[N/x] \Uparrow_{\mathrm{n}}}{(MN) \Uparrow_{\mathrm{n}}} \quad (\text{App Body}).\]

Explicitly, this defines a predicate as follows. First, we define the following monotone operator on the powerset lattice \(\mathcal{P}(\Lambda(\emptyset))\):

\begin{align*}F_{\mathrm{div,n}}(P) &= \{(MN) \mid M \in P, N \in \Lambda(\emptyset)\} \\&\cup \{(MN) \mid \exists x \in \mathcal{V} \exists M' \in \Lambda(\{x\}) (M \Downarrow_{\mathrm{n}} (\lambda x . M') \land M'[N/x] \in P)\}.\end{align*}

We define the following schematic rules that characterize lambda term divergence under the call-by-value evaluation strategy:

\[\frac{M \Uparrow_{\mathrm{v}}}{(MN) \Uparrow_{\mathrm{v}}} \quad (\text{App Left}),\]

\[\frac{M \Downarrow_{\mathrm{v}} (\lambda x . M'), N \Uparrow_{\mathrm{v}}}{(MN) \Uparrow_{\mathrm{v}}} \quad (\text{App Right}),\]

\[\frac{M \Downarrow_{\mathrm{v}} (\lambda x . M'), M'[N/x] \Uparrow_{\mathrm{v}}}{(MN) \Uparrow_{\mathrm{n}}} \quad (\text{App Body}).\]

Note that the convergence of \(M\) is required in the App Right rule so that there is at most one applicable rule in the case that both \(M\) and \(N\) diverge.

Explicitly, this defines a predicate as follows. First, we define the following monotone operator on the powerset lattice \(\mathcal{P}(\Lambda(\emptyset))\):

\begin{align*}F_{\mathrm{div,v}}(P) &= \{(MN) \mid M \in P, N \in \Lambda(\emptyset)\} \\&\cup \{(MN) \mid (\exists x \in \mathcal{V} \exists M' \in \Lambda(\{x\}) M \Downarrow_{\mathrm{v}} (\lambda x . M')) \land N \in P\} \\&\cup \{(MN)\mid \exists x \in \mathcal{V} \exists M' \in \Lambda(\{x\}) (M \Downarrow_{\mathrm{v}} (\lambda x . M') \land M'[N/x] \in P)\}.\end{align*}

We now proceed to prove the following result by coinduction.

Theorem (Divergence). If \(C \Uparrow_{\delta}\), then \(\text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \Uparrow_{\mathrm{s}}\).

Proof. We proceed to prove the following proposition by coinduction:

\[C \Uparrow_{\delta} ~ \Rightarrow ~ \text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \Uparrow_{\mathrm{s}}.\]

We define the following set:

\[P = \{M \in \Lambda(\emptyset) \mid \exists C \in \mathcal{C}(M \sim_{\mathrm{s}} \text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \land C \Uparrow_{\delta})\}.\]

Our goal is to show that \(P\) is a post-fixed point of \(F_{\mathrm{div,s}}(P)\) up to bisimilarity, i.e., that \(P \subseteq F_{\mathrm{div,s}}(\mathrm{cl}_{\mathrm{s}}(P))\), where \(\mathrm{cl}_{\mathrm{s}}\) is the closure operator defined as follows:

\[\mathrm{cl}_{\mathrm{s}}(P) = \{M \in \Lambda(\emptyset) \mid \exists N \in P(M \sim_{\mathrm{s}} N)\}.\]

The fundamental theorem of coinduction "up-to" techniques indicates that a post-fixed point up to an admissible relation (such as applicative bisimilarity) is also a strict post-fixed point, i.e., \(P \subseteq F_{\mathrm{div,s}}(P)\).

In particular, it is sufficient (for either the call-by-name or call-by-value strategies) to demonstrate for all \(Q \in \Lambda(\emptyset)\) that the App. Body rule is satisfied up-to applicative bisimilarity, namely, that

\[\exists C \in \mathcal{C}(Q \sim_{\mathrm{s}} \text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \land C \Uparrow_{\delta}) ~ \Rightarrow ~ \exists M,N \in \Lambda(\emptyset)(Q \sim_{\mathrm{s}} (MN) \land \exists x \in \mathcal{V} \exists M' \in \Lambda(\{x\}) (M \Downarrow_{\mathrm{v}} (\lambda x . M') \land \exists C' \in \mathcal{C}(M'[N/x] \sim_{\mathrm{s}} \text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C' \urcorner \land C' \Uparrow_{\delta})))).\]

Then, since \(\Uparrow_{\mathrm{s}}\) is the greatest such fixed point, it follows that \(P \subseteq \Uparrow_{\mathrm{s}}\). Thus, whenever \(C \Uparrow_{\delta}\),

\[\text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \in P \subseteq \Uparrow_{\mathrm{s}},\]

i.e., \(\text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \Uparrow_{\mathrm{s}}\).

Therefore, consider any closed term \(Q \in \Lambda(\emptyset)\) such that \(Q \sim_{\mathrm{s}} \text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner\) for some configuration \(C \in \mathcal{C}\) such that \(C \Downarrow_{\delta}\). By definition, this means that there exists a configuration \(C' \in \mathcal{C}\) such that \(C \xrightarrow{\delta} C'\) and \(C' \Uparrow_{\delta}\). By the Step Lemma, it follows that \(\text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \sim_{\mathrm{s}} \text{SOME} ~ \ulcorner C' \urcorner\).

Observe the following:

\begin{align*}Q &\sim_{\mathrm{s}} \text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner \\&\sim_{\mathrm{s}} (\text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner) ~ \ulcorner C \urcorner ~ (\lambda c' . \text{RUN} ~ \ulcorner \delta \urcorner ~ c') \\&\sim_{\mathrm{s}} (\text{SOME} ~ \ulcorner C' \urcorner) ~ \ulcorner C \urcorner ~ (\lambda c' . \text{RUN} ~ \ulcorner \delta \urcorner ~ c') \\&\sim_{\mathrm{s}} \text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C' \urcorner.\end{align*}

If we instantiate

• \(M = \text{RUN} ~ \ulcorner \delta \urcorner\),
• \(N = \ulcorner C \urcorner\),
• \(M' = (\text{STEP} ~ \ulcorner \delta \urcorner ~ c) ~ c ~ (\lambda c' . r ~ \ulcorner \delta \urcorner ~ c')\),
• \(x = c\),

then

• \(M \Downarrow_{\mathrm{s}} \lambda c . (\text{STEP} ~ \ulcorner \delta \urcorner ~ c) ~ c ~ (\lambda c' . r ~ \ulcorner \delta \urcorner ~ c')\) for an appropriate recursor term \(r\) inserted by the respective fixed-point combinator,
• \(M'[N/x] = (\text{STEP} ~ \ulcorner \delta \urcorner ~ \ulcorner C \urcorner) ~ \ulcorner C \urcorner ~ (\lambda c' . r ~ \ulcorner \delta \urcorner ~ c')\),
• \(M'[N/x] \sim_{\mathrm{s}} \text{RUN} ~ \ulcorner \delta \urcorner ~ \ulcorner C'\).

Thus, the App. Body Rule is satisfied up to bisimilarity. This completes the proof. \(\square\)

Summary

Thus, we have shown that, if a Turing machine initialized with a given configuration \(C\) halts in configuration \(C'\), then the combinator \(\text{RUN} ~ \ulcorner \delta \urcorner\) likewise, when applied to configuration encoding \(\ulcorner C \urcorner\), converges to configuration encoding \(\ulcorner C' \urcorner\). We have additionally shown that, if a Turing machine initialized with a given configuration \(C\) does not halt, then the combinator \(\text{RUN} ~ \ulcorner \delta \urcorner\) likewise, when applied to configuration encoding \(\ulcorner C \urcorner\), diverges.

Thus, the combinator \(\text{RUN} ~ \ulcorner \delta \urcorner\) faithfully simulates the respective Turing machine.

This means that anything computable by some Turing machine is likewise computable by some lambda term. Indeed, it is also possible to establish the converse, so that the two formalisms are equivalent. However, the goal of this post is only to establish that the lambda calculus can faithfully simulate any Turing machine.