Formal languages

DefinitionLanguage#

A language is a set of strings over an alphabet.

Language.{u_4} (α : Type u_4) : Type u_4
Sources
MathlibLanguage
Uses 2 · Used by 3
Statement usesList · Set
Used byArden's lemma · Context-free language · Regular language

TheoremArden's lemma#

Arden's lemma

Language.self_eq_mul_add_iff.{u_1} {α : Type u_1} {l m n : Language α} (hm : [] ∉ m) :
  l = m * l + n ↔ l = KStar.kstar m * n
Sources
MathlibLanguage.self_eq_mul_add_iff
Uses 2
Statement usesLanguage
Proof usesNatural number

DefinitionRegular language#

A regular language is a language that is defined by a DFA with finite states.

Language.IsRegular.{u} {T : Type u} (L : Language T) : Prop
Sources
MathlibLanguage.IsRegular
Uses 3 · Used by 1
Statement usesDFA · Finite set · Language
Used byMyhill–Nerode theorem

StructureDFA#

A DFA is a set of states (σ), a transition function from state to state labelled by the alphabet (step), a starting state (start) and a set of acceptance states (accept).

DFA.{u, v} (α : Type u) (σ : Type v) : Type (max u v)
Sources
MathlibDFA
Uses 1 · Used by 1
Statement usesSet
Used byRegular language

StructureNFA#

An NFA is a set of states (σ), a transition function from state to state labelled by the alphabet (step), a set of starting states (start) and a set of acceptance states (accept). Note the transition function sends a state to a Set of states. These are the states that it may be sent to.

NFA.{u, v} (α : Type u) (σ : Type v) : Type (max u v)
Sources
MathlibNFA
Uses 1
Statement usesSet

Structure\(\varepsilon\)-NFA#

An εNFA is a set of states (σ), a transition function from state to state labelled by the alphabet (step), a starting state (start) and a set of acceptance states (accept). Note the transition function sends a state to a Set of states and can make ε-transitions by inputting none. Since this definition allows for Automata with infinite states, a Fintype instance must be supplied for true εNFA's.

εNFA.{u, v} (α : Type u) (σ : Type v) : Type (max u v)
Sources
MathlibεNFA
Uses 1
Statement usesSet

InductiveRegular expression#

This is the definition of regular expressions. The names used here are meant to mirror the definition of a Kleene algebra. * 0 (zero) matches nothing * 1 (epsilon) matches only the empty string * char a matches only the string 'a' * star P matches any finite concatenation of strings that match P * P + Q (plus P Q) matches anything that matches P or Q * P * Q (comp P Q) matches x ++ y if x matches P and y matches Q

RegularExpression.{u} (α : Type u) : Type u
Sources
MathlibRegularExpression

DefinitionContext-free language#

Context-free languages are defined by context-free grammars.

Language.IsContextFree.{u_1} {T : Type u_1} (L : Language T) : Prop
Sources
MathlibLanguage.IsContextFree
Uses 2
Statement usesContext-free grammar · Language

StructureContext-free grammar#

Context-free grammar that generates words over the alphabet T (a type of terminals).

ContextFreeGrammar.{u_1} (T : Type u_1) : Type (max 1 u_1)
Sources
MathlibContextFreeGrammar
Uses 1 · Used by 1
Statement usesFinite set
Used byContext-free language

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.