Deterministic Context-Free Languages (DCFs) #

This file defines deterministic context-free languages (DCFs) as a grammar class and proves their basic inclusion into context-free languages.

Definition #

A language L is a deterministic context-free language (DCF) if there exists a deterministic pushdown automaton (DPDA) that accepts L by final-state acceptance.

Main results #

is_CF_of_is_DCF — Every DCF is context-free.
lang_aibjck_eq_union — The language {aⁱbʲcᵏ | i = j ∨ j = k} equals the union of two CFLs.
lang_aibjck_CFL — The language {aⁱbʲcᵏ | i = j ∨ j = k} is context-free.

References #

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

source

def is_DCF {T : Type} [Fintype T] (L : Language T) :

Prop

A language L over a finite alphabet T is a deterministic context-free language (DCF) if there exists a DPDA that recognizes L via final-state acceptance.

Equations

is_DCF L = is_DPDA L

Instances For

source

def DCF {T : Type} [Fintype T] :

Set (Language T)

The class of languages that are DCF