Re: [Haskell-cafe] Fold that quits early?

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_... 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 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

...

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 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 :

...

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@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

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,

On Sat, Jan 24, 2009 at 7:26 PM, Andrew Wagner wrote: 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe