From 8b5c35e41c5ea7fceec83a5134708ae02bcba395 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Sat, 6 May 2017 17:10:02 +0200 Subject: Finish indexing paper & demonstration haskell --- ss2017/stable_marriage_problem/ausarbeitung.lhs | 127 ++++++++++++++++++++++++ ss2017/stable_marriage_problem/structure.md | 10 +- 2 files changed, 135 insertions(+), 2 deletions(-) create mode 100644 ss2017/stable_marriage_problem/ausarbeitung.lhs (limited to 'ss2017') diff --git a/ss2017/stable_marriage_problem/ausarbeitung.lhs b/ss2017/stable_marriage_problem/ausarbeitung.lhs new file mode 100644 index 0000000..ca03280 --- /dev/null +++ b/ss2017/stable_marriage_problem/ausarbeitung.lhs @@ -0,0 +1,127 @@ +Preliminaries +============= + + - Efficient finite maps + +> import Data.Map (Map, (!)) +> import qualified Data.Map as Map + + - Efficient finite sets + +> import Data.Set (Set) +> import qualified Data.Set as Set + + - Some convenience functions for manipulating lists and endomorphisms + +> import Control.Monad (guard, when) +> import Data.Monoid (Endo(..)) + + - An arbitrary representation of a person + +> type Person = Integer + +Utilities +--------- + +> (&!) :: a -> [a -> a] -> a +> -- ^ Reverse application of a list of endomorphisms +> x &! fs = foldMap Endo fs `appEndo` x +> +> infix 3 ==> +> -- | Logical implication +> (==>) :: Bool -> Bool -> Bool +> False ==> _ = True +> True ==> True = True +> True ==> False = False + + + +Definitions +=========== + +\begin{def*} +A \emph{preference table} is a finite set of persons, each associated with a list of other persons, ordered by preference. +\end{def*} + +> type PreferenceTable = Map Person [Person] + +\begin{def*} +We call a pair ${a, b}$ \emph{embedded} in a preference table if $a$ occurs in $b$s preference list and vice versa. +\end{def*} + +Deleting a pair from a table means removing each from the others preference list: + +> delPair :: (Person, Person) -> (PreferenceTable -> PreferenceTable) +> delPair (p1, p2) = Map.mapWithKey delPair' +> where +> delPair' k v = do +> z <- v +> guard $ k == p1 ==> z /= p2 +> guard $ k == p2 ==> z /= p1 +> return z + +\begin{def*} +An ordered pair $(a, b)$ is said to be \emph{semiengaged} if $a$ occurs last in $b$s preference table and $b$ occurs first in $a$s. + +This means that, while $b$ is $a$s best choice of partner, $a$ has no worse choice in partner than $a$ +\end{def*} + +> semiEngaged :: (Person, Person) -> PreferenceTable -> Bool +> -- ^ `semiEngaged (x, y)`; is `x` last in `y`s preference list? +> semiEngaged (x, y) table = x == (last $ table ! y) + +Phase 1 +======= + +> phase1' :: Set Person -> PreferenceTable -> Maybe (Set Person, PreferenceTable) +> phase1' engaged table +> | any null (Map.elems table) +> = Nothing -- If a preference list became empty: fail +> | Set.null free +> = Just (engaged, table) -- If nobody is free, we have nobody left to engage +> | otherwise +> = let x = Set.findMin free -- Arbitrary choice of free person +> y = head $ table ! x -- Best choice of engagement for x +> adjTable = [ delPair (x', y) | x' <- dropWhile (/= x) (table ! y), x' /= x ] +> -- ^ For all worse (than x) choices x' for y; drop them from y's preference list +> adjEngaged = [ Set.insert x -- x is now engaged +> ] ++ [ Set.delete z | z <- Map.keys table, semiEngaged (z, y) table, z /= x ] -- Nobody else is engaged to y +> in Just (engaged &! adjEngaged, table &! adjTable) +> where +> free = Map.keysSet table `Set.difference` engaged + +The algorithm is iterated until all participants are engaged + +> phase1 :: PreferenceTable -> Maybe PreferenceTable +> phase1 = phase1Iter Set.empty +> where +> phase1Iter :: Set Person -> PreferenceTable -> Maybe PreferenceTable +> -- ^ Call `phase1'` until no person is free +> phase1Iter engaged table = do +> (engaged', table') <- phase1' engaged table +> if engaged' == Map.keysSet table' +> then return table' +> else phase1Iter engaged' table' diff --git a/ss2017/stable_marriage_problem/structure.md b/ss2017/stable_marriage_problem/structure.md index 89f467c..fa9ac96 100644 --- a/ss2017/stable_marriage_problem/structure.md +++ b/ss2017/stable_marriage_problem/structure.md @@ -7,10 +7,12 @@ - Definition: Tables, embedded tables, embedded pairs, embedded matchings - Definition: stable tables - Matchings embedded in stable tables are stable (4.2.4 ii) - - (Stable tables are determined by all first OR all last entries (4.2.4 iii)) + - Stable tables are determined by all first OR all last entries (4.2.4 iii) - No pair absent from a stable table can block any of it's embedded matchings (4.2.4 i) # Phase 1 + - Removal of pairs from tables + - Engagement - Present algorithm and demonstrate - Phase 1 has no effect on the embeddedness of stable pairs (4.2.3 i) - Phase 1 stabilizes a table, when it doesn't fail (4.2.2 + 4.2.3 ii) @@ -18,7 +20,8 @@ # Rotations - Definition: rotation, exposure of rotations in stable tables - - Rotations exposed in a stable T are either identical or disjunct (4.2.5) + - Directed graphs & tails + - (Rotations exposed in a stable T are either identical or disjunct (4.2.5)) # Phase 2 - Stable tables that are not already matchings expose at least one rotation and how to find it (4.2.6) @@ -26,4 +29,7 @@ - ignores non-elements of rotation (4.2.7 iii) - results in table consistent with rotation (4.2.7 i, ii) - Thus: produce stable subtables (4.2.8) + - Subtables that don't agree with an exposed rotation have at least that rotation removed entirely (4.2.9) + - Any subtable can be created by removing a series of exposed rotations (Cor 4.2.2) + - Removal of rotations preserve matchings (Thm 4.2.1) - Present derived algorithm and demonstrate -- cgit v1.2.3