[Agda] Nice programming challenge

[Martin Escardo]

Dear Andrea,

Sorry for being slow to reply - I traveled back from a conference after 
I sent the message, and yesterday I had some hard deadlines to attend to.

I got two other solutions, but yours was the first (one of them gave a 
proof and a construction, but not an implementation).

Your computation is fast for the given examples, and I think it is 
correct although you didn't give a proof. (I had to remove search2 from 
your file, and ghci didn't find your function "find". Is it defined 
somewhere else?)

On 30/05/11 01:18, Andrea Vezzosi wrote:
> Here [1] is my solution, it passes the benchmarks but i haven't tried
> to prove it correct.

I think you use continuity of H : (N -> N) -> N to find a witness 
(k,f,g) of the form f = f_k = 0^k 1 0^\omega, and g = 0^\omega (that is, 
f(n) = if n == k then 1 else 0, and g(n)=0). Such a witness exists 
because the limit of f_k is g, and so H(f_k) = H(g) for some k by 
continuity of H. Then you basically do an unbounded search to find the 
k. I guess this corresponds to using Markov's principle if you were to 
derive your program from a proof (in addition to using continuity).

(Notice that your algorithm doesn't need to have the recursive call 
updating g, because your g remains the same in recursive calls (namely 
g(n)=0): it is enough to change f, and you don't even need to change f 
as it can be directly defined from k as above. I guess that this is what 
search2 was intended to do.)

Paulo's (classical) proof doesn't assume continuity, and works by 
diagonalization and countable choice (the choice is to find a left 
inverse, and the diagonalization to get a contradiction). However, to 
implement countable choice, he uses a form of bar recursion that 
requires some principle to justify termination. This principle can be 
continuity, but more generally majorizability also works (and hence his 
algorithm would work for discontinuous H, if you were able to produce any).

I think your solution is faster than Paulo's, but I didn't analyse the 
run-time behaviour of Paulo's in detail. It is easy to understand his 
proof, and how it is translated to a program using the dialectica 
interpretation, but it is much harder to understand the resulting 
program directly. A diagonalization function is passed to bar recursion 
as one of the parameters.

Cheers,
Martin

> Computing the solutions is instantaneous on my machine, even in ghci,
> including f k for h = h3.
>
> [1] https://github.com/Saizan/snippets/blob/master/Search.hs
>
> - Andrea