Module Combinatorial

Author
Sergio Antoy (with extensions by Michael Hanus)
Version
June 2021

A collection of common non-deterministic and/or combinatorial operations. Many operations are intended to operate on sets. The representation of these sets is not hidden; rather sets are represented as lists. Ideally these lists contains no duplicate elements and the order of their elements cannot be observed. In practice, these conditions are not enforced.

Exported Functions:
allSubsetspartitionpermutesizedSubsetsplitSetsubset

Exported Functions

permute :: [a] -> [a]  Non-deterministic 

Compute any permutation of a list.

:: [a]  The list.
-> [a]  A permutation of the argument.
Properties:
permute [1,2,3,4] ~> [1,3,4,2](permute1234)
length (permute xs) <~> length xs(permLength)
anyOf (permute xs) <~> anyOf xs(permElems)

subset :: [a] -> [a]  Non-deterministic 

Compute any sublist of a list. The sublist contains some of the elements of the list in the same order.

:: [a]  The list.
-> [a]  A sublist of the argument.
Properties:
subset [1,2,3,4] ~> [1,3](subset1234)
subset [1,2,3] <~> ([1,2,3] ? ([1,2] ? ([1,3] ? ([1] ? ([2,3] ? ([2] ? ([3] ? [])))))))(subset123)
anyOf (subset xs) <~ anyOf xs(subsetElems)
Further infos:
  • solution complete, i.e., able to compute all solutions

allSubsets :: Ord a => [a] -> [[a]]  Deterministic 

Compute all the sublists of a list.

:: Ord a
=> [a]  The list.
-> [[a]]  All the sublists of the argument.
Properties:
allSubsets [1,2,3] -=- [[],[1],[1,2],[1,2,3],[1,3],[2],[2,3],[3]](allSubsets123)
Further infos:
  • might behave indeterministically

splitSet :: [a] -> ([a], [a])  Non-deterministic 

Split a list into any two sublists.

:: [a]  The list.
-> ([a], [a])  A pair consisting of two complementary sublists of the argument.
Properties:
splitSet [1,2,3,4] ~> ([1,3,4],[2])(splitSet1234)
(\(xs,ys) -> length xs + length ys) (splitSet zs) <~> length zs(splitSetLengths)
(\(xs,ys) -> anyOf xs ? anyOf ys) (splitSet zs) <~> anyOf zs(splitSetElems)
Further infos:
  • solution complete, i.e., able to compute all solutions

sizedSubset :: Int -> [a] -> [a]  Non-deterministic 

Compute any sublist of fixed length of a list. Similar to subset, but the length of the result is fixed.

:: Int  The length of the output sublist.
-> [a]  The input list.
-> [a]  A sublist of xs of length c.
Precondition:
(sizedSubset c _) requires c >= 0(sizedSubset'pre)
Properties:
((c >= 0) && (length xs >= c)) ==> (length (sizedSubset c xs) <~> c)(sizedSubsetLength)
((c >= 0) && (length xs < c)) ==> failing (sizedSubset c xs)(sizedSubsetLengthTooSmall)

partition :: [a] -> [[a]]  Non-deterministic 

Compute any partition of a list. The output is a list of non-empty lists such that their concatenation is a permutation of the input list. No guarantee is made on the order of the arguments in the output.

:: [a]  The input list.
-> [[a]]  A partition of xs represented as a list of lists.
Properties:
partition [1,2,3,4] ~> [[4],[2,3],[1]](partition1234)
partition [1,2,3] <~> ([[1,2,3]] ? ([[2,3],[1]] ? ([[1,3],[2]] ? ([[3],[1,2]] ? [[3],[2],[1]]))))(partition123)
sum (map length (partition xs)) <~> length xs(partitionLengths)
anyOf (map anyOf (partition xs)) <~> anyOf xs(partitionElems)
Further infos:
  • solution complete, i.e., able to compute all solutions