A greedy algorithm for dropping digits (Functional Pearl)

TL;DR

This paper presents a formal and constructive approach to deriving a linear-time greedy algorithm for maximizing a number by removing k digits, using predicate logic, dependently-typed proofs, and equational reasoning.

Contribution

It introduces a formal methodology combining logic and proof assistants to derive and justify a greedy algorithm for digit removal optimization.

Findings

The greedy algorithm operates in linear time.

Formal proofs validate the greedy choice property.

Equational reasoning clarifies the algorithm's steps.

Abstract

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.