Emptiness of context-free and regular intersections

14 fully proved

The procedure

DefinitionWhether a symbol fits at a DFA state#✓fully proved

Let \(D\) be an encoded DFA, \(R\) and \(S\) lists of natural numbers (the items found so far and the states where the rest of a right-hand side can start), \(X\) a grammar symbol and \(p \in \mathbb{N}\). The test is true exactly when either \(X\) is a terminal \(a\) and the step of \(D\) from \(p\) on \(a\) lies in \(S\), or \(X\) is a nonterminal \(B\) and some \(k\) in \(S\) has \(\langle B, \langle p, k \rangle \rangle\) in \(R\), where \(\langle \cdot, \cdot \rangle\) is the natural-number pairing.

def dfaSymFits (D : EncodedDFA T) (R S : List ℕ) (X : ℕ ⊕ T) (p : ℕ) : Bool :=
  match X with
  | .inr a => Decidability.memB S (D.step p a)
  | .inl B => S.any fun k => Decidability.memB R (Nat.pair B (Nat.pair p k))

Uses 3 · Used by 7

Statement usesEncoded DFA · Transition function of an encoded DFA · Boolean membership test for lists of natural numbers

Used byInclusion of a regular language in a DFA language is decidable · Start states of a right-hand side in a DFA · Start states of a right-hand side are states of the DFA · Correctness of the intersection-emptiness test · Completeness of the start states in a DFA · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable

DefinitionStart states of a right-hand side in a DFA#✓fully proved

Let \(D\) be an encoded DFA, \(R\) a list of natural numbers (the items found so far) and \(q \in \mathbb{N}\). The start states of a right-hand side \(\beta\), a list of grammar symbols, for \(q\) given \(R\) are defined by recursion on \(\beta\): for the empty right-hand side they are the one-element list \([q]\), and for a symbol \(X\) followed by \(\beta'\) they are the states of \(D\), in order, at which \(X\) fits given \(R\) and the start states of \(\beta'\) for \(q\) given \(R\).

def dfaStarts (D : EncodedDFA T) (R : List ℕ) (q : ℕ) (rhs : List (ℕ ⊕ T)) : List ℕ :=
  rhs.foldr (fun X S => D.states.filter (dfaSymFits D R S X)) [q]

Uses 3 · Used by 7

Statement usesEncoded DFA · States of an encoded DFA · Whether a symbol fits at a DFA state

Used byInclusion of a regular language in a DFA language is decidable · Start states of a right-hand side are states of the DFA · One round of the item search against a DFA · Correctness of the intersection-emptiness test · Completeness of the start states in a DFA · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable

DefinitionOne round of the item search against a DFA#✓fully proved

For an encoded grammar \(g\), an encoded DFA \(D\) and a list \(R\) of natural numbers (the items found so far), one round produces the list of the codes \(\langle A, \langle p, q \rangle \rangle\), where \(\langle \cdot, \cdot \rangle\) is the natural-number pairing, for every production \(A \to \beta\) of \(g\), every state \(q\) of \(D\) and every start state \(p\) of \(\beta\) for \(q\) given \(R\).

def dfaStep (g : EncodedCFG T) (D : EncodedDFA T) (R : List ℕ) : List ℕ :=
  g.rules.flatMap fun e => D.states.flatMap fun q =>
    (dfaStarts D R q e.2).map fun p => Nat.pair e.1 (Nat.pair p q)

Uses 4 · Used by 6

Statement usesEncoded DFA · States of an encoded DFA · Encoded context-free grammars · Start states of a right-hand side in a DFA

Used byInclusion of a regular language in a DFA language is decidable · Items found for a grammar and a DFA · Correctness of the intersection-emptiness test · Completeness of the start states in a DFA · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable

DefinitionCandidate items for a grammar and a DFA#✓fully proved

For an encoded grammar \(g\) and an encoded DFA \(D\), the candidate items form the list of the codes \(\langle A, \langle p, q \rangle \rangle\), where \(\langle \cdot, \cdot \rangle\) is the natural-number pairing, for every left-hand side \(A\) of a production of \(g\) (listed once per production) and all states \(p\) and \(q\) of \(D\).

