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.s...@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.and...@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.s...@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.and...@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.and...@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.d...@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@haskell.org > >> > http://www.haskell.org/mailman/listinfo/haskell-cafe > >> > > >> > > > > > >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe