5
$\begingroup$

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.

$\endgroup$
3

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ I can't imagine they managed to make it non-constructive... $\endgroup$ Commented Feb 16, 2021 at 12:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.