def dfaItems (g : EncodedCFG T) (D : EncodedDFA T) : List ℕ :=
  (g.rules.map Prod.fst).flatMap fun A => D.states.flatMap fun q =>
    D.states.map fun p => Nat.pair A (Nat.pair p q)

Uses 3 · Used by 6

Statement usesEncoded DFA · States of an encoded DFA · Encoded context-free grammars

Used byInclusion of a regular language in a DFA language is decidable · Items found for a grammar and a DFA · Correctness of the intersection-emptiness test · Completeness of the start states in a DFA · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable

DefinitionItems found for a grammar and a DFA#✓fully proved

For an encoded grammar \(g\) and an encoded DFA \(D\), the found items are the list obtained from the empty list by applying one round of the item search of \(g\) and \(D\) as many times as the length of the list of candidate items of \(g\) and \(D\).

def dfaFound (g : EncodedCFG T) (D : EncodedDFA T) : List ℕ :=
  (dfaStep g D)^[(dfaItems g D).length] []

Uses 4 · Used by 6

Statement usesEncoded DFA · Encoded context-free grammars · Candidate items for a grammar and a DFA · One round of the item search against a DFA

Used byInclusion of a regular language in a DFA language is decidable · The intersection-emptiness test for a grammar and a DFA · Correctness of the intersection-emptiness test · Completeness of the start states in a DFA · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable

DefinitionThe intersection-emptiness test for a grammar and a DFA#✓fully proved

Let \(g\) be an encoded grammar with start nonterminal \(S\), let \(D\) be an encoded DFA with start state \(s\), and write \(\langle \cdot, \cdot \rangle\) for the natural-number pairing. The test of \(g\) and \(D\) is true exactly when there is no accepting state \(f\) of \(D\) that is also one of the states of \(D\) and for which the code \(\langle S, \langle s, f \rangle \rangle\) is among the found items of \(g\) and \(D\).

def interEmptyB (g : EncodedCFG T) (D : EncodedDFA T) : Bool :=
  !(D.accept.any fun f => Decidability.memB D.states f &&
    Decidability.memB (dfaFound g D) (Nat.pair g.start (Nat.pair D.start f)))

Uses 5 · Used by 6

Statement usesEncoded DFA · States of an encoded DFA · Boolean membership test for lists of natural numbers · Encoded context-free grammars · Items found for a grammar and a DFA

Used byInclusion of a regular language in a DFA language is decidable · Correctness of the intersection-emptiness test · The inclusion test for a grammar and a DFA · Correctness of the inclusion test · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable

Stabilization

TheoremStart states of a right-hand side are states of the DFA#✓fully proved

Let \(D\) be an encoded DFA, \(R\) a list of natural numbers and \(q\) one of the states of \(D\). Then for every right-hand side \(\beta\), every start state of \(\beta\) for \(q\) given \(R\) is one of the states of \(D\).

theorem dfaStarts_subset {D : EncodedDFA T} {R : List ℕ} {q : ℕ} (hq : q ∈ D.states)
    (rhs : List (ℕ ⊕ T)) : ∀ p ∈ dfaStarts D R q rhs, p ∈ D.states

Uses 4 · Used by 1

Statement usesEncoded DFA · States of an encoded DFA · Start states of a right-hand side in a DFA

Proof usesWhether a symbol fits at a DFA state

Used byCompleteness of the start states in a DFA

Soundness

DefinitionSound items for a grammar and a DFA#✓fully proved

For an encoded grammar \(g\) and an encoded DFA \(D\), a natural number \(x\) is a sound item when there are natural numbers \(A\), \(p\), \(q\) and a word \(w\) such that \(x = \langle A, \langle p, q \rangle \rangle\), where \(\langle \cdot, \cdot \rangle\) is the natural-number pairing, the nonterminal \(A\) yields \(w\) in the grammar denoted by \(g\), and the automaton denoted by \(D\), run on \(w\) from state \(p\), ends in state \(q\).

