> module FSAlab4
> where 
> import Data.List

> infix 1 --> 
> 
> (-->) :: Bool -> Bool -> Bool
> p --> q = (not p) || q
> 
> forall = flip all

> assert :: (a -> b -> Bool) -> (a -> b) -> a -> b 
> assert p f x = if p x (f x) then f x 
>                 else error "assert"

> invar :: (a -> Bool) -> (a -> a) -> a -> a
> invar p = assert (\ x y -> p x --> p y)

This set of exercises deals with algorithms for matching. The matching problem is the problem of connecting nodes in a bipartite graph, while making sure that certain requirements are met.

Suppose equal sets of men and women are given, each man has listed the women in order of preference, and vice versa for the women. A stable marriage match between men and women is a one-to-one mapping between the men and women with the property that if a man prefers another woman over his own wife then that woman does not prefer him to her own husband, and if a woman prefers another man over her own husband, then that man does not prefer her to his own wife.

The computer scientists Gale and Shapley proved that stable matchings always exist, and gave an algorithm for finding such matchings, the so-called Gale-Shapley algorithm (Gale and Shapley 1962). This has many important applications, also outside of the area of marriage counseling. See Stable Marriage Problem for more information.

If we want to write this in functional imperative style, we have to check the number of parameters for the while loop. These are:

It may look like we also need the preference list of the women as a parameter, but this list is not used for stating the exit condition and it is not changed by the step function, and we can keep it outside the loop. So it is possible to phrase the algorithm in terms of while operating on triples.

> while = until . (not.)

> type Man   = Int
> type Woman = Int
> type Mpref = [(Man,[Woman])]
> type Wpref = [(Woman,[Man])]
> type Engaged = [(Woman,Man)]

> mt :: Mpref
> mt = [(1,[2,1,3]), (2, [3,2,1]), (3,[1,3,2])]
> 
> wt :: Wpref
> wt = [(1,[1,2,3]),(2,[3,2,1]), (3,[1,3,2])]

In mt, the entry (1,[2,1,3]) indicates that man \(1\) prefers woman \(2\) over woman \(1\) and woman \(1\) over woman \(3\). We assume that preferences are transitive, so man \(1\) also prefers woman \(2\) over woman \(3\).

Here is an auxiliary function for converting a preference list to a function, which allows us to express w prefers m to m' in a simple way.

