[Agda] Nice programming challenge

[Andrea Vezzosi]

On Wed, Jun 1, 2011 at 12:43 PM, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>[...]
> 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?)

Oh, sorry, I forgot to import Data.Maybe and Data.List when i added
search2 to that file.

> 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).

Yes, that was sort of my intuition behind it, I should really learn
how to deal with these things formally.
By the way, is there a standard generalization of the continuity axiom
to more structures than streams, and that doesn't require the codomain
to be discrete?

-- Andrea