def DfaSoundItem (g : EncodedCFG T) (D : EncodedDFA T) (x : ℕ) : Prop :=
  ∃ A p q w, x = Nat.pair A (Nat.pair p q) ∧ Yields g.toCFG [.nonterminal A] w ∧
    D.toDFA.evalFrom p w = q

Uses 5 · Used by 1

Statement usesEncoded DFA · The automaton denoted by an encoded DFA · Encoded context-free grammars · Grammar denoted by an encoding · Yield of a sentential form

Used byCorrectness of the intersection-emptiness test

Completeness

TheoremCompleteness of the start states in a DFA#✓fully proved

Let \(g\) be an encoded context-free grammar and \(D\) an encoded DFA over an alphabet \(T\) with decidable equality, and let \(\rho\) be an encoded right-hand side whose decoding yields a word \(u\) in the grammar that \(g\) denotes. If \(p\) is one of the states of \(D\) and the automaton that \(D\) denotes, run on \(u\) from state \(p\), ends in state \(q\), then \(p\) is a start state of \(\rho\) for \(q\) given the items found for \(g\) and \(D\).

theorem mem_dfaStarts_of_yields {g : EncodedCFG T} {D : EncodedDFA T}
    {β : List (Symbol T g.toCFG.NT)} {u : List T} (h : Yields g.toCFG β u) :
    ∀ (rhs : List (ℕ ⊕ T)) (p q : ℕ), β = rhs.map decodeSymbol → p ∈ D.states →
      D.toDFA.evalFrom p u = q → p ∈ dfaStarts D (dfaFound g D) q rhs

Uses 18 · Used by 1

Statement usesEncoded DFA · States of an encoded DFA · The automaton denoted by an encoded DFA · Encoded context-free grammars · Decoding a grammar symbol · Items found for a grammar and a DFA · Start states of a right-hand side in a DFA · Grammar denoted by an encoding · Yield of a sentential form

Proof usesTransition function of an encoded DFA · The listed states are closed under transitions · Bounded monotone rounds on lists close off · Boolean membership test for lists of natural numbers · Decoding a production · Candidate items for a grammar and a DFA · Start states of a right-hand side are states of the DFA · One round of the item search against a DFA · Whether a symbol fits at a DFA state

Used byCorrectness of the intersection-emptiness test

TheoremCorrectness of the intersection-emptiness test#✓fully proved

For every encoded grammar \(g\) and every encoded DFA \(D\), the intersection-emptiness test of \(g\) and \(D\) returns true if and only if the intersection of the language of \(g\) and the language of \(D\) is empty.

theorem interEmptyB_iff {g : EncodedCFG T} {D : EncodedDFA T} :
    interEmptyB g D = true ↔ g.language ⊓ D.language = 0

Uses 24 · Used by 2

Statement usesEncoded DFA · Language of an encoded DFA · Encoded context-free grammars · The intersection-emptiness test for a grammar and a DFA · Language of an encoded grammar

Proof usesStates of an encoded DFA · Transition function of an encoded DFA · The listed states are closed under transitions · The automaton denoted by an encoded DFA · Boolean membership test for lists of natural numbers · Sound items for a grammar and a DFA · Decoding a production · Decoding a grammar symbol · Items found for a grammar and a DFA · Candidate items for a grammar and a DFA · Start states of a right-hand side in a DFA · One round of the item search against a DFA · Whether a symbol fits at a DFA state · Completeness of the start states in a DFA · Grammar denoted by an encoding · Yield of a sentential form · Concatenation of yields · Language membership through yields · Yield through one production

Used byCorrectness of the inclusion test · Emptiness of the intersection of a context-free and a regular language is decidable

DefinitionThe inclusion test for a grammar and a DFA#✓fully proved

For an encoded context-free grammar \(g\) and an encoded DFA \(D\) over the same alphabet \(T\), where \(T\) has decidable equality, the inclusion test on \(g\) and \(D\) is the Boolean value of the emptiness test on \(g\) and the complement of \(D\).

