Nussinov algorithm for RNA secondary structure

StructureRNA secondary structure#✓fully proved

A secondary structure on s (Nussinov et al. 1978): a finite set of base pairs (i, j), each closing a hairpin with at least m unpaired positions strictly inside (i + m < j), joining complementary bases (pair s[i] s[j], which also puts both positions inside s), with every position in at most one pair and no two pairs crossing (i < k < j < l).

structure IsStructure {B : Type*} (pair : B → B → Prop) (m : ℕ) (s : List B)
    (P : Finset (ℕ × ℕ)) : Prop where
  /-- Each pair encloses at least `m` positions: `i + m < j`. -/
  loop : ∀ p ∈ P, p.1 + m < p.2
  /-- Both positions of a pair lie in `s` and carry complementary bases. -/
  compl : ∀ p ∈ P, ∃ a b, s[p.1]? = some a ∧ s[p.2]? = some b ∧ pair a b
  /-- Distinct pairs share no position. -/
  disjoint : ∀ p ∈ P, ∀ q ∈ P, p ≠ q →
    p.1 ≠ q.1 ∧ p.1 ≠ q.2 ∧ p.2 ≠ q.1 ∧ p.2 ≠ q.2
  /-- No two pairs cross. -/
  noncrossing : ∀ p ∈ P, ∀ q ∈ P, ¬ (p.1 < q.1 ∧ q.1 < p.2 ∧ p.2 < q.2)

Used by 13

Used byInside algorithm · Tropical semiring · Membership in the set of secondary structures · Total structure weight is at least one · Outside algorithm · Secondary structures within an interval · Each base pairs at most once · Soundness bound · Optimality · Unique loop decomposition · Every position has a unique innermost strict container · Zuker's algorithm · Minimum free energy is at most zero

DefinitionMaximum of a list of natural numbers#✓fully proved

The largest of a list of naturals (0 for the empty list).

def listMax (l : List ℕ) : ℕ := l.foldr max 0

Used by 3

Used bySoundness bound · Optimality · The Nussinov recursion

DefinitionThe Nussinov recursion#✓fully proved

The first base a of a :: rest is either unpaired, or paired with rest[k] for some k ≥ m with pair a rest[k], splitting the rest into the enclosed part rest.take k and the outer part rest.drop (k + 1). Exponential-time specification; the usual O(n³) table memoizes it on the intervals of s.

def nussinov {B : Type*} (pair : B → B → Prop) [DecidableRel pair] (m : ℕ) : List B → ℕ
  | [] => 0
  | a :: rest =>
      max (nussinov pair m rest)
        (listMax ((List.finRange rest.length).map fun k =>
          if m ≤ k.val ∧ pair a rest[k] then
            1 + nussinov pair m (rest.take k.val) + nussinov pair m (rest.drop (k.val + 1))
          else 0))
  termination_by l => l.length
  decreasing_by
    all_goals simp only [List.length_cons, List.length_take, List.length_drop]
    all_goals omega

Uses 1 · Used by 3

Statement usesMaximum of a list of natural numbers

Used byTropical semiring · Soundness bound · Optimality

TheoremSoundness bound#✓fully proved

Every secondary structure has at most nussinov pair m s pairs.

theorem card_le_nussinov {B : Type*} (pair : B → B → Prop) [DecidableRel pair] (m : ℕ)
    (s : List B) (P : Finset (ℕ × ℕ)) (hP : IsStructure pair m s P) :
    P.card ≤ nussinov pair m s

Uses 3 · Used by 1

Statement usesRNA secondary structure · The Nussinov recursion

Proof usesMaximum of a list of natural numbers

Used byTropical semiring

TheoremOptimality#✓fully proved

Some secondary structure has exactly nussinov pair m s pairs, so the recursion computes the maximum number of pairs over all non-crossing structures.

theorem exists_isStructure_card_eq {B : Type*} (pair : B → B → Prop) [DecidableRel pair]
    (m : ℕ) (s : List B) :
    ∃ P : Finset (ℕ × ℕ), IsStructure pair m s P ∧ P.card = nussinov pair m s

Uses 3 · Used by 1

Statement usesRNA secondary structure · The Nussinov recursion

Proof usesMaximum of a list of natural numbers

Used byTropical semiring

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.