Finish indexing paper & demonstration haskell

2 files changed, 135 insertions, 2 deletions

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
+
+<!--
+
+> pPrint :: PreferenceTable -> IO ()
+> pPrint = putStr . unlines . map (\(k, prefs) -> show k ++ ": " ++ unwords (map show prefs)) . Map.toList
+>
+> stepPhase1 :: PreferenceTable -> IO (Maybe PreferenceTable)
+> stepPhase1 = phase1Iter Set.empty
+>   where
+>     phase1Iter :: Set Person -> PreferenceTable -> IO (Maybe PreferenceTable)
+>     -- ^ Call `phase1'` until no person is free
+>     phase1Iter engaged table = do
+>         let r = phase1' engaged table
+>         case r of
+>             Just (engaged', table') -> do
+>                 when (table' /= table) $ do
+>                     pPrint table'
+>                     () <$ getLine
+>                 if engaged' == Map.keysSet table'
+>                     then return (Just table')
+>                     else phase1Iter engaged' table'
+>             Nothing -> return Nothing
+
+
+-->
+
+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