Thanks Olaf for a very good question. You made me scared for a minute. I think the subtlety is that in order for us to evaluate the predicate p on the function, we'd have to reach the "end" of the enumeration (to have a fully defined function). In other words, the search space of the functions (Integer -> Integer) is not the search space of the intermediate nodes of the tree, but of the leaves, which are unreachable by any algorithm of course. The intermediate nodes of the tree would be the space of functions defined on a finite (yet unbounded) subset of the integers, which is countable. My search can of course only possibly stop at nodes it reaches, be it either intermediate nodes or leaves because they are actually reachable (not in this case). So I don't think I am claiming to break any cardinality constraint. Maybe to put it more in context, and going back to my original example of finding odd powers of natural numbers, I am looking for odd powers of natural numbers, *not* for natural numbers such that all their powers are odd (which would be the computational equivalent of finding functions that satisfies p). Of course you can solve this problem easily because of the semantics, but not through sheer search as we are considering here. I hope that explanation is clear and also it makes sense to you? Thanks again for the observation, though. Juan Casanova. PS: I'll take the representation style you mentioned into account. In general, the way I consider infinite branching is relatively similar, except I don't commit to particular types like Integer. Maybe it is worth mentioning that, of course, the way in which the infinite branching takes place is always computable as a function of the current node, so the way I represent the branching is simply as a function: a -> EnumProc b, where a is the type of the current node and b the type of the subsequent nodes. For my application, these are usually proof states in a resolution proof, but I have not explained anything about my particular application at all so far. Quoting Olaf Klinke on Fri, 12 Jul 2019 21:47:01 +0200:

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.

-- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.