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 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`

.

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

- first entry Boolean saying whether parse is successful
- second entry
- if parse is successful, a pair with result and unconsumed output.
- if parse fails, say
`Null`

(it can be anything).

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.

`HackyLang`

We have written in code and illustrated in lectures

- A parsers (in Idris),
`ExpressionParser`

, for a language smaller but more complex that`HackyLang`

(since we needed to flat-map to deal with context dependence of parsing). - An interpreter for expressions in
`HackyLang`

built by recursive application of*simplification*(**warning:**simplification may actually complicate). - A program in
`HackyLang`

that can compute the factorial function. - Made enhancements to
`HackyLang`

to include pairs and a notion of running programs. - Made a program to sum lists of natural numbers using
`HackyLang`

.

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

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

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

- The language has
*definitions*and*expressions*, with a collection of definitions forming a*context*. Expressions include literals, strings, $\lambda$-definitions, function applications etc. - We can
*simplify*an expression in a context. Iterated simplification may or may not terminate in a literal. - We take a program to be a context and a main expression. Running this on an input expression (which we take to be a string) means applying the function to the input and repeatedly simplifying. By definition, we say running the program terminates on the input if repeated simplification gives a literal string. We view this as a
*partially defined*`run`

function`run: Program -> String -> String`

- We can
`quote`

programs, i.e. represent them by strings. - We have a (in general partially defined)
*interpreter*function`eval : String -> String -> String`

so that if the program`P`

when run with input`s`

terminates with output`t`

, then`eval (quote P) s = t`

(by this we mean the lhs is defined and equals the rhs). We say`eval`

is a*total interpreter*if it is defined in all cases, though there is no restriction on what it outputs except for programs and terminating input.

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

**Proof:**

- Assume that we have such a total interpreter
`eval`

. - Define
`evil: String -> String`

given by`evil s = (eval s s) + " contrariwise"`

- Let
`evilProg`

be the program giving this definition. - Note that as
`eval`

is total,`evilProg`

also terminates with all inputs, i.e.`runEvilprog s`

is always defined - Thus for any string
`s`

,`eval (quote evil) s = evil s`

- Observe that
`evil (quote evil) = (eval (quote Evil) (quote Evil)) + " contrariwise" = (evil (quote evil)) + " contrariwise"`

- The above is absurd, giving a contradiction to the existence of a total interpreter.

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)$`

.

**Proof:**

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.