def subsetB (g : EncodedCFG T) (D : EncodedDFA T) : Bool :=
  interEmptyB g D.compl

Uses 4 · Used by 4

Statement usesEncoded DFA · Complement of an encoded DFA · Encoded context-free grammars · The intersection-emptiness test for a grammar and a DFA

Used byInclusion test · Inclusion of a regular language in a DFA language is decidable · Correctness of the inclusion test · Inclusion of a context-free language in a regular language is decidable

TheoremCorrectness of the inclusion test#✓fully proved

For every alphabet \(T\) with decidable equality, every encoded context-free grammar \(g\) over \(T\) and every encoded DFA \(D\) over \(T\), the inclusion test on \(g\) and \(D\) returns true if and only if the language of \(g\) is contained in the language of \(D\).

theorem subsetB_iff {g : EncodedCFG T} {D : EncodedDFA T} :
    subsetB g D = true ↔ g.language ≤ D.language

Uses 9 · Used by 2

Statement usesEncoded DFA · Language of an encoded DFA · Encoded context-free grammars · Language of an encoded grammar · The inclusion test for a grammar and a DFA

Proof usesComplement of an encoded DFA · The complement DFA accepts the complement language · The intersection-emptiness test for a grammar and a DFA · Correctness of the intersection-emptiness test

Used byInclusion of a regular language in a DFA language is decidable · Inclusion of a context-free language in a regular language is decidable

Computability

TheoremEmptiness of the intersection of a context-free and a regular language is decidable#✓fully proved

For every alphabet \(T\) with decidable equality and a primitive recursive encoding, the property of a pair \((g, D)\), where \(g\) is an encoded context-free grammar over \(T\) and \(D\) is an encoded DFA over \(T\), that the intersection of the language of \(g\) and the language of \(D\) is empty is decidable by a multi-stack machine.

theorem tm2Decidable_inter_eq_zero :
    TM2Decidable fun p : EncodedCFG T × EncodedDFA T => p.1.language ⊓ p.2.language = 0

Uses 20

Statement usesEncoded DFA · Encoded DFAs as triples · Language of an encoded DFA · Decidability by multi-stack machines · Encoded context-free grammars · Encoded grammars as pairs · Language of an encoded grammar

Proof usesThe transition function of encoded DFAs is primitive recursive · States of an encoded DFA · Transition function of an encoded DFA · Predicates with a primitive recursive decision procedure are computable · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates · Items found for a grammar and a DFA · Candidate items for a grammar and a DFA · Start states of a right-hand side in a DFA · One round of the item search against a DFA · Whether a symbol fits at a DFA state · The intersection-emptiness test for a grammar and a DFA · Correctness of the intersection-emptiness test

TheoremInclusion of a context-free language in a regular language is decidable#✓fully proved

For every alphabet \(T\) with decidable equality and a primitive recursive encoding, the property of a pair \((g, D)\), where \(g\) is an encoded context-free grammar over \(T\) and \(D\) is an encoded DFA over \(T\), that the language of \(g\) is contained in the language of \(D\) is decidable by a multi-stack machine.

theorem tm2Decidable_language_le :
    TM2Decidable fun p : EncodedCFG T × EncodedDFA T => p.1.language ≤ p.2.language

Uses 23

Statement usesEncoded DFA · Encoded DFAs as triples · Language of an encoded DFA · Decidability by multi-stack machines · Encoded context-free grammars · Encoded grammars as pairs · Language of an encoded grammar

Proof usesComplement of an encoded DFA · Assembling an encoded DFA is primitive recursive · The transition function of encoded DFAs is primitive recursive · States of an encoded DFA · Transition function of an encoded DFA · Predicates with a primitive recursive decision procedure are computable · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates · Items found for a grammar and a DFA · Candidate items for a grammar and a DFA · Start states of a right-hand side in a DFA · One round of the item search against a DFA · Whether a symbol fits at a DFA state · The intersection-emptiness test for a grammar and a DFA · The inclusion test for a grammar and a DFA · Correctness of the inclusion test

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.