Sebastian Fischer wrote:
> > Unfortunately, the relation between residuation and narrowing
> > is still not clear since there are also examples where
> > narrowing has a finite search space whereas the use of
> > residuation leads to an infinite seach space.
>
> Can you (or somebody else) remind me of such an example?
Sure, the example is quite old (from my paper on the analysis
of residuation, appeared in JLP'95). Consider the following program
(an unusual definition of a predicate for list reversal):
rev [] [] = success
rev l (x:xs) = lx++[x]=:=l & rev lx xs where lx free
Then the goal "rev [0,1] ys" has a finite search space (in Curry where
"++" is evaluated by narrowing). However, if "++" is evaluated by
residuation, then the search space is infinite (the second rule
can be infinitely many often applied where the unsatisfiability
of the accumulated constraints is not detected since all calls
to "++" are delayed due to residuation).
Best regards,
Michael
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mo Mai 30 2011 - 05:23:30 CEST