diff --git a/thys/Gale_Shapley/document/root.tex b/thys/Gale_Shapley/document/root.tex --- a/thys/Gale_Shapley/document/root.tex +++ b/thys/Gale_Shapley/document/root.tex @@ -1,59 +1,59 @@ \documentclass[11pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage{isabelle,isabellesym} \usepackage{amssymb} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Gale-Shapley Algorithm} -\author{Tobias Nipkow} +\author{Tobias Nipkow\\Department of Informatics\\Technical University of Munich} \maketitle \begin{abstract} This is a stepwise refinement and proof of the Gale-Shapley stable matching (or marriage) algorithm down to executable code. Both a purely functional implementation based on lists and a functional implementation based on efficient arrays (provided by the Collections entry in the AFP) are developed. The latter implementation runs in time $O(n^2)$ where $n$ is the cardinality of the two sets to be matched. \end{abstract} \section{Introduction} The Gale-Shapley algorithm \cite{GaleS62,GusfieldI89} for stable matchings (or marriages) matches two sets of the same cardinality $n$, where each element has a complete list of preferences (a linear order) of the elements of the other set. The refinement process is carried out largely on the level of a simple imperative language. In every refinement step the whole algorithm is stated and proved. Most of the proof is abstrtacted into general lemmas that are used in multiple proofs. Except for one bigger step, each algorithm proof is obtained from the previous one by incremental changes. In the end, two executable functional algorithms are obtained: a purely functional one based on lists and a functional one based on a persistent imperative implementation of arrays (provided by the AFP entry Collections Framework \cite{Collections-AFP} based on \cite{Baker91} (see also \cite{ConchonF07})). The latter algorithm has linear complexity, i.e. $O(n^2)$. We prove that each of the algorithm computes a stable matching that is optimal for one of the two sets. \newpage % include generated text of all theories \input{session} \bibliographystyle{abbrv} \bibliography{root} \end{document}