We present an ongoing effort to build a framework and a library in Isabelle/HOL for formalising primal-dual arguments for the analysis of algorithms. We discuss a number of example formalisations from the theory of matching algorithms, covering classical algorithms like the Hungarian Method, widely considered the first primal-dual algorithm, and modern algorithms like the Adwords algorithm, which models the assignment of search queries to advertisers in the context of search engines.

翻译：我们正在推进一项持续性的工作，在Isabelle/HOL中构建一个用于形式化算法分析中原始对偶论证的框架与函数库。本文讨论来自匹配算法理论中的若干形式化实例，涵盖经典算法如匈牙利算法（被广泛认为是首个原始对偶算法），以及现代算法如Adwords算法（该算法在搜索引擎场景中模拟搜索查询与广告商的匹配分配）。