Article contents
A greedy algorithm for dropping digits
Published online by Cambridge University Press: 04 November 2021
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.
- Type
- Functional Pearl
- Information
- Copyright
- © The Author(s), 2021. Published by Cambridge University Press
References
- 1
- Cited by
Discussions
No Discussions have been published for this article.