# Impossible functions

I claim to have a function `H`

that maps any integer-valued function you give it to a different integer. That is,
an injection from `Int => Int`

to `Int`

that returns a different `Int`

for every function you give it.

This is clearly impossible, since there are way more functions from integers to integers than there are integers. But I
demand proof in the form of witnesses `f: Int => Int`

, `g: Int => Int`

and `n: Int`

such that
`H(f) == H(g)`

and `f(n) != g(n)`

.

Your job is to write a function `solve`

that takes a single argument `H: (Int => Int) => Int`

and returns
`f`

, `g`

and `n`

as described above.

One approach is to put together a mathematical proof that such an injection is impossible and try to extract a program from that proof à la the Curry-Howard isomorphism.

### Proof

The proof goes like this. Suppose exists. Construct an inverse . One way to look at is as an enumeration of functions of type . So is the first function in the list, is the second function, etc., and in general . Also notice that .

This list of functions might look something like this:

… | ||||||
---|---|---|---|---|---|---|

0 | 0 | 0 | 0 | 0 | … | |

0 | 1 | 2 | 3 | 4 | … | |

1 | 5 | 2 | 1 | 3 | … | |

1 | 0 | 0 | 1 | 2 | … | |

2 | 7 | 1 | 8 | 2 | … | |

… | … | … | … | … | … | … |

Now construct a new function from the diagonal of this table as follows:

For the table above, the diagonal would look like

… | ||||||
---|---|---|---|---|---|---|

1 | 2 | 3 | 2 | 3 | … |

It’s easy to see that is not any of the s, since by construction. But is still in the domain of . Let . Now but .

So we’ve found two functions, and , that differ at , but maps them both to . This completes the proof. Now all that’s left is to translate it into code!

### Code

Let’s start with the easy parts. Here’s the function that constructs the diagonal from .

And here’s the overall solution. It mirrors the proof pretty directly, but it depends on `invert`

which we have yet to write.

Now all we need to write is `invert`

, which inverts `H`

. Hm.

### Constructing the inverse

OK this is impossible. For one, `H`

might not be an onto function. It could be something like

which only returns even numbers. So `invert(h1)`

won’t be defined on odd numbers and we won’t have a complete
table to diagonalize.

Maybe this is OK. I mean, all we need is one row from the table and a diagonal that maps to the same row. So we don’t need to construct the entire table. Maybe we can construct a partial approximation of the table by starting with a bad guess for the table, checking the diagonal to see if we found a hit, and iteratively refining the table with new functions we’ve found as we go along.

So let’s start with the simplest possible thing, a table of constant 0 functions.

… | ||||||
---|---|---|---|---|---|---|

0 | 0 | 0 | 0 | 0 | … | |

0 | 0 | 0 | 0 | 0 | … | |

0 | 0 | 0 | 0 | 0 | … | |

0 | 0 | 0 | 0 | 0 | … | |

0 | 0 | 0 | 0 | 0 | … | |

… | … | … | … | … | … | … |

Now construct the diagonal as .

… | ||||||
---|---|---|---|---|---|---|

1 | 1 | 1 | 1 | 1 | … |

Now compute and see if there’s already a “correct” entry in the table for that value. Suppose for example that , which means that should be at position 3 in the table. So we check whether our bad guess at was in fact a lucky guess. Let’s say we get . OK, it was a bad guess, so we replace with in the table and try again.

Here’s what the table looks like after the first iteration:

… | ||||||
---|---|---|---|---|---|---|

0 | 0 | 0 | 0 | 0 | … | |

0 | 0 | 0 | 0 | 0 | … | |

0 | 0 | 0 | 0 | 0 | … | |

1 | 1 | 1 | 1 | 1 | … | |

0 | 0 | 0 | 0 | 0 | … | |

… | … | … | … | … | … | … |

Now construct a new diagonal from the updated table. It looks like this:

… | ||||||
---|---|---|---|---|---|---|

1 | 1 | 1 | 2 | 1 | … |

Compute as before. Suppose we get this time. so we update the table and iterate again.

… | ||||||
---|---|---|---|---|---|---|

0 | 0 | 0 | 0 | 0 | … | |

0 | 0 | 0 | 0 | 0 | … | |

0 | 0 | 0 | 0 | 0 | … | |

1 | 1 | 1 | 1 | 1 | … | |

1 | 1 | 1 | 2 | 1 | … | |

… | … | … | … | … | … | … |

The new diagonal is

… | ||||||
---|---|---|---|---|---|---|

