Deterministic context-free languages

15 fully proved

Automata

DefinitionDeterministic pushdown automaton#✓fully proved

A pushdown automaton is deterministic when every transition set has at most one element, and an available ε-transition precludes every consuming transition from the same state and stack symbol.

def PDA.IsDeterministic (M : PDA T σ Γ) : Prop :=
  (∀ (q : σ) (γ : Γ), (M.step q none γ).card ≤ 1) ∧
    (∀ (q : σ) (a : T) (γ : Γ), (M.step q (some a) γ).card ≤ 1) ∧
    ∀ (q : σ) (γ : Γ), (M.step q none γ).Nonempty →
      ∀ (a : T), M.step q (some a) γ = ∅

structure PDA (T : Type*) (σ : Type*) (Γ : Type*) where
  /-- The finitely branching transition function. -/
  step : σ → Option T → Γ → Finset (σ × List Γ)
  /-- The initial state. -/
  start : σ
  /-- The sole initial stack symbol. -/
  startStack : Γ

CSLibExt/Computability/Automata/PDA/Basic.lean:56

Sources

Sipser, Introduction to the Theory of Computation, 3rd ed., Chapter 2 (deterministic pushdown automata); Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 1 · Used by 2

Statement usesPushdown automaton

Used byDeterministic context-free languages are context-free · Deterministic context-free language

Language

DefinitionEnd-marker encoding of a word#✓fully proved

Encode a word by copying it to the left summand and appending the end marker Sum.inr ().

def endMarkerEncode (w : List T) : List (T ⊕ Unit) :=
  w.map Sum.inl ++ [Sum.inr ()]

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3 (deterministic pushdown automata, acceptance by empty stack with an end marker).

Used by 8

Used byLanguage of end-marker encoded words · Encoding DFA accepts every end-marker encoding · Injectivity of the end-marker encoding · Erasing the end-marker encoding recovers the word · Encoding DFA accepts only end-marker encodings · Deterministic context-free languages are context-free · Deterministic context-free language · End-marker encodings form a regular language

DefinitionEnd-marker erasure#✓fully proved

Erase the end marker: a left letter maps to its one-letter word, the end marker maps to the empty word.

def endMarkerErase : T ⊕ Unit → List T
  | .inl a => [a]
  | .inr _ => []

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3 (deterministic pushdown automata, acceptance by empty stack with an end marker).

Used by 3

Used byInjectivity of the end-marker encoding · Erasing the end-marker encoding recovers the word · Deterministic context-free languages are context-free

DefinitionLanguage of end-marker encoded words#✓fully proved

The encodings of words over T: the words over T ⊕ Unit consisting of left letters followed by a single end marker.

def encodedWords : Language (T ⊕ Unit) :=
  {u | ∃ w : List T, u = endMarkerEncode w}

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3 (deterministic pushdown automata, acceptance by empty stack with an end marker).

Uses 1 · Used by 2

Statement usesEnd-marker encoding of a word

Used byDeterministic context-free languages are context-free · End-marker encodings form a regular language

TheoremErasing the end-marker encoding recovers the word#✓fully proved

Erasing an encoding recovers the word.

theorem endMarkerErase_endMarkerEncode (w : List T) :
    ((endMarkerEncode w).map endMarkerErase).flatten = w

def endMarkerEncode (w : List T) : List (T ⊕ Unit) :=
  w.map Sum.inl ++ [Sum.inr ()]

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:91

def endMarkerErase : T ⊕ Unit → List T
  | .inl a => [a]
  | .inr _ => []

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:100

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 2 · Used by 2

Statement usesEnd-marker encoding of a word · End-marker erasure

Used byInjectivity of the end-marker encoding · Deterministic context-free languages are context-free

TheoremInjectivity of the end-marker encoding#✓fully proved

Encoding is injective.

theorem endMarkerEncode_injective :
    Function.Injective (endMarkerEncode (T := T))

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 3 · Used by 1

Statement usesEnd-marker encoding of a word

Proof usesEnd-marker erasure · Erasing the end-marker encoding recovers the word

Used byDeterministic context-free languages are context-free

DefinitionDFA recognizing end-marker encodings#✓fully proved

The DFA for the encodings: state inl false while reading left letters, inl true after the end marker (the accepting state), and inr () dead once anything follows the end marker.

noncomputable def endMarkerDFA : DFA (T ⊕ Unit) (Bool ⊕ Unit) where
  step := fun q c => match q, c with
    | .inl false, .inl _ => .inl false
    | .inl false, .inr _ => .inl true
    | .inl true, _ => .inr ()
    | .inr _, _ => .inr ()
  start := .inl false
  accept := {.inl true}

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Used by 6

