Language generation in the limit: basic definitions

This file fixes a countable universe ℕ and an indexed family of languages. The family is indexed, rather than represented as a set of sets, because the Kleinberg--Mullainathan algorithm depends on the enumeration order and permits repeated languages.

@[reducible, inline]

abbrev GenLimit.Language : Type

A language over the countable universe ℕ.

Equations

• GenLimit.Language = Set ℕ

@[reducible, inline]

abbrev GenLimit.LanguageFamily : Type

An indexed family of languages. Repeated languages are permitted.

Equations

• GenLimit.LanguageFamily = (ℕ → GenLimit.Language)

def GenLimit.Presents (stream : ℕ → ℕ) (L : Language) : Prop

A stream is an exact presentation of L when its range is exactly L.

Equations

• GenLimit.Presents stream L = (Set.range stream = L)

def GenLimit.sample (stream : ℕ → ℕ) (t : ℕ) : Finset ℕ

The set of observations strictly before time t.

Equations

• GenLimit.sample stream t = Finset.image stream (Finset.range t)

def GenLimit.Consistent (C : LanguageFamily) (stream : ℕ → ℕ) (t i : ℕ) : Prop

Candidate i is consistent with all observations strictly before t.

Equations

• GenLimit.Consistent C stream t i = (↑(GenLimit.sample stream t) ⊆ C i)

structure GenLimit.MembershipOracle (C : LanguageFamily) : Type

A Boolean membership oracle, uniform in the language index and element.

• query : ℕ → ℕ → Bool

  Decide whether an element belongs to the language with the given index.

• query_spec {i u : ℕ} : self.query i u = true ↔ u ∈ C i

theorem GenLimit.mem_sample_iff {stream : ℕ → ℕ} {t u : ℕ} : u ∈ sample stream t ↔ ∃ s < t, stream s = u

theorem GenLimit.sample_mono {stream : ℕ → ℕ} {s t : ℕ} (hst : s ≤ t) : sample stream s ⊆ sample stream t

theorem GenLimit.value_mem_sample {stream : ℕ → ℕ} {s t : ℕ} (hst : s < t) : stream s ∈ sample stream t

theorem GenLimit.mem_language_of_mem_sample_of_presents {stream : ℕ → ℕ} {L : Language} (hP : Presents stream L) {t u : ℕ} (hu : u ∈ sample stream t) : u ∈ L

theorem GenLimit.consistent_of_target_subset {C : LanguageFamily} {stream : ℕ → ℕ} {z i t : ℕ} (hP : Presents stream (C z)) (hsub : C z ⊆ C i) : Consistent C stream t i

Any candidate containing the presented target is consistent at every time.

theorem GenLimit.eventually_mem_sample_of_presents {stream : ℕ → ℕ} {L : Language} (hP : Presents stream L) {u : ℕ} (hu : u ∈ L) : ∃ (T : ℕ), ∀ (t : ℕ), T ≤ t → u ∈ sample stream t

theorem GenLimit.presents_consistent {C : LanguageFamily} {stream : ℕ → ℕ} {z t : ℕ} (hP : Presents stream (C z)) : Consistent C stream t z

theorem GenLimit.eventually_not_consistent_of_not_subset {C : LanguageFamily} {stream : ℕ → ℕ} {z i : ℕ} (hP : Presents stream (C z)) (hbad : ¬C z ⊆ C i) : ∃ (T : ℕ), ∀ (t : ℕ), T ≤ t → ¬Consistent C stream t i