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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Juan Casanova
Dear all,

I just subscribed to this list so I'm not familiar with the usual way  
to go about things here. I hope you'll excuse any cultural mistakes I  
might make. I'll also try to keep this message as short as possible,  
but this is hard for me and it is a complex topic, so I will  
presumably fail. Apologies for that in advance.

Short introduction. I'm a PhD student at University of Edinburgh. My  
research is not on programming languages itself, but during the course  
of it I ended up programming in Haskell and more particularly faced a  
problem that I developed a strategy (and eventually a library) for.  
After some discussions with my supervisors and with some more Haskell  
experienced people around university, they suggested that I looked  
into some existing work and also that I posted on this list, and here  
I am.

Let me introduce the problem that I'm trying to solve itself. I have a  
particular (yet somehow typical) case of non-determinism (search) in  
the program that I have been writing. It is characterized by:

- No joining back of branches ever.
- Potentially infinite depth (this is usual).
- Potentially infinite width. Meaning that at a single point I may  
have an infinite amount of possible paths to follow.
- It is critical that the search is complete. After reading a bit, I  
have realized this is usually referred to as being a fair search  
order. For me this means that there can be many (infinite) valid  
solutions in the search space, and I want to find all of them (i.e.  
for every valid solution, the program will eventually output it).

As I said, I developed my own (particular) approach to this, then  
generalized it in a library, and then, after talking to some people,  
realized this might be something quite interesting to share, but first  
had to check that it's not something that has already been done.

Long story short, the most relevant piece of research I was pointed to  
was "Backtracking, interleaving and terminating monad transformers",  
by O Kiselyov, C Shan, DP Friedman and A Sabry, published in 2005.  
(https://dl.acm.org/citation.cfm?id=1086390). I also know that this  
approach is embodied in Haskell through the Control.Monad.Logic  
library. I read the paper and skimmed through some related work, and  
gave a try to the library. Indeed, it seems to be doing mostly what I  
need. In particular, it can deal with infinite breadth/infinite width  
searches through a process of what I call "diagonalization". That is,  
a combination of breadth-first and depth-first that ensures fairness.  
Note that the library actually does a lot more things that I didn't  
consider because they were not relevant for my problem, for instance  
cuts.

However, I find that there is something that this library does not  
take into account, and after trying with the Haskell library I have  
verified that indeed it does not work, whereas my library does work. I  
am wondering if I have overlooked some work in which this is also  
taken into account or if I may be onto some useful extension of  
Control.Monad.Logic that hasn't been done yet. I still have to find a  
stable name for the feature that I am talking about, but I usually  
refer to it as "step-wise termination" or "quantization of  
computations". To understand it consider an example (that I have  
actually implemented):

1. Whenever I have a non-deterministic enumeration, I should have a  
way to output a fair search among that non-deterministic search (a  
list), following the properties that I indicated above.
2. I can make an enumeration that non-deterministically produces all  
multiples of a certain number.
3. I can make an enumeration that non-deterministically produces all  
powers of a certain number.
4. I can make a function that, given an enumeration, filters it  
through a boolean function.
5. I can monadically combine computations, so that I can, for  
instance, produce a computation that is the result of producing all  
multiples of a number, and for each of those, producing all their  
powers.
6. So what happens if I combine the three of them. In particular, what  
if I output all *odd* powers of all multiples of 1 (all naturals)?  
(multiples 1) >>= (\x -> filter odd (powers x))?

If I do this using the Control.Monad.Logic library (and using the >>-  
operator provided there, of course), this does not produce a fair  
search. Specifically, it outputs 1 and then hangs up. The reason? The  
order in which the search is produced picks one value from each  
sublist at a time, but because there are no odd powers of an even  
number (say 2), it never finds any element in the sublist of powers of  
2, and therefore never gets to even try with the powers of 3.

My library can deal with this by "quantizing" computation, making sure  
that each individual step of a computation always terminates (in  
Haskell terms, I wrap things up in a way that I can guarantee that a  
single look-ahead on the list will always produce a head normal form  
in finite time, even if that is still a continuation of the  
computation). Therefore, while it keeps trying to find powers of 2  
that are odd, this does not stop the search over all the other sublists.

