Documentation

LeanPool.DomainTheory.Neighborhood.Example24

Example 2.4 (Scott 1981, PRG-19, §2) — eliminating the first run of 1's, `g : #

B → B`

Scott's second approximable mapping reads a binary sequence left to right and "eliminates the first consecutive run of 1's while copying all the other digits." Thus

g(0ⁿ 1ᵏ 0 x) = 0ⁿ⁺¹ x (for k > 0), g(1^∞) = ⊥, g(0ⁿ 1^∞) = 0ⁿ.

It is instructive because it turns total inputs (e.g. 1^∞) into partial outputs.

We give the guaranteed finite output out : Σ* → Σ* for each finite input prefix via a two-state scan: out copies leading 0's and, on the first 1, hands over to del, which swallows the run of 1's and — on the terminating 0 — emits that single 0 and copies the rest verbatim. The elementwise value on the finite element ↑(σΣ*) is ↑((out σ)Σ*), so the neighbourhood relation is

X g Y ↔ ∃ σ, X = σΣ* ∧ (out σ)Σ* ⊆ Y ∧ Y ∈ B.

out is prefix-monotone (out_mono: σ <+: σ' → out σ <+: out σ'), which gives Definition 2.1(iii); (i) and (ii) are the principal-filter facts for the cone (out σ)Σ*. Constructive.

source
def Domain.Neighborhood.Example24.del :
ExampleB.Str → ExampleB.Str

Inside the first run of 1's: swallow 1's; on the first 0, emit it and copy the rest.

Equations
Instances For
    source
    @[simp]
    theorem Domain.Neighborhood.Example24.del_nil :
    del [] = []
    source
    @[simp]
    theorem Domain.Neighborhood.Example24.del_true (t : ExampleB.Str) :
    del (true :: t) = del t
    source
    @[simp]
    theorem Domain.Neighborhood.Example24.del_false (t : ExampleB.Str) :
    del (false :: t) = false :: t
    source
    def Domain.Neighborhood.Example24.out :
    ExampleB.Str → ExampleB.Str

    The guaranteed output prefix: copy leading 0's; on the first 1, eliminate the run via del.

    Equations
    Instances For
      source
      @[simp]
      theorem Domain.Neighborhood.Example24.out_nil :
      out [] = []
      source
      @[simp]
      theorem Domain.Neighborhood.Example24.out_false (t : ExampleB.Str) :
      out (false :: t) = false :: out t
      source
      @[simp]
      theorem Domain.Neighborhood.Example24.out_true (t : ExampleB.Str) :
      out (true :: t) = del t
      source
      theorem Domain.Neighborhood.Example24.del_append (s t : ExampleB.Str) :
      del s <+: del (s ++ t)

      del only grows under extension: del s <+: del (s ++ t).

      source
      theorem Domain.Neighborhood.Example24.out_append (σ t : ExampleB.Str) :
      out σ <+: out (σ ++ t)

      out only grows under extension: out σ <+: out (σ ++ t).

      source
      theorem Domain.Neighborhood.Example24.out_mono {σ σ' : ExampleB.Str} (h : σ <+: σ') :
      out σ <+: out σ'

      Prefix-monotonicity of the output. Extending the input prefix can only extend the guaranteed output: σ <+: σ' → out σ <+: out σ'. This is the heart of Definition 2.1(iii) for g.

      source
      def Domain.Neighborhood.Example24.runMap :
      ApproximableMap ExampleB.B ExampleB.B

      Example 2.4 — the run-eliminating mapping g : B → B. X g Y iff X = σΣ* and the cone of the guaranteed output (out σ)Σ* approximates Y. Definition 2.1: (i) out [] = [] so Δ g Δ; (ii) a fixed cone has a unique prefix, and the value is the principal filter ↑((out σ)Σ*), closed under ∩; (iii) out_mono shrinks the output cone as the input cone shrinks.

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