The auxiliary function (epsilon p) returns a stream for which p holds, if one exists, and an arbitrary stream otherwise. The auxiliary function (prefix b p) is like (epsilon p), but only considers streams beginning with b.
exists :: ([Bool] -> Bool) -> Bool
epsilon :: ([Bool] -> Bool) -> [Bool]
prefix :: Bool -> ([Bool] -> Bool) -> [Bool]
exists p = p (epsilon p)
epsilon p = prefix (p (prefix True p)) p
prefix b p = b : epsilon (\x -> p (b : x))
Here are some test predicates and a testing function.
pos i x = not (x !! i)
run i x = and (map not (take i x))
alt i x = take i x == take i (cycle [False,True])
fal i x = not (take i x == take i x)
test f i = (exists (f i), take (i+1) (epsilon (f i)))
And here are some test runs.
*Main> test pos 5
(True,[True,True,True,True,True,False,True,True])
*Main> test run 5
(True,[False,False,False,False,False,True,True,True])
*Main> test alt 5
(True,[False,True,False,True,False,True,True,True])
*Main> test fal 5
(False,[False,False,False,False,False,False,False,False])
6 comments:
For more on this function (and some related ones), you can read Martin Escardo's post on Andrej Bauer's blog.
Beautiful! =)
Martin Escardo just posted A Haskell monad for infinite search in finite time. I thought you'd like to know, it's relevant to this one.
Thanks to Anonymous for the links to Escardo's post on monads. It's lovely, and confirms a conjecture I had that (using the notation from Escardo's post) one can define search :: (a -> Bool) -> Maybe a in terms of find :: (a -> Bool) -> a, but not conversely.
Actually, in the papers LICS'07 & LMCS'08 cited in my blog post cited by Anonymous, I show that a non-empty set that admits an existential quantifier is necessarily searchable. Hence if there is a search operator (a -> Bool) -> Maybe a then there is also a search operator (a -> Bool) -> a. The program that transforms the existential quantifier in to the search operator can be written in Haskell, but is not efficient, and requires an implementation of the so-called Kleene-Kreisel density theorem. I use this to write an algorithm that, given a set that has a "secretly" known element, constructs explicitly some element of the set, from its existential quantifier. (That is, classical non-emptiness implies constructive non-emptiness, or inhabitedness.)
Couldn't you just do this, though?
find xs p = case search xs p of
Just x -> x
Nothing -> (\(Just x) -> x) $ search xs (const True)
Post a Comment