Formal Language Classification

Framework-agnostic classification of formal languages by generative capacity. This is the single canonical definition used throughout the library — phenomenon data files, theory modules, and study files all import this type rather than defining their own.

The four levels reflect the Chomsky hierarchy as relevant to natural language: regular (FSA), context-free (CFG), mildly context-sensitive (CCG, TAG, etc.), and context-sensitive (CSG).

inductive Core.FormalLanguageType : Type

Classification of formal languages by generative capacity.

• regular: generated by finite-state automata / regular grammars
• contextFree: generated by context-free grammars (CFGs)
• mildlyContextSensitive: beyond CFG but polynomially parsable (CCG, TAG)
• contextSensitive: full context-sensitive grammar power

• regular : FormalLanguageType
• contextFree : FormalLanguageType
• mildlyContextSensitive : FormalLanguageType
• contextSensitive : FormalLanguageType

instance Core.instDecidableEqFormalLanguageType : DecidableEq FormalLanguageType

Equations

• Core.instDecidableEqFormalLanguageType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.instBEqFormalLanguageType.beq : FormalLanguageType → FormalLanguageType → Bool

Equations

• Core.instBEqFormalLanguageType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.instBEqFormalLanguageType : BEq FormalLanguageType

Equations

• Core.instBEqFormalLanguageType = { beq := Core.instBEqFormalLanguageType.beq }

instance Core.instReprFormalLanguageType : Repr FormalLanguageType

Equations

• Core.instReprFormalLanguageType = { reprPrec := Core.instReprFormalLanguageType.repr }

def Core.instReprFormalLanguageType.repr : FormalLanguageType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Core.FormalLanguageType.toNat : FormalLanguageType → Nat

Numeric encoding for the Chomsky hierarchy ordering.

Equations

• Core.FormalLanguageType.regular.toNat = 0
• Core.FormalLanguageType.contextFree.toNat = 1
• Core.FormalLanguageType.mildlyContextSensitive.toNat = 2
• Core.FormalLanguageType.contextSensitive.toNat = 3

instance Core.instLTFormalLanguageType : LT FormalLanguageType

Equations

• Core.instLTFormalLanguageType = { lt := fun (a b : Core.FormalLanguageType) => a.toNat < b.toNat }

instance Core.instLEFormalLanguageType : LE FormalLanguageType

Equations

• Core.instLEFormalLanguageType = { le := fun (a b : Core.FormalLanguageType) => a.toNat ≤ b.toNat }

instance Core.instDecidableLtFormalLanguageType (a b : FormalLanguageType) : Decidable (a < b)

Equations

• Core.instDecidableLtFormalLanguageType a b = inferInstanceAs (Decidable (a.toNat < b.toNat))

instance Core.instDecidableLeFormalLanguageType (a b : FormalLanguageType) : Decidable (a ≤ b)

Equations

• Core.instDecidableLeFormalLanguageType a b = inferInstanceAs (Decidable (a.toNat ≤ b.toNat))

theorem Core.FormalLanguageType.hierarchy : regular < contextFree ∧ contextFree < mildlyContextSensitive ∧ mildlyContextSensitive < contextSensitive

The proper inclusion chain: regular ⊂ CF ⊂ MCS ⊂ CS.