This mail is already quite long, but let me make a few precisions. You  
may stop reading here if you don't wanna get your hands dirty, I've  
said the most important bits. I know a bit of what I say here will be  
confusing if you don't think about it yourself, so skip it if it gets  
confusing. It's mainly to answer some questions/comments I can foresee.

Of course, this only works if the embedding into the monad is  
terminating itself. So, when you do "pure x" for my monad, you need to  
guarantee that "x" will produce a head normal form in finite time).  
But as long as you guarantee this atomic notion and you only use the  
monadic transformation functions that are not labelled as "unsafe"  
(which are only the unnatural ones for the semantics that I am  
considering, such as appending in a list sense), then I can guarantee  
the search will always be fair.

Also, a thing I've been thinking quite a bit is whether you can  
consider this notion of "quantization" of computation separately from  
the notion of an enumeration of a non-deterministic search space. Of  
course you can, but the interesting bit is to do this diagonalization  
over non-deterministic search spaces in a quantized way so that rabbit  
holes like the odd powers of 2 are not a problem. I tried to implement  
this in a generic way that you can later on "combine" with  
Control.Monad.Logic in a non-specific way, but it won't work, due to  
the particular reason that you'd need to do pattern matching over the  
structure of the logic monad, and there's no way to type check that  
for an arbitrary data type (because the pattern matching could give  
literally any potential sub-types). Implementing the quantization  
separately and then the combination individually as a one-of thing  
could be done, of course, but it would essentially be the same that I  
have right now. A different story would be had if ghci actually had  
monadic functions to enable the evaluation of *any* thunk  
one-step-at-a-time (that is, one function evaluation or one pattern  
match). This is absolutely not what seq does, because seq evaluates  
until it is a weak head normal form, which is not what I want.  
Precisely, bottom seq a = bottom, and my quantized computation does  
not fulfill this equation (and it should not).

My library is not perfect now, and after having read and understood  
the Control.Monad.Logic library, I think the best thing would be to  
extend it, which is something I don't do right now. But still so,  
unless I have missed an already existing implementation of something  
like this, or I am seeing something in a really convoluted way. Please  
feel free to drop any questions or comments at all.

I'm attaching an example of why Control.Monad.Logic does not work in  
the case that I said. It also includes an example using my library,  
which I am not attaching. This example works. Just comment it. I'm not  
attaching my library now because it's not "polished" and because it is  
a lot for people to randomly look at, but feel free to ask for it and  
I'll happily send it over, so that you can run the example with it.

Again, any questions or comments are welcome. Lead me the right  
direction with this.

... And sorry for the wall of text.

Thank you very much for all of your time and attention,
Juan Casanova.

--
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-cafe
Only members subscribed via the mailman list are allowed to post.

