Module Combinatorial

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.

Author: Sergio Antoy (with extensions by Michael Hanus)

Version: June 2021

Summary of exported operations:

permute :: [a] -> [a]  Non-deterministic 
Compute any permutation of a list.
subset :: [a] -> [a]  Non-deterministic 
Compute any sublist of a list.
allSubsets :: Ord a => [a] -> [[a]]  Non-deterministic 
Compute all the sublists of a list.
splitSet :: [a] -> ([a],[a])  Non-deterministic 
Split a list into any two sublists.
sizedSubset :: Int -> [a] -> [a]  Non-deterministic 
Compute any sublist of fixed length of a list.
partition :: [a] -> [[a]]  Non-deterministic 
Compute any partition of a list.

Exported operations:

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

Compute any permutation of a list.

Example call:
(permute xs)
Parameters:
  • xs : The list.
Returns:
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)

Further infos:
  • solution complete, i.e., able to compute all solutions

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.

Example call:
(subset xs)
Parameters:
  • xs : The list.
Returns:
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]]  Non-deterministic 

Compute all the sublists of a list.

Example call:
(allSubsets xs)
Parameters:
  • xs : The list.
Returns:
All the sublists of the argument.
Properties:

allSubsets [1,2,3] -=- [[],[1],[1,2],[1,2,3],[1,3],[2],[2,3],[3]] (allSubsets123)

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

Split a list into any two sublists.

Example call:
(splitSet xs)
Parameters:
  • xs : The list.
Returns:
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.

Example call:
(sizedSubset c xs)
Parameters:
  • c : The length of the output sublist.
  • xs : The input list.
Returns:
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.

Example call:
(partition xs)
Parameters:
  • xs : The input list.
Returns:
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