Hostname: page-component-74656f9884-8rzl6 Total loading time: 0 Render date: 2026-11-06T08:15:49.773Z Has data issue: false hasContentIssue false
  • English
  • Français

A greedy algorithm for dropping digits

Part of: JFP Functional Pearls

Published online by Cambridge University Press:  04 November 2021

RICHARD BIRD Open the ORCID record for RICHARD BIRD [Opens in a new window]  and
SHIN-CHENG MU Open the ORCID record for SHIN-CHENG MU [Opens in a new window]
RICHARD BIRD
Affiliation:
Department of Computer Science, University of Oxford, Oxford OX1 3QD, UK (e-mail: richard.bird@cs.ox.ac.uk)
SHIN-CHENG MU
Affiliation:
Institute of Information Science, Academia Sinica, Taipei, Taiwan (e-mail: scm@iis.sinica.edu.tw)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

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.

Information

Type
Functional Pearl
Information
Journal of Functional Programming , Volume 31 , 2021 , e29
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Bird, R. S. & de Moor, O. (1997) Algebra of Programming . International Series in Computer Science. Prentice Hall.Google Scholar
Cormen, T. H., Leiserson, C. E., Rivest, R. L. & Stein, C. (2001) Introduction to Algorithms. MIT.Google Scholar
Curtis, S. (2003) The classification of greedy algorithms. Sci. Comput. Program. 49(1–3), 125–157.CrossRefGoogle Scholar
Dijkstra, E. W. (1974) Programming as a discipline of mathematical nature. Am. Math. Monthly 81(6), 608–612. EWD 361.CrossRefGoogle Scholar
Korte, B., Lovász, L. & Schrader, R. (1991) Greedoids. Springer-Verlag.CrossRefGoogle Scholar
Lawler, E. L. (1976) Combinatorial Optimization: Networks and Matroids. Holt, Rinehart, and Winston.Google Scholar
LeetCode. (2016) 402. Remove k digits. https://leetcode.com/problems/remove-k-digits/.Google Scholar
Norell, U. (2008) Dependently typed programming in Agda. In Advanced Functional Programming, Koopman, P., Plasmeijer, R. & Swierstra, S. D. (eds). Springer, pp. 230–266.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.