A greedy algorithm for dropping digits

Richard Bird and Shin-Cheng Mu. To appear in Journal of Functional Programming.

Consider the puzzle: given a number, remove k digits such that the resulting number is as large as possible. Various techniques were employed to derive a linear-time solution to the puzzle: predicate logic was used to justify the structure of a greedy algorithm, a dependently-typed proof assistant was used to give a constructive proof of the greedy condition, and equational reasoning was used to calculate the greedy step as well as the final, linear-time optimisation.

[arXiv:2101.09700|Haskell Code|Agda Proofs]

Leave a Comment

Your email address will not be published. Required fields are marked *