Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
Has anyone formalized, in a proof assistant (constructively!) the correctness of the computation of Levenshtein distance ? The related Q&A on here is about paper proofs. Searching around did not come up with any leads.
Note that I'm equally interested in correctness as that of a proof of optimality, i.e. knowing that an algorithm returns a correct sequence of edits, from which the distance is trivially computed, is quite interesting too. That the sequence is optimal can be a second step.
As pointed out in a comment above, the answer is yes, in Lean. See the paper and the code as linked into comments.
I was rather hoping Agda or Idris... but perhaps the Lean formalization is actually constructive.