1 | 1 | 1 | 2 | 2 | … |

Suppose . Well we already have such that , but by construction. So we’re done. We’ve constructed enough of that the diagonal collides with a function already in the table.

Here’s the algorithm in code:

So does it work? Let’s try it out on some sample functions.

REPL time.

```
scala> val (f, g, k) = test(h1)
H(f) = 2
H(g) = 2
f(k) = 2
g(k) = 1
f: Int => Int = <function1>
g: Int => Int = <function1>
k: Int = 2
scala> val (f, g, k) = test(h2)
H(f) = 3
H(g) = 3
f(k) = 2
g(k) = 1
f: Int => Int = <function1>
g: Int => Int = <function1>
k: Int = 3
scala> val (f, g, k) = test(h3)
H(f) = 2
H(g) = 2
f(k) = 2
g(k) = 1
f: Int => Int = <function1>
g: Int => Int = <function1>
k: Int = 2
scala> val (f, g, k) = test(h4)
H(f) = 6
H(g) = 6
f(k) = 2
g(k) = 1
f: Int => Int = <function1>
g: Int => Int = <function1>
k: Int = 6
scala> val (f, g, k) = test(h5)
H(f) = 17
H(g) = 17
f(k) = 2
g(k) = 1
f: Int => Int = <function1>
g: Int => Int = <function1>
k: Int = 17
scala> val (f, g, k) = test(h6)
H(f) = 2
H(g) = 2
f(k) = 2
g(k) = 1
f: Int => Int = <function1>
g: Int => Int = <function1>
k: Int = 2
```

OK!

### Termination

A natural question to ask is whether this algorithm is guaranteed to terminate. Maybe if is constructed deviously enough, we will keep updating the table forever and never find a collision.

Actually, it’s easy to show that it does terminate provided that terminates. Updating one row in the table changes the diagonal at only one point. In particular, for all except . But since terminates, we know it can only examine a finite number of points of its argument. So we will eventually find a where and never evaluates . That means that cannot distinguish between and , and at that point the algorithm terminates.

### A simpler approach

The key insight is that only evaluates at a finite number of points. So wouldn’t it be more straightforward to scan through the integers until we find an such that does not evaluate ?

We could do something like this:

Let’s try it:

```
scala> val (f, g, k) = test2(h1)
H(f) = 0
H(g) = 0
f(k) = 1
g(k) = 0
f: Int => Int = <function1>
g: Int => Int = <function1>
k: Int = 0
scala> val (f, g, k) = test2(h4)
H(f) = 5
H(g) = 5
f(k) = 1
g(k) = 0
f: Int => Int = <function1>
g: Int => Int = <function1>
k: Int = 0
scala> val (f, g, k) = test2(h6)
H(f) = 0
H(g) = 0
f(k) = 1
g(k) = 0
f: Int => Int = <function1>
g: Int => Int = <function1>
k: Int = 2
```

It works! And it’s guaranteed to terminate for the same reason.

### Bar induction

It seems like we didn’t extract a program directly from a proof when we found an approximation of . But actually, the solution is a direct translation of a proof by Paulo Oliva that uses a proof technique called bar induction. My admittedly poor understanding of bar induction is that it is simply structural induction on infinitely branching (but not necessarily infinitely deep) trees with values at the leaves, except that the trees are disguised as functions of type . The way to think about this is that the argument tells you which branch to take at each level of the tree. Eventually you will get to a leaf, and the value in the leaf is the result of the function. So you can see an isomorphism between infinitely branching trees and functions of this type.

So anyway, you use bar induction to prove that if such a tree has a finite depth, it must have 2 leaves with the same value. Then you extract a bar recursive program from this proof, and that gives you the first solution I presented above.

Both the proof and the program are due to Paulo Oliva. Any errors or misinterpretations are mine.

This started for me when I came across this tantalizing programming challenge
put forth by Martín Escardó. I initially came up with a solution that looked a lot like `solve2`

— actually, I constructed
a function `f`

that “cheats” by recording in a mutable set what points `H`

evalutes it at, then picked a value
not in that set as my `k`

— and sent it to Martín. He said it appeared to be correct, but Paulo’s solution (the one he had in mind)
was somewhat different.

Intrigued, I eventually found this presentation by Paulo Oliva and this paper on bar recursion by Martín Escardó and Paulo Oliva. The paper gave me some background understanding of the relevant topics and terminology, but most of it I cannot pretend to begin to understand. But it’s been fun trying!

All of the code in this post is available in this gist.

blog comments powered by Disqus