Graham Hutton wrote: > Readers of this list may enjoy the following note by > Martin Escardo, which shows how to write a number of > "seemingly impossible Haskell programs" that perform > exhaustive searches over spaces of infinite size, by > exploiting some ideas from topology: > > > http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/#more-69
Very nice! The note shows that you can actually compute (forall p) where p is a *total* predicate over streams of Bool (a.k.a. infinite lazy lists). Indeed, (writing [] for streams) forall :: ([Bool] -> Bool) -> Bool seems impossible to compute. Here's what I understood: (which might be wrong, of course!) This apparent magic relies on the fact that any total predicate over (total) bool streams, i.e. p :: [Bool] -> Bool can only inspect a _finite_ prefix of the input list. More importantly, the length of the inspected prefix has an upper bound which depends _only_ on p and not on the actual input of p. In rough formulas forall p, exists n:nat, forall l:[Bool], forall l':[Bool], p l == p (take n l ++ l') So, with some nice laziness tricks, you can actually check p over "all" the infinite [Bool] space, using only finite time. Zun. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
