[Haskell-cafe] "Quantization" of computations, or step-wise termination, as an extension of Logic Monads
juan.casanova at ed.ac.uk
Fri Jul 12 21:32:12 UTC 2019
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
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.
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
> 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?
> 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.
More information about the Haskell-Cafe