The halting problem states, informally, that there is no algorithm to
determine whether an *arbitrary* program (when provided with some
given input) will halt. Even for specific programs this can lead to
interesting unsolved questions. A well-known example is the Collatz
conjecture, which states, that the following function halts for all
inputs:

```
collatz :: Natural -> Bool
1 = True
collatz | even n = collatz (n `div` 2)
collatz n | otherwise = collatz (3 * n + 1) collatz n
```

```
> all id (fmap collatz [1..10000])
True
```

Typically, the halting problem is formalised by first picking some
specific theory of computation, and then demonstrating, within that
theory, that no such halting algorithm can be written. Unfortunately,
the theory typically chosen is that of Turing machines. These are hard
to formalise (Wikipedia
informs me, for example, that “a (one-tape) Turing machine can be
formally defined as a [certain] 7-tuple”!) and don’t offer a
particularly good foundation for programming. A Turing machine, after
all, is *not* (and was never meant to be) a programming
language!

Instead let’s take an alternative approach: we will use the lambda calculus as the basis for computation. The lambda calculus is both a programming language in itself and the foundation of all other functional languages. As a testament to this idea, we will first prove halting for the lambda calculus and then see how the same argument looks when transplanted to Haskell. Finally, in part two of this post, we will formalise the argument in Agda and fill in most of the lingering details we brush aside here.

In the setting of the lambda calculus, a precise statement of halting can be given thusly:

**Theorem (\(\lambda\)-Halting)**: There does not
exist a \(\lambda\)-term \(\def\h{\mathbf{HALT}} \def\s{\text{ }}
\def\L{\mathrm{L}} \def\l{\mathrm{l}} \def\true{\mathbf{true}}
\def\false{\mathbf{false}} \h\) such that for any given lambda
term \(\L\), \(\h \text{ } \L\) evaluates to \(\true\) when \(\L\) terminates and \(\false\) otherwise.

Here, by termination, we mean what is otherwise called normalization.
A term is normalizing if there exists a finite sequence of \(\beta\)-reductions (performed anywhere
within the term) after which, the term contains no further \(\beta\)-redexes. A well-known result in the
study of the lambda calculus says that a term normalizes if and only if
it normalizes when we always pick the leftmost, outermost redex. This
gives us an algorithm that will *confirm* that a given term does
indeed terminate but will never disconfirm whether a term loops
indefinitely. In other words, there is a semi-decision
procedure for halting.

Let’s turn to the proof of \(\lambda\)-Halting. The arguments here are adapted from the introduction to the paper Computational Foundations of Basic Recursive Function Theory by Constable and Smith. Essential to this argument is that lambda calculus allows us to encode arbitrary recursive functions. Such recursion is performed by fixed-point combinators. We will make use of perhaps the most well-known fixed-point combinator (though any other would do for our purposes), the \(\mathrm{Y}\)-combinator, defined as follows:

