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

[Juan Casanova]

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 <olf at aatal-apotheke.de> 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.