# Re: "Quantization" of computations, or step-wise termination, as an extension of Logic Monads Classic List Threaded 2 messages Reply | Threaded
Open this post in threaded view
|

## Re: "Quantization" of computations, or step-wise termination, as an extension of Logic Monads

 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. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafeOnly members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

## Re: "Quantization" of computations, or step-wise termination, as an extension of Logic Monads

 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 <[hidden email]> 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. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafeOnly members subscribed via the mailman list are allowed to post.