[Agda] Nice programming challenge

[Martin Escardo]

This message is not really about Agda, but I hope I'll be excused, as
it is related to getting programs from proofs. Moreover, this list
includes a fair amount of the cleverest functional programmers in the
world (feel free to forward this challenge to further lists with the
same property).

The proposal and a solution of the challenge has been given by Paulo
Oliva -- I just want to advertise it, without giving you his solution.

Programming challenge
---------------------

Using your favourite (higher-type) programming language, write an
*efficient* (and of course correct) program that given a function

     H : (N -> N) -> N,

where N is the type natural numbers (or the closest you can find in
your language), finds two functions

     f, g : N -> N

and a natural number k such that

     Hf = Hg but fk =/= gk.

This says, in a positive way, that there is no injection
H : (N -> N) -> N.

End of formulation of the challenge, followed by discussion.
-----------------------------------------------------------

This morning, at MFPS'XXVII, Paulo Oliva extracted such an algorithm
from a classical proof, using Godel's dialectica interpretation. We
quickly wrote it in Haskell, and it turns out to be very fast (and
short). I'll show you some examples that Paulo didn't have the
pleasure to see (yet) as he had to catch his plane. Before showing you
the examples, I make two remarks.

   1. I don't think this theorem has a constructive proof.

   2. I don't think a (clever) programmer will easily find a more
      efficient solution without the aid of proof-theoretic techniques
      -- but then you will of course prove me wrong, and I am looking
      forward to that.

Here are some benchmarks (contributed by Ulrich Berger and Monika
Seisenberger).

Benchmarks (written in Haskell)
----------

h1 :: (N -> N) -> N
h1 f = 2^(f (f 0)) + 3^(f (f ( f 1))) + 5^(f 2) + 7^(f 3)

rec f x 0 = x
rec f x (n+1) = f(rec f x n)

h2 :: (N -> N) -> N
h2 f = rec ((+1).f) (f 0) (f 1)

pair :: N -> N -> N
pair x y = let z = x + y in (z * (z + 1)) `div` 2 + y

hh :: N -> (N -> N) -> N
hh 0 f = 0
hh (n+1) f = pair (f n) (hh n f)

h3 :: (N -> N) -> N
h3 = hh 8

End of bench marks (produce your own too)
------------------

These all run under a second with Paulo's solution, for the
computation of k, including h3. However, the computation of f k takes
a long time for h = h3 (how can that be?).

I am looking forward to comments and answers to this problem.

Best wishes,
Martin