7.11.08
A bizarre function over streams
Alex Simpson showed me this bizarre function. Given a total predicate p over streams, the function (exists p) returns true if there is some stream for which the predicate returns true. This works because if the predicate is total, then there must be some bound on the initial segment of the stream that it examines.
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.
Here are some test predicates and a testing function.
And here are some test runs.
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])
Comments:
<< Home
For more on this function (and some related ones), you can read Martin Escardo's post on Andrej Bauer's blog.
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.
# posted by 
: 22/11/08 7:14 AM
: 22/11/08 7:14 AM
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
find xs p = case search xs p of
Just x -> x
Nothing -> (\(Just x) -> x) $ search xs (const True)
# posted by : 28/2/11 3:57 PM
: 28/2/11 3:57 PM << Home