Used byEncoding DFA after the end marker accepts only the empty input · Dead state of the encoding DFA is absorbing · Encoding DFA accepts every end-marker encoding · Encoding DFA stays in its start state on left letters · Encoding DFA accepts only end-marker encodings · End-marker encodings form a regular language

TheoremDead state of the encoding DFA is absorbing#✓fully proved

The dead state of the encoding DFA stays dead.

theorem endMarkerDFA_evalFrom_dead (u : List (T ⊕ Unit)) :
    endMarkerDFA.evalFrom (Sum.inr ()) u = Sum.inr ()

noncomputable def endMarkerDFA : DFA (T ⊕ Unit) (Bool ⊕ Unit) where
  step := fun q c => match q, c with
    | .inl false, .inl _ => .inl false
    | .inl false, .inr _ => .inl true
    | .inl true, _ => .inr ()
    | .inr _, _ => .inr ()
  start := .inl false
  accept := {.inl true}

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:143

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 1 · Used by 1

Statement usesDFA recognizing end-marker encodings

Used byEncoding DFA after the end marker accepts only the empty input

TheoremEncoding DFA stays in its start state on left letters#✓fully proved

The encoding DFA stays in its start state while reading left letters.

theorem endMarkerDFA_evalFrom_inl (w : List T) :
    endMarkerDFA.evalFrom (Sum.inl false) (w.map Sum.inl) = Sum.inl false

noncomputable def endMarkerDFA : DFA (T ⊕ Unit) (Bool ⊕ Unit) where
  step := fun q c => match q, c with
    | .inl false, .inl _ => .inl false
    | .inl false, .inr _ => .inl true
    | .inl true, _ => .inr ()
    | .inr _, _ => .inr ()
  start := .inl false
  accept := {.inl true}

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:143

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 1 · Used by 1

Statement usesDFA recognizing end-marker encodings

Used byEncoding DFA accepts every end-marker encoding

TheoremEncoding DFA after the end marker accepts only the empty input#✓fully proved

After the end marker, the encoding DFA can only be in its accepting state on empty input.

theorem endMarkerDFA_evalFrom_afterMarker {u : List (T ⊕ Unit)}
    (h : endMarkerDFA.evalFrom (Sum.inl true) u = Sum.inl true) : u = []

noncomputable def endMarkerDFA : DFA (T ⊕ Unit) (Bool ⊕ Unit) where
  step := fun q c => match q, c with
    | .inl false, .inl _ => .inl false
    | .inl false, .inr _ => .inl true
    | .inl true, _ => .inr ()
    | .inr _, _ => .inr ()
  start := .inl false
  accept := {.inl true}

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:143

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 2 · Used by 1

Statement usesDFA recognizing end-marker encodings

Proof usesDead state of the encoding DFA is absorbing

Used byEncoding DFA accepts only end-marker encodings

TheoremEncoding DFA accepts every end-marker encoding#✓fully proved

The encoding DFA accepts exactly the encodings: it reaches the accepting state on an encoding.

theorem endMarkerDFA_evalFrom_encode (w : List T) :
    endMarkerDFA.evalFrom (Sum.inl false) (endMarkerEncode w) = Sum.inl true

noncomputable def endMarkerDFA : DFA (T ⊕ Unit) (Bool ⊕ Unit) where
  step := fun q c => match q, c with
    | .inl false, .inl _ => .inl false
    | .inl false, .inr _ => .inl true
    | .inl true, _ => .inr ()
    | .inr _, _ => .inr ()
  start := .inl false
  accept := {.inl true}

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:143

def endMarkerEncode (w : List T) : List (T ⊕ Unit) :=
  w.map Sum.inl ++ [Sum.inr ()]

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:91

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 3 · Used by 1

Statement usesDFA recognizing end-marker encodings · End-marker encoding of a word

Proof usesEncoding DFA stays in its start state on left letters

Used byEnd-marker encodings form a regular language

TheoremEncoding DFA accepts only end-marker encodings#✓fully proved

The encoding DFA reaches the accepting state only on encodings.

theorem exists_endMarkerEncode_of_endMarkerDFA_evalFrom {u : List (T ⊕ Unit)}
    (h : endMarkerDFA.evalFrom (Sum.inl false) u = Sum.inl true) :
    ∃ w : List T, u = endMarkerEncode w

