We describe a formal correctness proof of RANKING, an online algorithm for online bipartite matching. An outcome of our formalisation is that it shows that there is a gap in all combinatorial proofs of the algorithm. Filling that gap constituted the majority of the effort which went into this work. This is despite the algorithm being one of the most studied algorithms and a central result in theoretical computer science. This gap is an example of difficulties in formalising graphical arguments which are ubiquitous in the theory of computing.
翻译:我们描述了RANKING的正式正确性证明,这是在线双方匹配的在线算法。我们正式化的一个结果是,它显示算法的所有组合证据都存在差距。填补这一差距构成了这项工作的大部分努力。尽管算法是最经过研究的算法之一,也是理论计算机科学的核心结果。这个差距是难以正式化计算理论中普遍存在的图形参数的一个实例。</s>