Send Beginners mailing list submissions to
[email protected]
To subscribe or unsubscribe via the World Wide Web, visit
http://www.haskell.org/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Using the state monad. (dan portin)
2. Re: Integer performance of GHC (Sebasti?n E. Peyrott)
3. Re: Integer performance of GHC (Sebasti?n E. Peyrott)
4. Re: Using the state monad. (Stephen Tetley)
----------------------------------------------------------------------
Message: 1
Date: Sat, 7 Aug 2010 10:14:05 -0700
From: dan portin <[email protected]>
Subject: [Haskell-beginners] Using the state monad.
To: [email protected]
Message-ID:
<[email protected]>
Content-Type: text/plain; charset="utf-8"
I wrote a simple tableau theorem prover for propositional logic as my first
Haskell program. My next goal is to write a theorem prover for modal logic.
Fortunately, this is more complicated. In essence, I have a tableau data
type, a rules function, and a rewrite function, which generate a tableau,
surrounded by auxiliary functions to collapse the tableau into paths and
extract interpretations. The tableau rewrite function is below. The "Status"
and "check" functions are unnecessary, but I added them anyways, because
some (other) tableau proof systems will require them.
data Tableau = Node Status Expr [Tableau]
deriving Eq
data Status = C | I
deriving (Show, Eq)
-- Rules for propositional tableau. Rules are of the form (s, ex), where
-- the value of s (Action) indicates the appropriate action (extend or
branch)
-- for the tableau rewritign function to take when injecting the formulas in
-- the list ex.
rule :: Expr -> (Action, [Expr])
rule (Var x) = (None, [Var x])
rule (Not (Var x)) = (None, [Not (Var x)])
rule (Not (Not e)) = (Extend, [e])
rule (Impl e1 e2) = (Branch, [Not e1, e2])
rule (Not (Impl e1 e2)) = (Extend, [e1, Not e2])
rule (Conj e1 e2) = (Extend, [e1, e2])
rule (Not (Conj e1 e2)) = (Branch, [Not e1, Not e2])
rule (Disj e1 e2) = (Branch, [e1, e2])
rule (Not (Disj e1 e2)) = (Extend, [Not e1, Not e2])
-- 'rewrite' constructs a complete tableau from a given tableau by applying
the
-- appropriate tableau rule at each incomplete node, then appropriately
-- injecting the resultant expressions into the tableau. 'rewrite' recurses
over
-- the tableau until all nodes are complete. 'consTableau' constructs a
-- complete tableau from an expression.
consTableau :: Expr -> Tableau
consTableau e = rewrite $ Node I e []
rewrite :: Tableau -> Tableau
rewrite t = case (isComplete t) of
True -> moveAnd rewrite t
False -> case (rule $ getExpr t) of
(None, _) -> check $ moveAnd rewrite t
(Extend, ex) -> rewrite (check $ inject Extend ex t)
(Branch, ex) -> rewrite (check $ inject Branch ex t)
inject :: Action -> [Expr] -> Tableau -> Tableau
inject a ex (Node s expr []) = case a of
Extend -> Node s expr [foldr (\e y -> Node I e [y]) (Node I (last ex) [])
(init ex)]
Branch -> Node s expr $ map (\e -> Node I e []) ex
inject a ex (Node s expr es) = Node s expr $ map (\b -> inject a ex b) es
The most common rule for modal tableaux is:
For a formula (âP, *w*), increment *w* by some number *n *to yield the
relation (*w*, *w* + *n*), then extending the tableau with a formula (P, *w
+ n*) for each formula (â»P, *w*) on the current path.
In order to implement the rule, I would need to: (a) save the state of the
tableau after each rewrite rule is applied; (b) if a rewrite rule for â is
applied, index the resultant relation and rewrite every formula â»P on the
current path; (3) check for infinite loops using a fairly simple algorithm.
I see two ways this could be accomplished: (1) Implement the tableau
rewriting using the state monad; (2) use a function like *rewrite* which
saves the state of the tableau in an argument (so that after each rewrite,
the state of the tableau is stored, and I can restart the recursion at that
point).
I'm trying to learn Haskell, however, so I'd like to learn more about
monads. I understand the simple examples of monads generally given in
tutorials (like Wadler's paper, which I'm working through), but I'm not sure
what the *general structure* of what I'm looking for would look like (that
is a problem). So my question, finally, is: *what would be the general
structure of the implementation of the state monad for a tableau-style
theorem prover* *look like, schematically*. I can't really square my goal
with example implementations of the state monad, where the state is threaded
through in a series of let expressions.
Thanks, and sorry for the long post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://www.haskell.org/pipermail/beginners/attachments/20100807/fa62939d/attachment-0001.html
------------------------------
Message: 2
Date: Sat, 7 Aug 2010 14:52:38 -0300
From: Sebasti?n E. Peyrott <[email protected]>
Subject: Re: [Haskell-beginners] Integer performance of GHC
To: [email protected]
Message-ID:
<[email protected]>
Content-Type: text/plain; charset=UTF-8
Thanks for the links. I had already seen Don's post, but I have yet to
try the LLVM backend. I'll do so as soon as a stable GHC version with
it is out.
The Haskell math performance link is interesting. If I'm not mistaken,
the OP achieved C levels of performance by switching to Data.Vector
and keeping data structures as close to C as possible. That seems
reasonable. However, for the example I gave earlier (an MD5
implementation), I don't see a way to use Data.Vector. The algorithm
performs repeated operations on 4 32-bit integers and that's it. The
implementation in Happstack is as close to C as possible, yet it's
still slower. My own too.
I've been trying to read the generated Core and assembly but I don't
really have any experience doing that. I can see most fields are
unboxed and inlining appears to be working. I see repeated calls to
GHC.Prim.narrow32Word# too. In the generated assembly I see many
operations with literal '$4294967295'. Could that be the culprit?
I have uploaded the generated Core for the main MD5 computation
(RFC1321, section 3.4) here: http://pastebin.com/e51njdcS
The actual computation starts at line 1507. Please note this is not
from the version in Happstack but rather from my own. You can find
RFC1321 here: http://tools.ietf.org/html/rfc1321
If you feel talking about Core and assembly is perhaps not suitable
for Haskell-beginners, I'll move this discussion to Haskell-cafe.
Thanks.
2010/8/7 David Virebayre <[email protected]>:
> 2010/8/7 Sebastián E. Peyrott <[email protected]>:
>> Hi, I'm looking for information on Haskell's viability for heavy
>> integer math. My (very) naive tests show Haskell lagging behind C even
>
> Relevant links :
>
>
> Benefits of the LLVM code generator (lots of other relevant posts on Dons'
> blog)
> http://donsbot.wordpress.com/2010/02/21/smoking-fast-haskell-code-using-ghcs-new-llvm-codegen/
>
> Archive of threads about loop unrolling :
> http://www.haskell.org/pipermail/glasgow-haskell-users/2009-March/thread.html#16741
>
> (Also check some of the links in "You might also be interested in:")
> http://efreedom.com/Question/1-2978979/Haskell-math-performance
>
> David.
>
------------------------------
Message: 3
Date: Sat, 7 Aug 2010 20:42:31 -0300
From: Sebasti?n E. Peyrott <[email protected]>
Subject: Re: [Haskell-beginners] Integer performance of GHC
To: [email protected]
Message-ID:
<[email protected]>
Content-Type: text/plain; charset=UTF-8
I just tried the LLVM code generator from GHC HEAD. I must say I am
impressed. Now my simple MD5 is just 1.8 times slower, rather 2.77.
Still not as efficient as I would like, but hey...
I'll have a look at the generated assembly.
2010/8/7 Sebastián E. Peyrott <[email protected]>:
> Thanks for the links. I had already seen Don's post, but I have yet to
> try the LLVM backend. I'll do so as soon as a stable GHC version with
> it is out.
>
> The Haskell math performance link is interesting. If I'm not mistaken,
> the OP achieved C levels of performance by switching to Data.Vector
> and keeping data structures as close to C as possible. That seems
> reasonable. However, for the example I gave earlier (an MD5
> implementation), I don't see a way to use Data.Vector. The algorithm
> performs repeated operations on 4 32-bit integers and that's it. The
> implementation in Happstack is as close to C as possible, yet it's
> still slower. My own too.
>
> I've been trying to read the generated Core and assembly but I don't
> really have any experience doing that. I can see most fields are
> unboxed and inlining appears to be working. I see repeated calls to
> GHC.Prim.narrow32Word# too. In the generated assembly I see many
> operations with literal '$4294967295'. Could that be the culprit?
>
> I have uploaded the generated Core for the main MD5 computation
> (RFC1321, section 3.4) here: http://pastebin.com/e51njdcS
> The actual computation starts at line 1507. Please note this is not
> from the version in Happstack but rather from my own. You can find
> RFC1321 here: http://tools.ietf.org/html/rfc1321
>
> If you feel talking about Core and assembly is perhaps not suitable
> for Haskell-beginners, I'll move this discussion to Haskell-cafe.
>
> Thanks.
>
> 2010/8/7 David Virebayre <[email protected]>:
>> 2010/8/7 Sebastián E. Peyrott <[email protected]>:
>>> Hi, I'm looking for information on Haskell's viability for heavy
>>> integer math. My (very) naive tests show Haskell lagging behind C even
>>
>> Relevant links :
>>
>>
>> Benefits of the LLVM code generator (lots of other relevant posts on Dons'
>> blog)
>> http://donsbot.wordpress.com/2010/02/21/smoking-fast-haskell-code-using-ghcs-new-llvm-codegen/
>>
>> Archive of threads about loop unrolling :
>> http://www.haskell.org/pipermail/glasgow-haskell-users/2009-March/thread.html#16741
>>
>> (Also check some of the links in "You might also be interested in:")
>> http://efreedom.com/Question/1-2978979/Haskell-math-performance
>>
>> David.
>>
>
------------------------------
Message: 4
Date: Sun, 8 Aug 2010 14:32:38 +0100
From: Stephen Tetley <[email protected]>
Subject: Re: [Haskell-beginners] Using the state monad.
To: dan portin <[email protected]>
Cc: [email protected]
Message-ID:
<[email protected]>
Content-Type: text/plain; charset=ISO-8859-1
On 7 August 2010 18:14, dan portin <[email protected]> wrote:
> So my question, finally, is: what would be the general structure
> of the implementation of the state monad for a tableau-style theorem prover
> look like, schematically.
Hi Dan
One would need a detailed knowledge of tableau-style theorem provers
to answer that...
In the code above Tableau is the same type after rewriting. If that's
the case, maybe you don't need a state monad solution. However, if you
are labelling something with /w/ which looks like an integer from your
explanation, then first you want to make a variation of the Tableau
datatype that holds the label, thus rewrite would be a type changing
function:
rewrite :: Tableau -> Tableau'
Where Tableau' is an alternative definition of Tableau that includes a
field for /w/ (possibly in the auxiliary types Status or Expr, which
would likewise need an alternative definition).
If this is what you want to do, you should be able to thread "number
supply" through the rewrite and rule functions fairly simply with a
state monad.
rewrite :: Tableau -> State Int Tableau'
Best wishes
Stephen
------------------------------
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
End of Beginners Digest, Vol 26, Issue 17
*****************************************
