examples/edit_distance.mlw

   1
   2 (* Correctness of a program computing the minimal distance between
   3    two words (code by Claude Marché).
   4
   5    This program computes a variant of the Levenshtein distance. Given
   6    two strings [w1] and [w2] of respective lengths [n1] and [n2], it
   7    computes the minimal numbers of insertions and deletions to
   8    perform in one of the strings to get the other one.  (The
   9    traditional edit distance also includes substitutions.)
  10
  11    The nice point about this algorithm, due to Claude Marché, is to
  12    work in linear space, in an array of min(n1,n2) integers. Time
  13    complexity is O(n1 * n2), as usual.
  14 *)
  15
  16 theory Word
  17
  18   use export int.Int
  19   use export int.MinMax
  20   use export list.List
  21   use export list.Length
  22
  23   type char
  24
  25   val eq (c1 c2:char) : bool
  26     ensures { result <-> c1 = c2 }
  27
  28   type word = list char
  29
  30   inductive dist word word int =
  31   | dist_eps :
  32       dist Nil Nil 0
  33   | dist_add_left :
  34       forall w1 w2: word, n: int.
  35       dist w1 w2 n -> forall a: char. dist (Cons a w1) w2 (n + 1)
  36   | dist_add_right :
  37       forall w1 w2: word, n: int.
  38       dist w1 w2 n -> forall a: char. dist w1 (Cons a w2) (n + 1)
  39   | dist_context :
  40       forall w1 w2:word, n: int.
  41       dist w1 w2 n -> forall a: char. dist (Cons a w1) (Cons a w2) n
  42
  43   predicate min_dist (w1 w2: word) (n: int) =
  44     dist w1 w2 n /\ forall m: int. dist w1 w2 m -> n <= m
  45
  46   (* intermediate lemmas *)
  47
  48   use export list.Append
  49
  50   function last_char (a: char) (u: word) : char = match u with
  51     | Nil -> a
  52     | Cons c u' -> last_char c u'
  53   end
  54
  55   function but_last (a: char) (u: word) : word = match u with
  56     | Nil -> Nil
  57     | Cons c u' -> Cons a (but_last c u')
  58   end
  59
  60   lemma first_last_explicit:
  61     forall u: word, a: char.
  62     but_last a u ++ Cons (last_char a u) Nil = Cons a u
  63
  64   lemma first_last:
  65      forall a: char, u: word. exists v: word, b: char.
  66      v ++ Cons b Nil = Cons a u /\ length v = length u
  67
  68   lemma key_lemma_right:
  69     forall w1 w'2: word, m: int, a: char.
  70     dist w1 w'2 m ->
  71     forall w2: word. w'2 = Cons a w2 ->
  72     exists u1 v1: word, k: int.
  73     w1 = u1 ++ v1 /\ dist v1 w2 k /\ k + length u1 <= m + 1
  74
  75   lemma dist_symetry:
  76     forall w1 w2: word, n: int. dist w1 w2 n -> dist w2 w1 n
  77
  78   lemma key_lemma_left:
  79     forall w1 w2: word, m: int, a: char.
  80     dist (Cons a w1) w2 m ->
  81     exists u2 v2: word, k: int.
  82     w2 = u2 ++ v2 /\ dist w1 v2 k /\ k + length u2 <= m + 1
  83
  84   lemma dist_concat_left:
  85     forall u v w: word, n: int.
  86     dist v w n -> dist (u ++ v) w (length u + n)
  87
  88   lemma dist_concat_right:
  89     forall u v w: word, n: int.
  90     dist v w n -> dist v (u ++ w) (length u + n)
  91
  92   (* main lemmas *)
  93
  94   lemma min_dist_equal:
  95     forall w1 w2: word, a: char, n: int.
  96      min_dist w1 w2 n -> min_dist (Cons a w1) (Cons a w2) n
  97
  98   lemma min_dist_diff:
  99     forall w1 w2: word, a b: char, m p: int.
 100     a <> b ->
 101     min_dist (Cons a w1) w2 p ->
 102     min_dist w1 (Cons b w2) m ->
 103     min_dist (Cons a w1) (Cons b w2) (min m p + 1)
 104
 105   lemma min_dist_eps:
 106     forall w: word, a: char, n: int.
 107     min_dist w Nil n -> min_dist (Cons a w) Nil (n + 1)
 108
 109   lemma min_dist_eps_length:
 110     forall w: word. min_dist Nil w (length w)
 111
 112 end
 113
 114 module EditDistance
 115
 116   use Word
 117   use list.Length as L
 118   use ref.Ref
 119   use array.Array
 120
 121   (* Auxiliary definitions for the program and its specification. *)
 122
 123   function suffix (a: array char) (i: int) : word
 124
 125   axiom suffix_nil:
 126     forall a: array char. suffix a a.length = Nil
 127
 128   axiom suffix_cons:
 129     forall a: array char, i: int.
 130     0 <= i < a.length -> suffix a i = Cons a[i] (suffix a (i+1))
 131
 132   lemma suffix_length:
 133     forall a: array char, i: int.
 134     0 <= i <= a.length -> L.length (suffix a i) = (a.length - i)
 135
 136   predicate min_suffix (a1 a2: array char) (i j n: int) =
 137     min_dist (suffix a1 i) (suffix a2 j) n
 138
 139   function word_of (a: array char) : word = suffix a 0
 140
 141   (* The program. *)
 142
 143   let distance (w1: array char) (w2: array char)
 144     ensures  { min_dist (word_of w1) (word_of w2) result }
 145   = let n1 = length w1 in
 146     let n2 = length w2 in
 147     let t = Array.make (n2+1) 0 in
 148     (* initialization of t *)
 149     for i = 0 to n2 do
 150       invariant { forall j:int. 0 <= j < i -> t[j] = n2 - j }
 151       t[i] <- n2 - i
 152     done;
 153     (* loop over w1 *)
 154     for i = n1 - 1 downto 0 do
 155       invariant { forall j:int. 0 <= j <= n2 -> min_suffix w1 w2 (i+1) j t[j] }
 156       let oldt = ref t[n2] in
 157       t[n2] <- t[n2] + 1;
 158       (* loop over w2 *)
 159       for j = n2 - 1 downto 0 do
 160         invariant { forall k:int. j < k <= n2 -> min_suffix w1 w2 i k t[k] }
 161         invariant { forall k:int. 0 <= k <= j -> min_suffix w1 w2 (i+1) k t[k] }
 162         invariant { min_suffix w1 w2 (i+1) (j+1) !oldt }
 163         let temp = !oldt in
 164         oldt := t[j];
 165         if eq w1[i] w2[j] then
 166           t[j] <- temp
 167         else
 168           t[j] <- (min t[j] t[j + 1]) + 1
 169       done
 170     done;
 171     t[0]
 172
 173 end