[Haskell] Re: A MonadPlusT with fair operations and pruning
oleg at pobox.com
oleg at pobox.com
Sat Jul 16 01:52:44 EDT 2005
on Jun 22 Andrew Bromage wrote about the usefulness of
soft-cuts and "don't care" non-determinism in non-deterministic
computations in Haskell.
> http://www.haskell.org/pipermail/haskell/2005-June/016037.html
Thank you very much for your explanation, it was helpful indeed. You
noted,
> Some of the interesting examples in Prolog are moot in Haskell by virtue
> of the fact that Haskell is "strongly moded"
And hence was our quandary. Even the leanTAP theorem prover looked too
simple in Haskell to serve as a good example of advanced
non-determinism. Your Tic-Tac-Toe example is thus even more
appreciated. We have extended your code to boards of arbitrary NxN
size (with M consecutive marks needed for winning). There is also a
function for a human to play against the machine. We added some limits
on the breadth and the depth of the search -- to keep both the
reasonable response time and the pride. All in all, playing on the 5x5
board (with 4 marks needed for winning) is fairly entertaining. The
archive LogicT.tar.gz mentioned previously now contains the
tic-tac-toe code. The paper has been updated with its description.
BTW,
> best p b
...
> | otherwise
> = ifte (once (do
> m <- choose [1..9]
> b' <- move m p b
> guard (win p b)
> return (Win, b')))
> return
> return
> (ifte (once (do
> m <- choose [1..9]
> b' <- move m (otherPlayer p) b
> guard (win (otherPlayer p) b')
> return m))
> (\m -> do
> b' <- move m p b
> (w,_) <- best (otherPlayer p) b'
> return (w,b'))
The last statement should probably be `return (otherState w,b')',
right?
on Jan 5 2005, Andrew Bromage wrote on Haskell-Cafe:
> Logical if-then-else has this signature:
>
> mif :: LogicT m a -> (a -> LogicT m b) -> LogicT m b -> LogicT m b
>
> Intuitively, this takes three arguments: the "condition", the "then"
> case and the "else" case. This obeys the "obvious" laws of if-then-else:
>
> mif (return a) t e = t a
> mif (mzero) t e = e
> mif (mif c t' e') t e = mif c (\x -> mif (t' x) t e) (mif e' t e)
Chung-chieh Shan has pointed out a problem with the last law: Let us
consider the following instance of that law. We use Prolog, which
implements soft-cuts (aka mif aka ifte) natively. In Prolog,
`mif test t e' is written as `test *-> t ; e'
He chose t === true, e === true, e' === fail, t' === X = 1,
c === (X=1 ; X=2)
mif (mif c t' e') t e
translates to
((X=1 ; X=2) *-> X=1 ; fail) *-> true; true.
and gives one answer, 1.
mif c (\x -> mif (t' x) t e) (mif e' t e)
translates to
(X=1 ; X=2) *-> ( X=1 *-> true ; true) ; (fail *-> true; true).
and gives two answers, 1 and 2.
So, it seems the law has to be formulated in a more complex way,
mif (mif c t' e') t e =
mif (once c) (const $ mif (c >>= t') t e) (mif e' t e)
with a surprising occurrence of `once'. That formulation isn't
particularly useful for a backtracking _transformer_. In any case, we
haven't encountered a need to simplify "mif (mif c t' e') t e"
algebraically. It is interesting to see when such a law may be
required.
More information about the Haskell
mailing list