residuation for compositional search?

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Tue, 24 May 2011 16:49:31 +0200

Hello,

assume I want to write a function that nondeterministically yields a
partition of its input list where a partition of a list `l` is defined as a
list `p` that satisfies the following properties:

    concat p = l
    all (not . null) p = True

If I define this in Curry either as

    partition l | concat p =:= l & all (not . null) p =:= True = p
      where p free

or as

    partition l | all (not . null) p =:= True & concat p =:= l = p
      where p free

then `partition` fails to terminate at least when querying for all
solutions.

I get a terminating version, if I define my own variant of `concat` that
ensures that all concatenated lists are non-empty:

    concatNE [] = []
    concatNE (l:ls) | not (null l) = l ++ concatNE ls

Now,

    partition l | concatNE p =:= l = p
      where p free

succeeds to enumerate all solutions but only at the cost of hampering
modularity: I could not reuse `concat`.

The last solution interleaves the constraints differently. Is it possible to
achieve the same in a modular way, for example, by cleverly using
residuation?

Best regards,
Sebastian

P.S. Maybe a fair search strategy like breadth first search would also help
here. However, there are only finitely many solutions and, therefore, I'd
prefer to be able to write the program such that it terminates regardless of
the search strategy.



_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Tue May 24 2011 - 17:30:47 CEST

This archive was generated by hypermail 2.3.0 : Mon Nov 18 2019 - 07:15:08 CET