\[ \def\Y{\mathrm{Y}} \def\mr#1{\mathrm{#1}} \def\la#1{\lambda \s \mathrm{#1} \s . \s } \def\ap#1#2{\mathrm{#1} \s {\mathrm{#2}}} \def\be{\mapsto_{\beta}} \Y = \la{f} \ap{(\la{x} \ap{f}{(\ap{x}{x})})}{(\la{x} \ap{f}{(\ap{x}{x})})} \]

The key property that fixed-point combinators satisfy is that for any lambda term \(\rm{g}\) we have that \((\ap{\Y}{\rm{g}})\) is a fixed point for \(\rm{g}\) in the sense that \(\ap{g}{(\ap{\Y}{g})}\) is \(\beta\)-equivalent to \(\ap{\Y}{g}\). This is straightforward to see as follows:

\[ \begin{aligned} \ap{\Y}{g} \be \; &\ap{(\la{x} \ap{g}{(\ap{x}{x})})}{(\la{x} \ap{g}{(\ap{x}{x})})} \\ \be \; &\ap{g}({\ap{(\la{x} \ap{g}{(\ap{x}{x})})}{(\la{x} \ap{g}{(\ap{x}{x})})}}) \\ \equiv_\beta \; &\ap{g}{(\ap{Y}{g})} \end{aligned}\]

Fixed point combinators allow us to write recursive functions. For example, supposing we have already encoded Booleans and Natural numbers as certain lambda terms. In a language which allowed recursive definitions we could write: \[ \mathrm{fact} (n) = \mathrm{if}\; n = 0\; \mathrm{then} \; 1 \; \mathrm{else} \; n * \;\mathrm{fact} (n - 1) \] In the lambda calculus we can’t refer to the variables we are defining in their body and so instead we make use of a fixed point combinator like so: \[ \mathrm{fact} = \Y ( \la{f} \la{n} \mathrm{if}\; n = 0\; \mathrm{then} \; 1 \; \mathrm{else} \; n * f \; (n - 1)) \]

Given this, and supposing we are given such a \(\h\) term as above, we then introduce the following terms:

\[ \begin{aligned} \bot & = \ap{Y}{(\la{x}x)} \\ \rm{p}& = {\la{f}\text{if $(\ap{\h}{f})$ then $\bot$ else true}} \\ \rm{d}& = \ap{Y}{p} \def\betaStep{\mapsto_{\beta}} \end{aligned} \]

The suggestively named \(\bot\) is an infinitely looping expression:

\[ \begin{aligned} \ap{\Y}({\la{x}x}) \be \; & \ap{(\la{x} x)}(\ap{\Y}({\la{x}x})) \\ \be \; &{\ap{Y}{(\la{x}x})} \end{aligned}\]

The term \(\rm{p}\) takes any argument \(\mathrm{f}\) and returns true if the argument doesn’t terminate and otherwise loops forever. We then define \(\mathrm{d}\) as the fixed point of this function. With ordinary recursion we would write this as follows:

\[ \rm{p} = \text{if } (\ap{\h}{\rm{p}}) \text{ then } \bot \text{ else true} \]

Intuitively, we can see the problem with this term - if it halts then it reduces to \(\bot\) and if it doesn’t halt then it reduces to \(\mathrm{true}\). In slightly more detail:

- if \(\ap{\h}{d}\) is \(\rm{true}\) then: \[ \rm{d} \equiv_\beta \ap{p}{d} :\equiv \text{if $(\ap{\h}{d})$ then $\bot$ else true} \betaStep \bot \] We therefore have that \(\rm{d}\) does not terminate and so \(\ap{\h}{d}\) must be \(\rm{false}\).
- Similarly if \(\ap{\h}{d}\) is \(\rm{false}\) then: \[ \rm{d} \equiv_\beta \ap{p}{d} :\equiv \text{if $(\ap{\h}{d})$ then $\bot$ else true} \betaStep \text{true} \] and so we get that \(\rm{d}\) terminates and so we get that \(\ap{\h}{d}\) is true.

Let us see how easily these concepts translate to a language like
Haskell. Note that in Haskell all types are *partial* (using
Constable’s terminology). This means that every type is inhabited by
some non-terminating term; this is typically denoted \(\bot\) (analogous to the term considered
above). Reformulating the theorem with this in mind we get:

**Theorem (Haskell-Halting)**: In Haskell there is no
function \(\mathbf{halt}\) with the
following behaviour:

```
halt :: Nat -> Nat
= 0
halt ⊥ = 1 halt _
```

Of course, this specification is not legal Haskell (and moreover we
are claiming that no function can have this behaviour). This formulation
may appear slightly different to the Halting problem insomuch as we are
only considering the (partial) natural numbers, but we can observe that
for any `f :: Nat -> Nat`

we can use
`halt (f n)`

to determine if `f`

halts on input
`n`

, and so this would allow us to determine on which inputs
`f`

terminates.

In order to mimic the argument above, let’s use a fixed point function similar to \(\Y\), aptly named \(\mathrm{fix}\):

```
fix :: (a -> a) -> a
= let x = f x in x fix f
```

We note that \(\rm{fix}\) satisfies precisely the same fixed-point property as \(\Y\): \[ \ap{f}{(\ap{fix}{f})} \equiv_\beta \ap{fix}{f} \]

As in the lambda calculus, \(\mathrm{fix}\) allows us to capture all forms of recursion in a single function. For instance, if we define an “openly recursive” sum function:

```
{-# LANGUAGE LambdaCase #-}
sumR :: forall n . (Num n) => ([n] -> n) -> ([n] -> n)
= \case
sumR recFn -> 0
[] :xs) -> x + recFn xs (x
```

Then taking \(\mathrm{fix}\) recovers the usual sum:

```
mySum :: forall n . (Num n) => [n] -> n
= fix sumR mySum
```

```
> mySum [1..100]
5050
```

Recasting our problem terms from earlier we get:

```
bottom :: a
= fix id
bottom
p :: Natural -> Natural
= if halt n == 0 then 1 else bottom
p n
d :: Natural
= fix p d
```

As above let us think about the value of \((\ap{h}{problem})\):

```
d
≡ fix d
≡ p dif halt d == 0 then 1 else bottom ≡
```

As before:

- If
`halt d`

is \(0\) then it is 1. - If
`halt d`

is \(1\) then it is 0.

We therefore conclude that no such function `h`

can be
written in Haskell and so we cannot tell (in general) whether a term of
type \(\mathrm{Natural}\) will diverge
or not. We should note that there is nothing special about \(\mathrm{Natural}\) in this argument and we
could have picked any type containing at least two distinct terms along
with some ability to compare terms for equality.

Thank you for reading! Hopefully this has demonstrated the unity of ideas between the lambda calculus and a functional language like Haskell and the naturality of studying computability theory from this perspective. In the next post, we will formalise this argument in Agda.

*With warmest thanks to Alixandra Prybyla and Sam Derbyshire for
their valuable feedback.*