Parikh images and semilinear sets

DefinitionParikh vector of a word#✓fully proved

The Parikh vector of a word: the function counting, for each letter, how many times it occurs in the word.

def parikhVector (w : List T) [DecidableEq T] : T → ℕ :=
  fun a => w.count a
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Used by 6
Used byParikh image of a language · Parikh image of the empty language is empty · Parikh image of a singleton language · Parikh image of a union of languages · Parikh vectors add over concatenation · Parikh vector of the empty word is zero

DefinitionParikh image of a language#✓fully proved

The Parikh image of a language: the set of Parikh vectors of its words.

def parikhImage (L : Language T) [DecidableEq T] : Set (T → ℕ) :=
  (fun w => parikhVector w) '' L
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 1 · Used by 3
Statement usesParikh vector of a word
Used byParikh image of the empty language is empty · Parikh image of a singleton language · Parikh image of a union of languages

TheoremParikh vector of the empty word is zero#✓fully proved

The Parikh vector of the empty word is zero.

theorem parikhVector_nil [DecidableEq T] : parikhVector ([] : List T) = 0
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 1
Statement usesParikh vector of a word

TheoremParikh vectors add over concatenation#✓fully proved

Parikh vectors add over concatenation.

theorem parikhVector_append [DecidableEq T] (u v : List T) :
    parikhVector (u ++ v) = parikhVector u + parikhVector v
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 1
Statement usesParikh vector of a word

TheoremParikh image of a union of languages#✓fully proved

The Parikh image of a union is the union of the Parikh images.

theorem parikhImage_union [DecidableEq T] (L M : Language T) :
    parikhImage (L + M) = parikhImage L ∪ parikhImage M
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 2
Statement usesParikh image of a language
Proof usesParikh vector of a word

TheoremParikh image of the empty language is empty#✓fully proved

The Parikh image of the empty language is empty.

theorem parikhImage_empty [DecidableEq T] :
    parikhImage (0 : Language T) = ∅
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 2
Statement usesParikh image of a language
Proof usesParikh vector of a word

TheoremParikh image of a singleton language#✓fully proved

The Parikh image of a singleton language is the singleton of the Parikh vector.

theorem parikhImage_singleton [DecidableEq T] (w : List T) :
    parikhImage ({w} : Language T) = {parikhVector w}
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 2
Statement usesParikh image of a language · Parikh vector of a word

DefinitionLinear combination of period vectors#✓fully proved

The linear combination of a list of period vectors with a coefficient list c: pair the two lists position by position and sum the scaled periods, and reject mismatched lengths by returning 0 (the length guard is checked up front, before the recursion, so a shorter coefficient list cannot silently truncate and a longer one cannot silently drop coefficients). Coefficients are indexed by position in P, not by period value, so duplicate periods get independent coefficients: for P = [p, p], linComb P [1, 0] = p, not 2 • p.

def linComb (P : List (T → ℕ)) (c : List ℕ) : T → ℕ :=
  if P.length = c.length then linCombAux P c else 0
where
  /-- The unguarded recursion behind `linComb`: pair the two lists
  position by position. Used only behind the length guard in
  `linComb`, so the two lists have equal length here. -/
  linCombAux : List (T → ℕ) → List ℕ → T → ℕ
    | [], _ => 0
    | _, [] => 0
    | p :: P, n :: c => n • p + linCombAux P c
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Used by 6
Used byLinear set of vectors · A singleton set of vectors is linear · Duplicate periods get independent coefficients · Unguarded linear combination agrees on equal lengths · Linear combination with too many coefficients is zero · Linear combination with too few coefficients is zero

TheoremUnguarded linear combination agrees on equal lengths#✓fully proved

The unguarded recursion agrees with linComb on equal-length inputs.

theorem linComb_eq_aux_of_length_eq {P : List (T → ℕ)} {c : List ℕ}
    (h : P.length = c.length) : linComb P c = linComb.linCombAux P c
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 1 · Used by 1
Statement usesLinear combination of period vectors
Used byDuplicate periods get independent coefficients