> type PrefFct = Int -> Int -> Int -> Bool
> 
> plist2pfct :: [(Int,[Int])] -> PrefFct 
> plist2pfct table x y y' = 
>   let 
>     Just prefs = lookup x table
>   in elem y (takeWhile (/= y') prefs)

Initialisation of the loop: the list of all men is extracted from the table of men's preferences, all men are free, no-one is engaged to start with. Note that map fst mpref gives us the list of all men.

> stableMatch :: (Wpref,Mpref) -> Engaged
> stableMatch (wpref,mpref) = 
>   let 
>      men     = map fst mpref
>      free    = men
>      engaged = []
>      f       = \ (_,_,x) ->  x
>   in
>    f $ stable wpref (mpref,free,engaged)

The test function for the while loop just checks whether the list of free men is exhausted.

The step function for the while loop has an argument of type Mpref for the current list of men's preferences, Engaged for the list of currently engaged \((w,m)\) pairs, and an argument of type [Man] for the list of currently free (not engaged) men. The list of men's preferences changes in the loop step, for each woman that a man proposes to is crossed from his preference list. %This is to ensure that no man proposes to the same woman twice.

> stable ::  Wpref -> (Mpref,[Man],Engaged) -> (Mpref,[Man],Engaged)
> stable wpref = let 
>    wpr = plist2pfct wpref
>  in while (\ (_,free, _) -> not (null free))
>            (\ (mpr, (m:free), engaged)  ->
>             let
>                Just (w:ws) = lookup m mpr
>                match = lookup w engaged
>                mpr' = (m,ws) : (delete (m,w:ws) mpr)
>                (engaged',free') = case match of 
>                    Nothing -> ((w,m):engaged,free)
>                    Just m' -> 
>                      if wpr w m m' then (
>                          (w,m) : (delete (w,m') engaged),
>                           m':free)
>                      else (engaged, m:free)
>             in (mpr',free',engaged'))

The algorithm assumes that there are equal numbers of men and women to start with, and that both men and women have listed all members of the opposite sex in order of preference.

> makeMatch = stableMatch (mt,wt)

This gives \((w,m)\) pairs. So woman \(1\) is married to man \(1\), and so on. Note that the first woman ends up with the man of her preference, but the other two women do not. But this match is still stable, for although the second woman is willing to swap her husband for the third man, she is at the bottom of his list. And so on.

Note that the algorithm is sensitive to the choice of party that does the proposing. The following gives a different stable matching, arguably more favourable to the women.

> makeMatch2 = stableMatch (wt,mt)

To show that this algorithm is correct, we have to show two things: termination and stability of the constructed match.

Show that if there are equal numbers of men and women, the algorithm always terminates. Hint: analyze what happens to the preference lists of the men. Observe that no man proposes to the same woman twice.

To show stability, we have to show that each step through the step function preserves the invariant the set of currently engaged men and women is stable. Prove this.

An alternative to reasoning about the correctness of an algorithm is specification-based testing, which we will explore now.

One of the properties that has to be maintained through the loop step function for stable marriage is:

> freeProp :: (Mpref,[Man],Engaged) -> Bool
> freeProp (mpref, free, engaged) = let 
>     men  = map fst mpref
>     emen = map snd engaged 
>   in forall men (\x -> elem x free == notElem x emen)

The other invariant is the stability property. Here is the definition of stability for a relation \(E\) consisting of engaged \((w,m)\) pairs:

\[ \forall (w,m) \in E \forall (w',m') \in E ((\text{pr}_w m' m \rightarrow \text{pr}_{m'} w' w) \land (\text{pr}_m w' w \rightarrow \text{pr}_{w'} m' m)). \]

What this says (once more) is: if \(w\) prefers another guy \(m'\) to her own fiancee \(m\) then \(m'\) does prefer his own fiancee \(w'\) to \(w\), and if \(m\) prefers another woman \(w'\) to his own fiancee \(w\) then \(w'\) does prefer her own fiancee \(m'\) to \(m\).

Once it is written like this it is straightforward to implement it, for we have all the ingredients:

> isStable :: (Wpref, Mpref) -> Engaged -> Bool
> isStable (wpref, mpref) engaged = let 
>     wf = plist2pfct wpref
>     mf = plist2pfct mpref
>   in 
>     forall engaged (\ (w,m) -> forall engaged 
>           (\ (w',m') -> (wf w m' m --> mf m' w' w)
>                          && 
>                         (mf m w' w --> wf w' m' m)))

> stableMatch' :: (Wpref, Mpref)  -> Engaged
> stableMatch' = assert isStable stableMatch

> mt2 = [(1, [1, 5, 3, 9, 10, 4, 6, 2, 8, 7]),
>        (2, [3, 8, 1, 4, 5, 6, 2, 10, 9, 7]),
>        (3, [8, 5, 1, 4, 2, 6, 9, 7, 3, 10]),
>        (4, [9, 6, 4, 7, 8, 5, 10, 2, 3, 1]), 
>        (5, [10, 4, 2, 3, 6, 5, 1, 9, 8, 7]),
>        (6, [2, 1, 4, 7, 5, 9, 3, 10, 8, 6]),
>        (7, [7, 5, 9, 2, 3, 1, 4, 8, 10, 6]),
>        (8, [1, 5, 8, 6, 9, 3, 10, 2, 7, 4]),
>        (9, [8, 3, 4, 7, 2, 1, 6, 9, 10, 5]), 
>        (10, [1, 6, 10, 7, 5, 2, 4, 3, 9, 8])]

> wt2 =[(1, [2, 6, 10, 7, 9, 1, 4, 5, 3, 8]),
>       (2, [2, 1, 3, 6, 7, 4, 9, 5, 10, 8]),
>       (3, [6, 2, 5, 7, 8, 3, 9, 1, 4, 10]),
>       (4, [6, 10, 3, 1, 9, 8, 7, 4, 2, 5]),
>       (5, [10, 8, 6, 4, 1, 7, 3, 5, 9, 2]),
>       (6, [2, 1, 5, 9, 10, 4, 6, 7, 3, 8]),
>       (7, [10, 7, 8, 6, 2, 1, 3, 5, 4, 9]),
>       (8, [7, 10, 2, 1, 9, 4, 8, 5, 3, 6]),
>       (9, [9, 3, 8, 7, 6, 2, 1, 5, 10, 4]),
>       (10, [5, 8, 7, 1, 2, 10, 3, 9, 6, 4])]

> makeMatch3 = stableMatch' (mt2,wt2)

The task in the stable roommate problem is like that in the stable marriage problem: find a stable matching of \(2n\) students. Unlike the stable marriage case, the set of students is not broken up into male and female. Any person can prefer anyone in the same set.

Look up the algorithm given for this in (Irving 1985) or on wikipedia, implement it, and next develop an assertive version (a version with an assert wrapped around the main function) for it.

Analyze what went wrong in the combined matching and lottery approach to secondary school allocation in Amsterdam, in Spring 2015, and compare with the improved system that was adopted in Spring 2016.

A description of the method of 2015 and an analysis can be found this report (in Dutch) by Pieter Gautier, Monique de Haan, Bas van der Klaauw and Hessel Overbeek. A more scholarly version of this report, in English, was sent to me by Pieter Gautier. See here.

There was great dissatisfaction among pupils and parents about the outcome of the algorithm. Lots of children wanted to swap schools. Since this was not allowed by (the aggregation of school boards) OSVO and the Municipality, some parents took the case to court. The judge ruled in favour of OSVO and the Municipality. Some details are here.

What does the student-proposing Deferred Acceptance algorithm with Multiple Tie-Breaking (DA-MTB) that was used amount to? How does it relate to the algorithms of Gale and Shapley and of Irving? Why did it not lead to stable matchings? What does stability mean in the context of school allocation, anyway?

Because of the widespread dissatisfaction DA-MTB was replaced in 2016 by a single tie-breaking deferred acceptance allocation mechanism (DA-STB). In single tie breaking, one lottery determines the augmentation of each high school’s preference list. Here, augmentation means that the preferences of the schools are partly given by the lottery. What does this system amount to, and how does it compare to DA-MTB?

Can you implement the algorithms that were used, and reproduce the outcomes on suitable data? Next, discuss the differences, and compare the results.

Gale, D., and L. Shapley. 1962. “College Admissions and the Stability of Marriage.” American Mathematical Monthly 69: 9–15.

Irving, Robert W. 1985. “An Efficient Algorithm for the ‘Stable Roommates’ Problem.” Journal of Algorithms 6 (4): 577–95.

FSA Lab Exercises Week 4

Matching Algorithms