一句话：通过谓词逻辑、依赖类型证明助手和等式推理，系统推导出删除 k 位数字使结果最大的线性时间贪心算法。
论文研究一个经典谜题：给定一个十进制数，删除 k 个数字，使剩余数字按原序组成的新数尽可能大。作者采用程序计算与证明相结合的方法：先用谓词逻辑论证贪心算法的整体结构，说明为何逐步删除局部最差数字可得到全局最优；再在依赖类型证明助手中构造性地证明贪心条件成立；最后通过等式推理推导出单步贪心操作，并将算法优化为线性时间。该工作展示了如何从逻辑规约与构造性证明出发，严谨地推导出高效贪心算法，而无需依赖非形式化论证。
Abstract Consider the following puzzle: given a number, remove k digits such that the resulting number is as large as possible. Various techniques are employed to derive a linear-time solution to the puzzle: we justify the structure of a greedy algorithm by predicate logic, give a constructive proof of the greedy condition using a dependently typed proof assistant and calculate the greedy step as well as the final, linear-time optimisation by equational reasoning.
DOI 原文 ·
@article{paperbot1225,
title = {A greedy algorithm for dropping digits},
author = {RICHARD BIRD and SHIN-CHENG MU},
journal = {Journal of Functional Programming},
volume = {31},
year = {2021},
doi = {10.1017/s0956796821000198}
}