Recursively Enumerable Languages

This file defines the class of recursively enumerable languages via unrestricted grammars.

def is_RE {T : Type} (L : Language T) : Prop

Predicate that a language is recursively enumerable.

Equations

• is_RE L = ∃ (g : grammar T), grammar_language g = L

def RE {T : Type} : Set (Language T)

The class of recursively enumerable languages.

Equations

• RE = setOf is_RE