# A Greedy Algorithm for Dropping Digits

*Richard S. Bird and Shin−Cheng Mu*

### 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.

Journal

Journal of Functional Programming

Pages

e29

Volume

31

Year

2021