Subject: Nice programming challenge Newsgroups: gmane.comp.lang.agda Date: Sunday 29th May 2011 05:12:12 UTC (over 6 years ago) 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 |
|||