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
$\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$ Feb 16 at 12:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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