A greedy algorithm for dropping digits (Functional Pearl)
Programming Languages
2023-12-01 v1
Abstract
Consider the puzzle: given a number, remove 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.
Cite
@article{arxiv.2101.09700,
title = {A greedy algorithm for dropping digits (Functional Pearl)},
author = {Richard Bird and Shin-Cheng Mu},
journal= {arXiv preprint arXiv:2101.09700},
year = {2023}
}