Generation properties for classes of languages

Paper-independent quantifier patterns for generation from positive data over an arbitrary example type.

def GenLimit.Generic.UUS {α : Type u_1} (H : LanguageClass α) : Prop

Every language in the class is infinite.

Equations

• GenLimit.Generic.UUS H = ∀ L ∈ H, Set.Infinite L

def GenLimit.Generic.IsLimitGenerator {α : Type u_1} (gen : Generator α) (H : LanguageClass α) : Prop

gen eventually generates fresh elements of every presented target.

Equations

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

def GenLimit.Generic.GeneratableInLimit {α : Type u_1} (H : LanguageClass α) : Prop

Generation in the limit from positive presentations.

Equations

• GenLimit.Generic.GeneratableInLimit H = ∃ (gen : GenLimit.Generic.Generator α), GenLimit.Generic.IsLimitGenerator gen H

def GenLimit.Generic.IsUniformGeneratorAt {α : Type u_1} (gen : Generator α) (H : LanguageClass α) (d : ℕ) : Prop

d is a uniform distinct-sample threshold for gen on H.

Equations

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

def GenLimit.Generic.UniformlyGeneratable {α : Type u_1} (H : LanguageClass α) : Prop

One generator and one threshold work uniformly over the class.

Equations

• GenLimit.Generic.UniformlyGeneratable H = ∃ (gen : GenLimit.Generic.Generator α) (d : ℕ), GenLimit.Generic.IsUniformGeneratorAt gen H d

def GenLimit.Generic.IsNonuniformGenerator {α : Type u_1} (gen : Generator α) (H : LanguageClass α) : Prop

One generator works with a target-dependent distinct-sample threshold.

Equations

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

def GenLimit.Generic.NonuniformlyGeneratable {α : Type u_1} (H : LanguageClass α) : Prop

One generator works with target-dependent thresholds.

Equations

• GenLimit.Generic.NonuniformlyGeneratable H = ∃ (gen : GenLimit.Generic.Generator α), GenLimit.Generic.IsNonuniformGenerator gen H

theorem GenLimit.Generic.uniform_implies_nonuniform {α : Type u_1} {H : LanguageClass α} (h : UniformlyGeneratable H) : NonuniformlyGeneratable H

theorem GenLimit.Generic.nonuniform_implies_limit {α : Type u_1} {H : LanguageClass α} (hUUS : UUS H) (h : NonuniformlyGeneratable H) : GeneratableInLimit H

theorem GenLimit.Generic.uniform_implies_limit {α : Type u_1} {H : LanguageClass α} (hUUS : UUS H) (h : UniformlyGeneratable H) : GeneratableInLimit H