------------------------------------------------------------------------------ --- 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 ------------------------------------------------------------------------------ {-# OPTIONS_FRONTEND -Wno-overlapping -Wno-missing-signatures #-} module Combinatorial ( permute, subset, allSubsets, splitSet, sizedSubset, partition ) where import Data.List ( sum ) import Control.SetFunctions import Test.Prop ------------------------------------------------------------------------------ -- Public Operations ------------------------------------------------------------------------------ --- Compute any permutation of a list. --- --- @param xs - The list. --- @return A permutation of the argument. permute :: [a] -> [a] permute [] = [] permute (x:xs) = ndinsert (permute xs) where ndinsert ys = x : ys ndinsert (y:ys) = y : ndinsert ys -- Properties: permute1234 = permute [1,2,3,4] ~> [1,3,4,2] -- The length of a permutation is identical to the length of the argument: permLength xs = length (permute xs) <~> length xs -- lengths are equal -- The permutation contains the same elements as the argument: permElems xs = anyOf (permute xs) <~> anyOf xs ------------------------------------------------------------------------------ --- Compute any sublist of a list. --- The sublist contains some of the elements of the list in the same order. --- --- @param xs - The list. --- @return A sublist of the argument. subset :: [a] -> [a] subset [] = [] subset (x:xs) = x:subset xs subset (_:xs) = subset xs -- Properties: subset1234 = subset [1,2,3,4] ~> [1,3] subset123 = subset [1,2,3] <~> ([1,2,3]?[1,2]?[1,3]?[1]?[2,3]?[2]?[3]?[]) subsetElems xs = anyOf (subset xs) <~ anyOf xs ------------------------------------------------------------------------------ --- Compute all the sublists of a list. --- --- @param xs - The list. --- @return All the sublists of the argument. allSubsets :: Ord a => [a] -> [[a]] allSubsets xs = sortValues (set1 subset xs) -- Properties: allSubsets123 = allSubsets [1,2,3] -=- [[],[1],[1,2],[1,2,3],[1,3],[2],[2,3],[3]] ------------------------------------------------------------------------------ --- Split a list into any two sublists. --- --- @param xs - The list. --- @return A pair consisting of two complementary sublists of the argument. splitSet :: [a] -> ([a],[a]) splitSet [] = ([],[]) splitSet (x:xs) = let (u,v) = splitSet xs in (x:u,v) ? (u,x:v) -- Properties: splitSet1234 = splitSet [1,2,3,4] ~> ([1,3,4],[2]) -- The sum of the length of the two sublists is the length of the argument list: splitSetLengths zs = (\ (xs,ys) -> length xs + length ys) (splitSet zs) <~> length zs -- The two sublists and the argument list have the same elements: splitSetElems zs = (\ (xs,ys) -> anyOf xs ? anyOf ys) (splitSet zs) <~> anyOf zs ------------------------------------------------------------------------------ --- Compute any sublist of fixed length of a list. --- Similar to 'subset', but the length of the result is fixed. --- --- @param c - The length of the output sublist. --- @param xs - The input list. --- @return A sublist of `xs` of length `c`. sizedSubset :: Int -> [a] -> [a] sizedSubset c l = if c == 0 then [] else aux l where aux (x:xs) = x:sizedSubset (c-1) xs ? sizedSubset c xs -- Precondition: sizedSubset'pre :: Int -> [a] -> Bool sizedSubset'pre c _ = c>=0 -- Properties: sizedSubsetLength c xs = (c>=0 && length xs >= c) ==> length (sizedSubset c xs) <~> c -- No result if the given output length is larger than the length of the input: sizedSubsetLengthTooSmall c xs = (c>=0 && length xs < c) ==> failing (sizedSubset c xs) ------------------------------------------------------------------------------ --- 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. --- --- @param xs - The input list. --- @return A partition of `xs` represented as a list of lists. partition :: [a] -> [[a]] partition [] = [] partition (x:xs) = insert x (partition xs) where insert e [] = [[e]] insert e (y:ys) = ((e:y):ys) ? (y:insert e ys) -- Properties: partition1234 = partition [1,2,3,4] ~> [[4],[2,3],[1]] partition123 = partition [1,2,3] <~> ([[1,2,3]] ? [[2,3],[1]] ? [[1,3],[2]] ? [[3],[1,2]] ? [[3],[2],[1]]) -- The sum of the length of the sublists is the length of the argument list: partitionLengths xs = sum (map length (partition xs)) <~> length xs -- The sublists of the partition and the argument list have the same elements: partitionElems xs = anyOf (map anyOf (partition xs)) <~> anyOf xs -- end module Combinatorial