noncomputable def endMarkerDFA : DFA (T ⊕ Unit) (Bool ⊕ Unit) where
  step := fun q c => match q, c with
    | .inl false, .inl _ => .inl false
    | .inl false, .inr _ => .inl true
    | .inl true, _ => .inr ()
    | .inr _, _ => .inr ()
  start := .inl false
  accept := {.inl true}

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:143

def endMarkerEncode (w : List T) : List (T ⊕ Unit) :=
  w.map Sum.inl ++ [Sum.inr ()]

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:91

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 3 · Used by 1

Statement usesDFA recognizing end-marker encodings · End-marker encoding of a word

Proof usesEncoding DFA after the end marker accepts only the empty input

Used byEnd-marker encodings form a regular language

TheoremEnd-marker encodings form a regular language#✓fully proved

The encodings of words form a regular language.

theorem isRegular_encodedWords :
    (encodedWords : Language (T ⊕ Unit)).IsRegular

Sources

Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 5 · Used by 1

Statement usesLanguage of end-marker encoded words

Proof usesDFA recognizing end-marker encodings · Encoding DFA accepts every end-marker encoding · End-marker encoding of a word · Encoding DFA accepts only end-marker encodings

Used byDeterministic context-free languages are context-free

DefinitionDeterministic context-free language#✓fully proved

A language is deterministic context-free when some deterministic pushdown automaton with finite state and stack alphabets, whose transitions consume letters from a finite set, accepts by empty stack exactly the end-marker encodings of its words.

def IsDeterministicContextFree (L : Language T) : Prop :=
  ∃ (σ Γ : Type) (_ : Fintype σ) (_ : Fintype Γ) (M : PDA (T ⊕ Unit) σ Γ),
    M.IsDeterministic ∧
      (∃ T₀ : Finset (T ⊕ Unit), ∀ (p : σ) (a : T ⊕ Unit) (γ : Γ),
        a ∉ T₀ → M.step p (some a) γ = ∅) ∧
      M.accepts = (fun w : List T => endMarkerEncode w) '' L

structure PDA (T : Type*) (σ : Type*) (Γ : Type*) where
  /-- The finitely branching transition function. -/
  step : σ → Option T → Γ → Finset (σ × List Γ)
  /-- The initial state. -/
  start : σ
  /-- The sole initial stack symbol. -/
  startStack : Γ

CSLibExt/Computability/Automata/PDA/Basic.lean:56

def endMarkerEncode (w : List T) : List (T ⊕ Unit) :=
  w.map Sum.inl ++ [Sum.inr ()]

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:91

Sources

Ginsburg and Greibach, "Deterministic context free languages", Information and Control 9 (1966), 620-648; Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 4 · Used by 1

Statement usesPushdown automaton · Deterministic pushdown automaton · Language accepted by a pushdown automaton · End-marker encoding of a word

Used byDeterministic context-free languages are context-free

TheoremDeterministic context-free languages are context-free#✓fully proved

Every deterministic context-free language is context-free: the encoded language is accepted by a pushdown automaton, hence context-free; intersecting with the regular language of encodings and erasing the end marker recovers the original language.

theorem IsDeterministicContextFree.isContextFree
    (hL : IsDeterministicContextFree L) : L.IsContextFree

def IsDeterministicContextFree (L : Language T) : Prop :=
  ∃ (σ Γ : Type) (_ : Fintype σ) (_ : Fintype Γ) (M : PDA (T ⊕ Unit) σ Γ),
    M.IsDeterministic ∧
      (∃ T₀ : Finset (T ⊕ Unit), ∀ (p : σ) (a : T ⊕ Unit) (γ : Γ),
        a ∉ T₀ → M.step p (some a) γ = ∅) ∧
      M.accepts = (fun w : List T => endMarkerEncode w) '' L

CSLibExt/Computability/Languages/ContextFree/Deterministic.lean:236

Sources

Ginsburg and Greibach, "Deterministic context free languages", Information and Control 9 (1966), 620-648; Hopcroft, Motwani, and Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Section 10.3.

Uses 13

Statement usesDeterministic context-free language

Proof usesPushdown automaton · Deterministic pushdown automaton · Language accepted by a pushdown automaton · Context-free languages are closed under homomorphic images · Intersection of a context-free language with a regular language · Finite pushdown automata accept context-free languages · Language of end-marker encoded words · End-marker encoding of a word · Injectivity of the end-marker encoding · End-marker erasure · Erasing the end-marker encoding recovers the word · End-marker encodings form a regular language

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.