LogicVsEnumProc.hs (2K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

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

Li-yao Xia-2
Hello Juan,


On 7/11/19 3:24 PM, Juan Casanova wrote:
> I just subscribed to this list so I'm not familiar with the usual way to
> go about things here. I hope you'll excuse any cultural mistakes I might
> make.


You're most definitely welcome here. I dare say that anyone who
participates in the mailing list makes the rules (within the limits of
moderation of course).


 > feel free to ask for it and I'll happily
 > send it over, so that you can run the example with it.


I am curious to have a look at your library.


> Let me introduce the problem that I'm trying to solve itself. I have a
> particular (yet somehow typical) case of non-determinism (search) in the
> program that I have been writing. It is characterized by:
>
> - No joining back of branches ever.
> - Potentially infinite depth (this is usual).
> - Potentially infinite width. Meaning that at a single point I may have
> an infinite amount of possible paths to follow.
> - It is critical that the search is complete. After reading a bit, I
> have realized this is usually referred to as being a fair search order.
> For me this means that there can be many (infinite) valid solutions in
> the search space, and I want to find all of them (i.e. for every valid
> solution, the program will eventually output it).
>


I think all of these points can be addressed by starting from an
infinite binary tree.


data Tree a = Empty | Leaf a | Branch (Leaf a) (Leaf a)

instance Monad Tree where ...


In particular:

- infinite branching can be modeled by an infinite sequence of finite
branches: Branch 1 (Branch 2 (Branch 3 (...)));

- the problem of completeness is addressed by, uh, postponing it. Okay
that's not really addressed, but the point is that the data is all there
at least (not lost in a diverging computation), and the search problem
is now a very concrete tree traversal problem, which does not require
any fancy monadic abstraction a priori, but also does not prevent you
from building one up as other requirements make themselves known.


Regarding the issue of fairness you mention, a key point is that
"filter" should only replace Leaf with Empty, and not try to do any
merging like rewriting (Branch Empty t) to t. More precisely, as soon as
a function satisfies the equation

f (Branch Empty t) = f t,

then it has to diverge on trees with no leaves (or it has to discard
leaves, so it's useless if completeness is a concern). I'm guessing
that's where the logic monad goes astray.

One way to think of this problem is in terms of "productivity": "filter"
for Logic may not be productive if its argument represents an infinite
search space. In total programming languages, i.e., those which enforce
productivity, Agda and Coq being chief examples, you would actually be
stopped because the Logic monad cannot represent infinite search spaces
(such as log_multiples in your sample).

Coinductive types are a promising alternative here, with two main
solutions off the top of my head being coinductive trees, as I sketched
above, and coinductive lists/streams with an extra "delay" constructor.
I am curious to see how your library relates to that.

Cheers,
Li-yao
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only 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

Juan Casanova
Thank you for your very detailed and very relevant response. It made  
me think about some things.


> I am curious to have a look at your library.

I guess I'll just attach it here and end up sharing it with the whole  
list. Just hope noone feels overwhelmed by too much code to look at.



> I think all of these points can be addressed by starting from an  
> infinite binary tree.
>
>
> data Tree a = Empty | Leaf a | Branch (Leaf a) (Leaf a)
>
> instance Monad Tree where ...
>
>
> In particular:
>
> - infinite branching can be modeled by an infinite sequence of  
> finite branches: Branch 1 (Branch 2 (Branch 3 (...)));
This is correct, but not complete in general, although the logic monad  
library does deal with this. The problem is, if you have a conceptual  
infinite branching, in which each branch is infinite in depth, the  
process of expressing the infinite branching as an infinite sequence  
of finite branching will, if done naively, be unfair towards later  
branches. So, if I want to search all the multiples of all powers of  
2, the "naive" transformation will "concatenate" all those lists /  
branches, but because the first one is infinite, any search performed  
in that way will not reach the latter ones. In other words, things  
that were at depth 2 before will now be at depth infinity because you  
have prepended them with an infinite amount of finite branches. This  
can be overcome by doing the transformation from infinite branching to  
binary/finite branching diagonally, as I described and as the logic  
monad library does.

So, yeah, it can be modelled that way, but the process of translation  
is very relevant for fairness.

> - the problem of completeness is addressed by, uh, postponing it.  
> Okay that's not really addressed, but the point is that the data is  
> all there at least (not lost in a diverging computation), and the  
> search problem is now a very concrete tree traversal problem, which  
> does not require any fancy monadic abstraction a priori, but also  
> does not prevent you from building one up as other requirements make  
> themselves known.
>
>
> Regarding the issue of fairness you mention, a key point is that  
> "filter" should only replace Leaf with Empty, and not try to do any  
> merging like rewriting (Branch Empty t) to t. More precisely, as  
> soon as a function satisfies the equation
>
> f (Branch Empty t) = f t,
>
> then it has to diverge on trees with no leaves (or it has to discard  
> leaves, so it's useless if completeness is a concern). I'm guessing  
> that's where the logic monad goes astray.
This is a very good point, one that I had not thought of. In some  
sense, the problem is precisely that, that the logic monad library  
does not represent the computation itself (neither as a tree or as a  
list), but instead only the results, and therefore a filter must  
satisfy that equation, and therefore it will diverge.

>
> One way to think of this problem is in terms of "productivity":  
> "filter" for Logic may not be productive if its argument represents  
> an infinite search space. In total programming languages, i.e.,  
> those which enforce productivity, Agda and Coq being chief examples,  
> you would actually be stopped because the Logic monad cannot  
> represent infinite search spaces (such as log_multiples in your  
> sample).
>
> Coinductive types are a promising alternative here, with two main  
> solutions off the top of my head being coinductive trees, as I  
> sketched above, and coinductive lists/streams with an extra "delay"  
> constructor. I am curious to see how your library relates to that.
Indeed, my library relies essentially on lists/streams with an extra  
"delay" constructor. I must say the word "coinductive" got me a bit  
puzzled there, but after looking it up a bit, I think I understand  
what you mean. I definitely know what inductive means, I just did not  
know there was such a concept as coinduction.

You can see the library in the attachment, but the definition of my  
data structure is (I differentiate Empty from Halt but that is pretty  
inconsequential, it just alters how I deal with joining several  
infinites. In a sense it's a type of cut. I also wrap errors within  
it, which may be bad practice.):

data EnumProc t = Empty | Halt | Error String | Produce t (EnumProc t)  
| Continue (EnumProc t)

where the Continue constructor is the extra "delay" one. Whenever a  
function that works on this structure needs to do a recursive call (or  
mutually recursive call, etc.), instead of just doing the recursive  
call, I prepend it with "Continue", so that I can ensure that it will  
be in head normal form, and therefore I can perform the computation  
one step at a time.

Now, I see how you feel that Trees are a more natural way to describe  
the computation than infinite lists with delay, but I'm not sure if  
there are any actual advantages to using that approach instead of mine.

In other words, I think what you are suggesting is essentially what I  
did, and what you are saying are perhaps better argumented reasons as  
to why you need to do it. What I wonder is if there is indeed a way to  
do these kind of things with the logic monad library (and perhaps  
other standard libraries) without having to implement my own?

Thanks again,
Juan




--
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-cafe
Only members subscribed via the mailman list are allowed to post.

EnumProc.hs (40K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

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

Li-yao Xia-2


On 7/11/19 10:56 PM, Juan Casanova wrote:
> Thank you for your very detailed and very relevant response. It made me
> think about some things.


I'm glad you appreciated my answer!


 >> I am curious to have a look at your library.
 >
 > I guess I'll just attach it here and end up sharing it with the whole
 > list. Just hope noone feels overwhelmed by too much code to look at.


That looks quite reasonable. At a high level, one can imagine this
basically as a list library, so most functions look quite familiar at a
glance.


 >> - infinite branching can be modeled by an infinite sequence of finite
 >> branches: Branch 1 (Branch 2 (Branch 3 (...)));
 >
 > This is correct, but not complete in general, although the logic monad
 > library does deal with this. The problem is, if you have a conceptual
 > infinite branching, in which each branch is infinite in depth, the
 > process of expressing the infinite branching as an infinite sequence of
 > finite branching will, if done naively, be unfair towards later
 > branches. So, if I want to search all the multiples of all powers of 2,
 > the "naive" transformation will "concatenate" all those lists /
 > branches, but because the first one is infinite, any search performed in
 > that way will not reach the latter ones. In other words, things that
 > were at depth 2 before will now be at depth infinity because you have
 > prepended them with an infinite amount of finite branches. This can be
 > overcome by doing the transformation from infinite branching to
 > binary/finite branching diagonally, as I described and as the logic
 > monad library does.


For "all the multiples of all powers of 2", the tree obtained naively by
monadic composition will look like this:

mulPow2 = liftA2 (*) nats pow2s
-- Branch (... multiples of 2^0) (Branch (... multiples of 2^1) (Branch
(... multiples of 2^2) (...)))

-- where nats contains all natural numbers and pow2s all powers of 2.

No elements are lost precisely thanks to the tree structure allowing you
to nest subtrees without pushing others back.

That said, your approach is certainly still worth pursuing.


 > What I wonder is if there is indeed a way to do
 > these kind of things with the logic monad library (and perhaps other
 > standard libraries) without having to implement my own?


The problem you described appears to be deeply embedded in the
definition of LogicT. A handwavy argument is that Logic is exactly the
Church encoding of lists with Nil and Cons (Empty and Produce), but you
really need the Continue constructor in there.

One idea to try is "Logic (Maybe a)", since it is isomorphic to [Maybe
a] which is isomorphic to the Empty+Produce+Continue variant of lists
(using the names from your code). But although the representation is
equivalent, I'm not sure the abstractions are reusable enough to save
much work.


Cheers,
Li-yao
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.