residuation for compositional search?

From: Sebastian Fischer <>
Date: Tue, 24 May 2011 16:49:31 +0200


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

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


    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

Best regards,

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
Received on Di Mai 24 2011 - 17:30:47 CEST

This archive was generated by hypermail 2.3.0 : Mi Aug 05 2020 - 07:15:04 CEST