This is exactly right. The lazy version seems like magic, but it's really just exploiting the fact that if computing p(a) never evaluates a(n) for n >= m, then

This is exactly right. The lazy version seems like magic, but it's really just exploiting the fact that if computing p(a) never evaluates a(n) for n >= m, then p(b) = p(a) whenever the first m elements of a and b agree, so you can cut off an infinite portion of the search space without checking them all. I wrote up a Python gist (https://gist.github.com/evanpw/d69f1ccb5edd0b672e9e https://gist.github.com/evanpw/d69f1ccb5edd0b672e9e) which performs this same trick by explicitly snooping on the callbacks. It seems a lot less magical than the Haskell version. EDIT: The main "cheat" seems to be the ability to identify the predicate which returns false on every input (e.g., by seeing if returns false without evaluating its argument). The continuity argument described in the article basically says that if p is not always false, then there's some input a with a(n) = 0 for all sufficiently large n that causes p to return true, so you could just enumerate all such inputs until one returns true.