[Haskell-cafe] "Quantization" of computations, or step-wise termination, as an extension of Logic Monads

[Olaf Klinke]

Dear Juan,

Is the following problem of the class you are considering? 
   Given a predicate 
   p ::  (Integer -> Integer) -> Bool
   enumerate all functions f :: Integer -> Integer for which p f == True.

The search space (Integer -> Integer) can be rendered into a tree of infinite width and depth: On the first level, branch on the value of f(0), on the next level branch on the value of f(1) and so forth. 

If the above problem were tractable, then you'd have an enumeration of the real numbers. If the target is to find whether there is at least one such f, then you have proven compactness of Baire space. 
So there must be something about your problem that remained unclear to me. Care to explain? 

Regards,
Olaf

P.S.: Infinite branching trees could be modeled as
data Tree a = Tree (Integer -> Maybe (a,Tree a))
Maybe this can help bringing your algorithms closer to the literature on computable functions and recursion theory.