I strongly recommend Escardó′s Seemingly impossible functional programs, which constructs a function search : ((Nat -> Bool) -> Bool) -> (Nat -> Bool) which, given a predicate on infinite bitstrings, finds an infinite bitstring satisfying the predicate if one exists. (In other words, if p : (Nat -> Bool) -> Bool and any bitstring at all satisfies p, then p (search p) == True
(Here I’m intending Nat to be the type of natural numbers, of course) .
I strongly recommend Escardó′s Seemingly impossible functional programs, which constructs a function
search : ((Nat -> Bool) -> Bool) -> (Nat -> Bool)which, given a predicate on infinite bitstrings, finds an infinite bitstring satisfying the predicate if one exists. (In other words, ifp : (Nat -> Bool) -> Booland any bitstring at all satisfiesp, thenp (search p) == True(Here I’m intending
Natto be the type of natural numbers, of course) .