TheoremLinear combination with too few coefficients is zero#✓fully proved

Mismatched lengths are rejected: a shorter coefficient list does not silently truncate.

theorem linComb_eq_zero_of_length_lt {P : List (T → ℕ)} {c : List ℕ}
    (h : c.length < P.length) : linComb P c = 0
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 1
Statement usesLinear combination of period vectors

TheoremLinear combination with too many coefficients is zero#✓fully proved

Mismatched lengths are rejected: a longer coefficient list does not silently drop coefficients.

theorem linComb_eq_zero_of_length_gt {P : List (T → ℕ)} {c : List ℕ}
    (h : P.length < c.length) : linComb P c = 0
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 1
Statement usesLinear combination of period vectors

TheoremDuplicate periods get independent coefficients#✓fully proved

Duplicate periods get independent coefficients: with P = [p, p], the coefficients (1, 0) give p.

theorem linComb_dup (p : T → ℕ) : linComb [p, p] [1, 0] = p
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 2
Statement usesLinear combination of period vectors
Proof usesUnguarded linear combination agrees on equal lengths

DefinitionLinear set of vectors#✓fully proved

A set of vectors is linear when it consists of a base vector plus arbitrary nonnegative combinations of finitely many period vectors, with one coefficient per position in the period list.

def IsLinear (S : Set (T → ℕ)) : Prop :=
  ∃ (b : T → ℕ) (P : List (T → ℕ)),
    S = {v | ∃ c : List ℕ, c.length = P.length ∧ v = b + linComb P c}
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 1 · Used by 5
Statement usesLinear combination of period vectors
Used byA singleton set of vectors is linear · Semilinear set of vectors · Linear sets are semilinear · The empty set is semilinear · Semilinear sets are closed under union

DefinitionSemilinear set of vectors#✓fully proved

A set of vectors is semilinear when it is a finite union of linear sets.

def IsSemilinear (S : Set (T → ℕ)) : Prop :=
  ∃ (F : Finset (Set (T → ℕ))), (∀ S' ∈ F, IsLinear S') ∧ ⋃₀ F = S
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 1 · Used by 4
Statement usesLinear set of vectors
Used byLinear sets are semilinear · The empty set is semilinear · A singleton set of vectors is semilinear · Semilinear sets are closed under union

TheoremA singleton set of vectors is linear#✓fully proved

A singleton set of vectors is linear, with no periods.

theorem isLinear_singleton (b : T → ℕ) : IsLinear ({b} : Set (T → ℕ))
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 2 · Used by 1
Statement usesLinear set of vectors
Proof usesLinear combination of period vectors
Used byA singleton set of vectors is semilinear

TheoremLinear sets are semilinear#✓fully proved

Linear sets are semilinear.

theorem IsLinear.isSemilinear {S : Set (T → ℕ)} (hS : IsLinear S) :
    IsSemilinear S
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 2 · Used by 1
Statement usesLinear set of vectors · Semilinear set of vectors
Used byA singleton set of vectors is semilinear

TheoremThe empty set is semilinear#✓fully proved

The empty set of vectors is semilinear.

theorem isSemilinear_empty : IsSemilinear (∅ : Set (T → ℕ))
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 2
Statement usesSemilinear set of vectors
Proof usesLinear set of vectors

TheoremA singleton set of vectors is semilinear#✓fully proved

A singleton set of vectors is semilinear.

theorem isSemilinear_singleton (b : T → ℕ) :
    IsSemilinear ({b} : Set (T → ℕ))
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 3
Statement usesSemilinear set of vectors
Proof usesLinear sets are semilinear · A singleton set of vectors is linear

TheoremSemilinear sets are closed under union#✓fully proved

Semilinear sets are closed under union.

theorem IsSemilinear.union {S S' : Set (T → ℕ)}
    (hS : IsSemilinear S) (hS' : IsSemilinear S') :
    IsSemilinear (S ∪ S')
Sources
  • Parikh, "On context-free languages", Journal of the ACM 13 (1966), 570-581.
Uses 2
Statement usesSemilinear set of vectors
Proof usesLinear set of vectors
19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.