Hello; I am writing a parallel theorem prover using Haskell, and I am trying to do several things. As a first cut, I want to try using the par construct to attempt right and left rules simultaneously, and to evaluate both branches of an and clause in parallel. My code (attached) does not seem to generate sparks, however. When I run ./proposition +RTS -N2 -sstderr I get that no sparks are created. What am I doing wrong? Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first. Can I use strategies to code up something like this? I suppose this doesn't play nicely with the idea of determinism, but thought it might be worth asking anyway. Thanks, -Jamie
On Sun, 2009-12-20 at 17:25 -0500, Jamie Morgenstern wrote:
Hello;
I am writing a parallel theorem prover using Haskell, and I am trying to do several things. As a first cut, I want to try using the par construct to attempt right and left rules simultaneously, and to evaluate both branches of an and clause in parallel. My code (attached) does not seem to generate sparks, however. When I run
./proposition +RTS -N2 -sstderr
I get that no sparks are created. What am I doing wrong?
Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first. Can I use strategies to code up something like this? I suppose this doesn't play nicely with the idea of determinism, but thought it might be worth asking anyway.
Thanks, -Jamie
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-threaded? Regards
I did compile with -threaded.
On Sun, Dec 20, 2009 at 5:42 PM, Maciej Piechotka
On Sun, 2009-12-20 at 17:25 -0500, Jamie Morgenstern wrote:
Hello;
I am writing a parallel theorem prover using Haskell, and I am trying to do several things. As a first cut, I want to try using the par construct to attempt right and left rules simultaneously, and to evaluate both branches of an and clause in parallel. My code (attached) does not seem to generate sparks, however. When I run
./proposition +RTS -N2 -sstderr
I get that no sparks are created. What am I doing wrong?
Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first. Can I use strategies to code up something like this? I suppose this doesn't play nicely with the idea of determinism, but thought it might be worth asking anyway.
Thanks, -Jamie
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-threaded?
Regards
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Dec 20, 2009, at 17:42 , Maciej Piechotka wrote:
-threaded?
RTS wouldn't accept -N2 if it weren't compiled threaded. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH
Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie Morgenstern:
Hello;
I am writing a parallel theorem prover using Haskell, and I am trying to do several things. As a first cut, I want to try using the par construct to attempt right and left rules simultaneously, and to evaluate both branches of an and clause in parallel. My code (attached) does not seem to generate sparks, however. When I run
./proposition +RTS -N2 -sstderr
I get that no sparks are created. What am I doing wrong?
findProof ctx goal n = maybe where m1 = (tryRight ctx goal n) m2 = (tryLeft ctx goal n) m = m1 `par` m2 maybe = (m1 `mplus` m2) You never use m, so no threads are sparked. Put the par where it will actually be used: findProof ctx goal n = m2 `par` (m1 `mplus` m2) where m1 = (tryRight ctx goal n) m2 = (tryLeft ctx goal n) and you get sparks (5 (4 converted, 0 pruned)). You know that you get a pattern match error due to incomplete patterns in tryLeftHelper, though, do you?
Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first.
This wouldn't be easy to reconcile with referential transparency. You can do that in IO, roughly m <- newEmptyMVar t1 <- forkIO $ method1 >>= putMVar m t2 <- forkIO $ method2 >>= putMVar m rs <- takeMVar m killThread t1 killThread t2 return rs But in pure code, I think not.
Can I use strategies to code up something like this? I suppose this doesn't play nicely with the idea of determinism, but thought it might be worth asking anyway.
Thanks, -Jamie
On Mon, Dec 21, 2009 at 12:39:06AM +0100, Daniel Fischer wrote:
Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie Morgenstern:
Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first.
This wouldn't be easy to reconcile with referential transparency. You can do that in IO, roughly
m <- newEmptyMVar t1 <- forkIO $ method1 >>= putMVar m t2 <- forkIO $ method2 >>= putMVar m rs <- takeMVar m killThread t1 killThread t2 return rs
But in pure code, I think not.
There's 'unamb' in Hackage, however I think you should carefully understand its implementation details before using it. Not that I use it myself. Link: http://hackage.haskell.org/package/unamb -- Felipe.
Felipe Lessa schrieb:
On Mon, Dec 21, 2009 at 12:39:06AM +0100, Daniel Fischer wrote:
Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie Morgenstern:
Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first. This wouldn't be easy to reconcile with referential transparency. You can do that in IO, roughly
m <- newEmptyMVar t1 <- forkIO $ method1 >>= putMVar m t2 <- forkIO $ method2 >>= putMVar m rs <- takeMVar m killThread t1 killThread t2 return rs
But in pure code, I think not.
There's 'unamb' in Hackage, however I think you should carefully understand its implementation details before using it. Hello Jamie, you might want to have a look at the implementation of `race` in the Conal's 'unamb' package:
http://hackage.haskell.org/packages/archive/unamb/0.2.2/doc/html/src/Data-Un... As your left and right branch do not neccessarily have the same result, you have to stay in the IO monad. The function provided by that package is:
amb :: a -> a -> IO a
Not that I use it myself. Neither do I, btw.
benedikt
Am Montag 21 Dezember 2009 01:00:10 schrieb Felipe Lessa:
On Mon, Dec 21, 2009 at 12:39:06AM +0100, Daniel Fischer wrote:
Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie Morgenstern:
Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first.
This wouldn't be easy to reconcile with referential transparency. You can do that in IO, roughly
m <- newEmptyMVar t1 <- forkIO $ method1 >>= putMVar m t2 <- forkIO $ method2 >>= putMVar m rs <- takeMVar m killThread t1 killThread t2 return rs
But in pure code, I think not.
There's 'unamb' in Hackage, however I think you should carefully understand its implementation details before using it. Not that I use it myself.
Which is a (much) refined version of the above, wrapped in unsafePerformIO. It is your obligation to call it only when legit, because it is *not* referentially transparent: Prelude Data.Unamb> let go :: Int -> Bool -> Bool; go 0 b = b; go n b = let c = not b in c `seq` go (n-1) c Prelude Data.Unamb> :set +s Prelude Data.Unamb> let fun n = go n True (0.00 secs, 0 bytes) Prelude Data.Unamb> unamb (fun $ 10^6) (fun $ 10^6+1) Loading package unamb-0.2.2 ... linking ... done. True (2.38 secs, 75324960 bytes) Prelude Data.Unamb> unamb (fun $ 10^6) (fun $ 10^6+1) False (2.29 secs, 73940848 bytes)
Link: http://hackage.haskell.org/package/unamb
-- Felipe.
On Mon, Dec 21, 2009 at 01:46:57AM +0100, Daniel Fischer wrote:
Am Montag 21 Dezember 2009 01:00:10 schrieb Felipe Lessa:
There's 'unamb' in Hackage, however I think you should carefully understand its implementation details before using it. Not that I use it myself.
Which is a (much) refined version of the above, wrapped in unsafePerformIO. It is your obligation to call it only when legit, because it is *not* referentially transparent:
Actually my concern was about performance, not correctness. That's why I mentioned the "implementation details". It is probably easy to make your machine crawl by putting unamb in your inner loop. -- Felipe.
Am Montag 21 Dezember 2009 02:03:20 schrieb Felipe Lessa:
Actually my concern was about performance, not correctness. That's why I mentioned the "implementation details". It is probably easy to make your machine crawl by putting unamb in your inner loop.
Heh :D I'd think so, too.
-- Felipe.
Daniel Fischer schrieb:
Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie Morgenstern:
Hello;
Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first.
This wouldn't be easy to reconcile with referential transparency. You can do that in IO, roughly
m <- newEmptyMVar t1 <- forkIO $ method1 >>= putMVar m t2 <- forkIO $ method2 >>= putMVar m rs <- takeMVar m killThread t1 killThread t2 return rs
And in this case (returning (Maybe Proof)), you are not happy with any of the results, but with one of the proofs. So you would need something like solve :: Ctx -> Prop -> Int -> IO (Maybe Proof) solve ctx goal n = amb leftRight rightLeft where leftRight = m1 `mplus` m2 rightLeft = m2 `mplus` m1 m1 = (tryRight ctx goal n) m2 = (tryLeft ctx goal n) I think the idea of directly supporting this kind of thing is quite interesting. benedikt
Thank you for all of the responses! The amb package is something like what I
want; though, as aforementioned, the right and left rules won't return the
same proof and so we can't really use it here.
I've been thinking about this problem generally, not just in the Haskell
setting. It makes sense (in the very least, with theorem proving)
to allow
a p|| b
to return the value of a or b, whichever returns first, wrapped in a
constructor which would allow you to case analyze which result returned
case (a p|| b) of
(1, Xa) = ...
(2, Xb) = ...
On Sun, Dec 20, 2009 at 8:52 PM, Benedikt Huber
Daniel Fischer schrieb:
Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie Morgenstern:
Hello;
Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first.
This wouldn't be easy to reconcile with referential transparency. You can do that in IO, roughly
m <- newEmptyMVar t1 <- forkIO $ method1 >>= putMVar m t2 <- forkIO $ method2 >>= putMVar m rs <- takeMVar m killThread t1 killThread t2 return rs
And in this case (returning (Maybe Proof)), you are not happy with any of the results, but with one of the proofs. So you would need something like
solve :: Ctx -> Prop -> Int -> IO (Maybe Proof) solve ctx goal n = amb leftRight rightLeft where leftRight = m1 `mplus` m2 rightLeft = m2 `mplus` m1
m1 = (tryRight ctx goal n) m2 = (tryLeft ctx goal n)
I think the idea of directly supporting this kind of thing is quite interesting.
benedikt
\a b -> Left a `amb` Right b
________________________________
From: haskell-cafe-bounces@haskell.org
[mailto:haskell-cafe-bounces@haskell.org] On Behalf Of Jamie Morgenstern
Sent: 21 December 2009 16:50
To: Benedikt Huber
Cc: haskell-cafe@haskell.org
Subject: [Haskell-cafe] Re: no sparks?
Thank you for all of the responses! The amb package is something like
what I want; though, as aforementioned, the right and left rules won't
return the same proof and so we can't really use it here.
I've been thinking about this problem generally, not just in the Haskell
setting. It makes sense (in the very least, with theorem proving)
to allow
a p|| b
to return the value of a or b, whichever returns first, wrapped in a
constructor which would allow you to case analyze which result returned
case (a p|| b) of
(1, Xa) = ...
(2, Xb) = ...
On Sun, Dec 20, 2009 at 8:52 PM, Benedikt Huber
On Dec 20, 2009, at 2:25 PM, Jamie Morgenstern wrote:
Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first. Can I use strategies to code up something like this? I suppose this doesn't play nicely with the idea of determinism, but thought it might be worth asking anyway.
There is in fact a package that seems to do exactly that; look up "unamb" (short for "unambiguous choice") on Hackage. Cheers, Greg
participants (8)
-
Benedikt Huber -
Brandon S. Allbery KF8NH -
Daniel Fischer -
Felipe Lessa -
Gregory Crosswhite -
Jamie Morgenstern -
Maciej Piechotka -
Sittampalam, Ganesh