Saturday, February 14, 2009

Resources for folds

Reading this post by Matthew Podwysocki, who's a super smart guy, inspired me. I figure, even if I don't manage to come up with interest blog posts on my own, I can at least piggyback on other really smart people, and blog about their blogs.

So, in that spirit, I thought I'd at least make some comments about some great resources for understanding and experimenting with folds. For example, on #haskell on the freenode IRC, there's a bot called lambdabot, which can interpret haskell. One cool thing it can do is give a bit better idea of how an expression would be evaluated, via the SimpleReflect module (which is quite cool, and explained here). Below is a sample session:
09:28:42 <chessguy> > foldl f 1 [1..5] :: Expr
09:28:43 <lambdabot> f (f (f (f (f 1 1) 2) 3) 4) 5
09:28:56 <chessguy> > foldl' f 1 [1..5] :: Expr
09:28:58 <lambdabot> f (f (f (f (f 1 1) 2) 3) 4) 5
09:29:17 <chessguy> > foldr f 1 [1..5] :: Expr
09:29:19 <lambdabot> f 1 (f 2 (f 3 (f 4 (f 5 1))))
Also, speaking of really smart guys, here's a resource from Cale Gibbard. This shows diagrams of how various folds are evaluated.

Here's a link to the Real World Haskell discussion of folds.

And finally, for the only bit of original work in this entry, here's a (very inefficient) logical entailment algorithm, written as a fold, by yours truly:


-- one sentence entails a second sentence if negating the second
-- and inserting its clauses, and the clauses that can be deduced, into
-- the first, results in a contradiction (which we'll represent as an
-- empty list of clauses)
entails :: (Show a,Eq a) => Sentence a -> Sentence a -> Bool
entails s1 s2 = any null $ foldr insert s1 (neg s2)

insert :: (Show a,Eq a) => Clause a -> [Clause a] -> [Clause a]
insert x y | x `elem` y = y
insert x [] = [x] -- inserting a clause into a tautology gives just that clause
insert x y | contradiction x = [[]] -- inserting a clause which is contradictory is also a contradiction
| otherwise = foldr insert (nub$x:y) (filter (not . (`elem` (x:y))) $ concatMap (resolve x) y)

contradiction :: Clause a -> Bool
contradiction = null

-- a list of all the ways the resolution law can be applied:
-- http://en.wikipedia.org/wiki/Resolution_(logic)#Resolution_in_propositional_logic
resolve :: Eq a => Clause a -> Clause a -> [Clause a]
resolve xs ys = [combine x (xs ++ ys) | x <- xs, (neg_term x) `elem` ys]

combine :: Eq a => Term a -> Clause a -> Clause a
combine x = nub . delete x . delete (neg_term x)

No comments: