Languages and Limits of Mathematics and Computation

Date: 26 March 2019

In this note we discuss what we have illustrated that we can do - parsing and interpretation, and show how this leads to results about what is impossible.

The Setup

Functional languges

The languages we use are functional languages, i.e., langauges where functions are first-class objects, so we can have functions of functions and so on, and where definitions can be recursive. Indeed recursion is the only form of looping we have. Idris is certainly a functional langauge, but so is the HackyLang that we have created.

Note: We have extending HackyLang adding expressions for pairs - Cons to form pairs, Left: Exp -> Exp and Right: Exp -> Exp for projections and introduced Null to deal with invalid cases. We have also added a data type Program, which is a context with a main expression (to be though of as a function), and a run function that takes a program and an input expression, applies the main expression to the input and interprets in the context.

A rich type system makes programming much easier and more pleasant, but the power of a weakly/dynamically typed functional language is no less. So while we have illustrated various things with Idris code, we can presumaby write code in HackyLang. In practice it would be best to use say Scheme (or a subset of it) to replace both Idris and HackyLang, and it is a nice project to port this part of the course to Scheme.

Parsers and their combinations

In functional langauges parsing can be very pleasant. We view parsers as functions taking an input and giving an output, or rather a ParseResult. The key point is we can define parsers by combinations of other parsers - sequencing (i.e. ++), alternatives (i.e. ||), mapping, repetition and flat-mapping. Starting with basic parsers that just match a single character based on a predicate, we can combine mutually recursively to parse a language.

We can presumably do all this in HackyLang, with ParseResult replaced by a pair with

A string can be represented by an iterated pair of characters (with characters represented by natural numbers). One can readily implement basic parsers as well as combinations. Doing this in Scheme is an enjoyable exercise.

Parsers and Intepreters for and in HackyLang

We have written in code and illustrated in lectures

We hope this is enough to make all the claimed constructions below plausible.

Theorems of Church and Turing

We sketch how diagonal arguments let us prove some fundamental results showing the limits of computation.

A postulated language

We postulate that we have a language and associated objects that satisfy the following:

The results

Theorem 1: A language as postulated above cannot have a total interpreter defined in itself.


We can bootstrap this result to prove some fundamental results. We say that a function f is computable if there is a program in our language that when run with input arguments to f outputs the result. This depends on our language, but if we can interpret another language in ours, then computability in the other language implies computability in ours.

Let halt: String -> String -> Bool be the function such that halt(q)(s) is true if and only if q = quote P and P halts when run with input s.

Theorem 2: The function halt is not computable.

Proof: Assume that halt is computable. Then we can modify the (partially defined) eval function to be a total interpreter, namely define

safeEval : String -> String -> String
safeEval q s = if (halt q s) then eval q s else "farewell and thanks for all the fish".

It follows that there is a function that grows faster than any computable function.

Theorem 3: There is a function $f: \mathbb{N} \to \mathbb{N}$ such that if $g: \mathbb{N} \to \mathbb{N}$ is a computable function, for some $n \in \mathbb{N}$ we have $f(n) > g(n)$.


For a natural number n, consider all programs P of length n and strings s with length n so that the program P with input s terminates. Given such a P and s, let t(P, s) be the number of simplification steps needed when running the program P with input s. Let f(n) be the maximum of t(P, s) over all such pairs.

We see that $f$ is as claimed. Suppose not. Then there is a computable function $g: \mathbb{N} \to \mathbb{N}$ such that $f(n)\leq g(n)\ \forall n\in\mathbb{N}$. Then it is easy to define a computable function halt using $g$, contracting Theorem 2.

All notes