[Haskell-cafe] Fold that quits early?

Andrew Wagner wagner.andrew at gmail.com
Sat Jan 24 23:54:48 EST 2009 

Ok, maybe let's make this a little more concrete. I'm trying to write
forward-chaining logical inference as a fold. I actually don't mind this
code much as it is (about half or 2/3 the size it was an hour ago), but I'm
wondering if I can do better.

-- a sentence is a conjunction of clauses
type Sentence a = [Clause a]

-- each clause is a disjunction of terms
type Clause a = [Term a]

-- 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 :: Eq a => Sentence a -> Sentence a -> Bool
entails s1 s2 = null $ foldr (flip insertInto) s1 (neg s2)

insertInto :: Eq a => [Clause a] -> Clause a -> [Clause a]
insertInto [] _ = [] -- inserting into a contradictory set of clauses is
still contradictory
insertInto x y | contradiction y = [] -- inserting a clause which is
contradictory is also a contradiction
                     | otherwise = foldr (flip insertInto) (y:x) (concatMap
(resolve y) x)

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)


On Sat, Jan 24, 2009 at 11:25 PM, Ryan Ingram <ryani.spam at gmail.com> wrote:

> My point is that without further knowledge of this function, it's not
> possible to simplify into a fold.  For f to be a fold, the result
> would have to terminate for *every* total function g; given that there
> are some total functions for which f does not terminate, f cannot be a
> fold.
>
> It's possible that the particular combination of f and g that you have
> in mind *does* simplify to a fold, but the current function cannot,
> unless I've made a mistake.
>
>  -- ryan
>
> On Sat, Jan 24, 2009 at 7:26 PM, Andrew Wagner <wagner.andrew at gmail.com>
> wrote:
> > There's at least one thing; I won't call it a flaw in your logic, but
> it's
> > not true of my usage. Your definition always produces a non-null list.
> The
> > particular g in my mind will eventually produce a null list, somewhere
> down
> > the line. I think if that's true, we can guarantee termination.
> >
> > On Sat, Jan 24, 2009 at 10:16 PM, Ryan Ingram <ryani.spam at gmail.com>
> wrote:
> >>
> >> foldr f z xs =
> >>   x0 `f` (x1 `f` (x2 `f` ... (xN `f` z) ...))
> >>
> >> In particular, note that if f is a total function, xs is finite and
> >> totally defined, and z is totally defined, then the result of this
> >> fold is totally defined.
> >>
> >> Now consider your "f" (rewritten slightly)
> >>
> >> f x xs
> >>   | null xs = []
> >>   | p x = []
> >>   | otherwise = foldr f (x:xs) (g x xs)
> >>
> >> with these definitions:
> >>
> >> c _ = False
> >> g = (:)
> >>
> >> c and g are definitely total functions, so what happens when we
> >> evaluate f 0 [1]?
> >>
> >> f 0 [1]
> >>        = foldr f [0,1] [0,1]
> >>        = let t1 = foldr f [0,1] [1] in f 0 $ t1
> >>        = let t1 = foldr f [0,1] [1] in foldr f (0 : t1) (0 : t1)
> >>        = let t1 = foldr f [0,1] [1]
> >>              t2 = foldr f (0:t1) t1
> >>          in f 0 t2
> >>
> >> etc.; this is clearly non-terminating.
> >>
> >> Therefore there is no way to make f into a fold.
> >>
> >> Any errors in my logic?
> >>
> >>  -- ryan
> >>
> >> 2009/1/24 Andrew Wagner <wagner.andrew at gmail.com>:
> >> > Ahem. That's what happens when you don't type-check your brainstorming
> >> > before barfing it out, kids. Sorry about that. Let's try this again:
> >> >
> >> > f _ [] = []
> >> > f y x | c y = []
> >> >         | otherwise = foldr f (y:x) (g y x)
> >> >
> >> > I've got a fold on the inside now, but I'm pretty sure the whole thing
> >> > is
> >> > just a fold. Not quite there yet, though...
> >> >
> >> > On Sat, Jan 24, 2009 at 1:42 PM, Andrew Wagner <
> wagner.andrew at gmail.com>
> >> > wrote:
> >> >>
> >> >> Actually, I think I can rewrite it this way:
> >> >>
> >> >> f xs [] = False
> >> >> f xs (y:ys) | any c ys' = True
> >> >>                 | otherwise = f (f (y:xs) ys') ys
> >> >>   where ys' = g y ys
> >> >>
> >> >> This should help, I think.
> >> >>
> >> >> On Sat, Jan 24, 2009 at 12:11 PM, Dan Doel <dan.doel at gmail.com>
> wrote:
> >> >>>
> >> >>> On Saturday 24 January 2009 11:39:13 am Andrew Wagner wrote:
> >> >>> > This is almost a fold, but seemingly not quite? I know I've seem
> >> >>> > some
> >> >>> > talk
> >> >>> > of folds that potentially "quit" early. but not sure where I saw
> >> >>> > that,
> >> >>> > or
> >> >>> > if it fits.
> >> >>> >
> >> >>> > f xs [] = False
> >> >>> > f xs (y:ys) | any c ys' = True
> >> >>> >
> >> >>> >             | otherwise = f (nub (y:xs)) (ys' ++ ys)
> >> >>> >
> >> >>> >    where ys' = g y xs
> >> >>>
> >> >>> Quitting early isn't the problem. For instance, any is defined in
> >> >>> terms
> >> >>> of
> >> >>> foldr, and it works fine on infinite lists, quitting as soon as it
> >> >>> finds
> >> >>> a
> >> >>> True. As long as you don't use the result of the recursive call
> (which
> >> >>> is
> >> >>> the
> >> >>> second argument in the function you pass to foldr), it will exit
> >> >>> early.
> >> >>>
> >> >>> The problem is that your function doesn't look structurally
> recursive,
> >> >>> and
> >> >>> that's what folds (the usual ones, anyway) are: a combinator for
> >> >>> structural
> >> >>> recursion. The problem is in your inductive case, where you don't
> just
> >> >>> recurse
> >> >>> on "ys", you instead recurse on "ys' ++ ys", where ys' is the result
> >> >>> of
> >> >>> an
> >> >>> arbitrary function. folds simply don't work that way, and only give
> >> >>> you
> >> >>> access
> >> >>> to the recursive call over the tail, but in a language like Agda,
> the
> >> >>> termination checker would flag even this definition, and you'd have
> >> >>> to,
> >> >>> for
> >> >>> instance, write a proof that this actually does terminate, and do
> >> >>> induction on
> >> >>> the structure of the proof, or use some other such technique for
> >> >>> writing
> >> >>> non-
> >> >>> structurally recursive functions.
> >> >>>
> >> >>> -- Dan
> >> >>
> >> >
> >> >
> >> > _______________________________________________
> >> > Haskell-Cafe mailing list
> >> > Haskell-Cafe at haskell.org
> >> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >> >
> >> >
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090124/f017fb23/attachment.htm

More information about the Haskell-Cafe mailing list