Longest common subsequence

DefinitionLongest common subsequence by dynamic programming#✓fully proved

Given lists \(x = x_1 \cdots x_m\) and \(y = y_1 \cdots y_n\) over a type with a boolean equality test, fill a table \(c_{i,j}\) for \(0 \le i \le m\) and \(0 \le j \le n\) by \(c_{i,0} = c_{0,j} = 0\), by \(c_{i,j} = c_{i-1,j-1} + 1\) when the test reports \(x_i = y_j\), and by \(c_{i,j} = \max(c_{i-1,j}, c_{i,j-1})\) otherwise. Then build a witness \(w\) by walking back from \((m, n)\) until \(i = 0\) or \(j = 0\): when the test reports \(x_i = y_j\), put \(x_i\) in front of \(w\) and move to \((i-1, j-1)\); otherwise move to \((i-1, j)\) if \(c_{i-1,j} \ge c_{i,j-1}\) and to \((i, j-1)\) if not. The algorithm returns the pair \((c_{m,n}, w)\).

The abstract time counts one step for each table entry \(c_{i,j}\) with \(i, j \ge 1\) and one for each backward step taken from a position with \(i, j \ge 1\); everything else is free.

Cslib.Algorithms.Lean.longestCommonSubsequence · 62 lines

def longestCommonSubsequence {α : Type u} [BEq α] (xs ys : List α) :
    TimeM Nat (Nat × List α) :=
  let Row (n : Nat) : Type u :=
    ULift.{u} (Subtype (fun row : Array Nat => row.size = n + 1))
  let rec @[reducible] buildRow (x : α) (ys : Array α) (up : Row ys.size) :
      (j : Nat) → j ≤ ys.size → TimeM Nat (Row j)
    | 0, _ => pure ⟨⟨#[0], by simp⟩⟩
    | j + 1, hj => do
      let row ← buildRow x ys up j (by omega)
      TimeM.tick 1
      let value := if x == ys[j] then
        up.down.1[j]'(by rw [up.down.2]; omega) + 1
      else
        max (up.down.1[j + 1]'(by rw [up.down.2]; omega))
          (row.down.1[j]'(by rw [row.down.2]; omega))
      pure ⟨⟨row.down.1.push value, by simp [row.down.2]⟩⟩
  let Table (m n : Nat) : Type u :=
    ULift.{u} (Subtype (fun data : Array (Array Nat) =>
      data.size = m + 1 ∧ ∀ i (hi : i < data.size), data[i].size = n + 1))
  let cell {m n : Nat} (table : Table m n) (i j : Nat)
      (hi : i ≤ m) (hj : j ≤ n) : Nat :=
    (table.down.1[i]'(by rw [table.down.2.1]; omega))[j]'(by
      rw [table.down.2.2]; omega)
  let rec @[reducible] buildTable (xs ys : Array α) :
      (i : Nat) → i ≤ xs.size → TimeM Nat (Table i ys.size)
    | 0, _ => pure
      ⟨⟨#[Array.replicate (ys.size + 1) 0], by simp,
          by
            intro i hi
            have : i = 0 := by simpa using hi
            subst i
            simp⟩⟩
    | i + 1, hi => do
      let table ← buildTable xs ys i (by omega)
      let up : Row ys.size :=
        ⟨⟨table.down.1[i]'(by rw [table.down.2.1]; omega),
          table.down.2.2 i (by rw [table.down.2.1]; omega)⟩⟩
      let row ← buildRow (xs[i]'(by omega)) ys up ys.size (by omega)
      pure ⟨⟨table.down.1.push row.down.1, by simp [table.down.2.1], by
          intro k hk
          rw [Array.getElem_push]
          split
          · exact table.down.2.2 _ _
          · exact row.down.2⟩⟩
  let rec @[reducible] reconstruct (xs ys : Array α) (table : Table xs.size ys.size) :
      (i j : Nat) → i ≤ xs.size → j ≤ ys.size → List α → TimeM Nat (List α)
    | 0, _, _, _, acc => pure acc
    | _, 0, _, _, acc => pure acc
    | i + 1, j + 1, hi, hj, acc => do
      TimeM.tick 1
      if xs[i] == ys[j] then
        reconstruct xs ys table i j (by omega) (by omega) (xs[i] :: acc)
      else if cell table i (j + 1) (by omega) hj ≥ cell table (i + 1) j hi (by omega) then
        reconstruct xs ys table i (j + 1) (by omega) hj acc
      else
        reconstruct xs ys table (i + 1) j hi (by omega) acc
  termination_by i j _ _ _ => i + j
  do
    let table ← buildTable xs.toArray ys.toArray xs.toArray.size (by omega)
    let witness ← reconstruct xs.toArray ys.toArray table xs.toArray.size ys.toArray.size
      (by omega) (by omega) []
    pure (cell table xs.toArray.size ys.toArray.size (by omega) (by omega), witness)

Used by 4

Used byLength of a longest common subsequence · The LCS length is the maximum common-subsequence length · Correctness of the longest common subsequence algorithm · Running time of the longest common subsequence algorithm

TheoremCorrectness of the longest common subsequence algorithm#✓fully proved

Let \(\alpha\) be a type whose boolean equality test agrees with equality, let \(x\) and \(y\) be lists over \(\alpha\), and let \((k, w)\) be the pair returned by the dynamic-programming longest common subsequence algorithm on \(x\) and \(y\). Then \(w\) has length \(k\), \(w\) is a subsequence (not necessarily contiguous) of both \(x\) and \(y\), and every common subsequence of \(x\) and \(y\) has length at most the length of \(w\).

theorem longestCommonSubsequence_correct {α : Type u} [BEq α] [LawfulBEq α]
    (xs ys : List α) :
    let result := (longestCommonSubsequence xs ys).ret
    result.2.length = result.1 ∧ result.2 <+ xs ∧ result.2 <+ ys ∧
      (∀ zs, zs <+ xs → zs <+ ys → zs.length ≤ result.2.length)

Uses 1 · Used by 1

Statement usesLongest common subsequence by dynamic programming

Used byThe LCS length is the maximum common-subsequence length

TheoremRunning time of the longest common subsequence algorithm#✓fully proved

For lists \(x\) and \(y\) of lengths \(m\) and \(n\) over a type with a boolean equality test, the abstract time of the dynamic-programming longest common subsequence algorithm on \(x\) and \(y\) (its number of table and reconstruction transitions) is at most \(mn + (m + n)\).

theorem longestCommonSubsequence_time {α : Type u} [BEq α] (xs ys : List α) :
    (longestCommonSubsequence xs ys).time ≤ xs.length * ys.length + (xs.length + ys.length)

Uses 1

Statement usesLongest common subsequence by dynamic programming

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.