Docking processes

A docking process is the positional rewrite of the subregular program ([Cha14a], [CJ19]) with its context left semantic: what docking does to a position's symbol, and a decidable predicate saying at which positions of a word it docks; the other positions keep their symbol. It is the string function a relabelling transduction computes, and the object over which locality is stated once: when the context is a quantifier-free formula bounded by l back and r forward, the output at a position reads only that window, so the map depends boundedly on both sides in the sense of Subregular.BoundedDependence.

Main definitions

• Docking, Docking.map — the process and its rewrite; Docking.support, the docking set.
• Docking.ofQF — the process with a quantifier-free context.

Main results

• Docking.map_getElem? — the rewrite pointwise.
• Docking.requiresBothSides_of_flanks — the flank-witness template, from three docking facts.
• Docking.ofQF_map_getElem?_congr — with a bounded guard, the output at a position reads only the guard's window.
• Docking.ofQF_boundedDependence — hence bounded dependence on both sides.

References

• [Cha14a]
• [CJ19]

structure Subregular.Docking (α : Type u_1) : Type u_1

A docking process over the alphabet α is what docking does to a position's symbol, together with the context predicate saying at which positions of a word it docks; the other positions keep their symbol.

• dock : α → α

  dock a is the change docked at a position holding a.

• Docks : List α → ℕ → Prop

  Position i of w is docked at.

• lt_length {w : List α} {i : ℕ} : self.Docks w i → i < w.length

  Docking positions are in-domain.

• decDocks (w : List α) (i : ℕ) : Decidable (self.Docks w i)

  The context predicate is decidable, so the map computes.

@[instance_reducible]

instance Subregular.Docking.instDecidableDocks {α : Type u_1} (P : Docking α) (w : List α) (i : ℕ) : Decidable (P.Docks w i)

Equations

• P.instDecidableDocks w i = P.decDocks w i

def Subregular.Docking.map {α : Type u_1} (P : Docking α) (w : List α) : List α

The induced rewrite docks the change exactly at the docking positions.

Equations

• P.map w = List.mapIdx (fun (i : ℕ) (a : α) => if P.Docks w i then P.dock a else a) w

@[simp]

theorem Subregular.Docking.map_nil {α : Type u_1} (P : Docking α) : P.map [] = []

@[simp]

theorem Subregular.Docking.map_length {α : Type u_1} (P : Docking α) {w : List α} : (P.map w).length = w.length

theorem Subregular.Docking.map_getElem? {α : Type u_1} (P : Docking α) {w : List α} {i : ℕ} : (P.map w)[i]? = Option.map (fun (a : α) => if P.Docks w i then P.dock a else a) w[i]?

theorem Subregular.Docking.map_getElem?_of_docks {α : Type u_1} (P : Docking α) {w : List α} {i : ℕ} (h : P.Docks w i) : (P.map w)[i]? = Option.map P.dock w[i]?

theorem Subregular.Docking.map_getElem?_of_not_docks {α : Type u_1} (P : Docking α) {w : List α} {i : ℕ} (h : ¬P.Docks w i) : (P.map w)[i]? = w[i]?

def Subregular.Docking.support {α : Type u_1} (P : Docking α) (w : List α) : Finset ℕ

P.support w is the finite set of docking positions of w.

Equations

• P.support w = Finset.filter (P.Docks w) (Finset.range w.length)

@[simp]

theorem Subregular.Docking.mem_support {α : Type u_1} (P : Docking α) {w : List α} {i : ℕ} : i ∈ P.support w ↔ P.Docks w i

theorem Subregular.Docking.requiresBothSides_of_flanks {α : Type u_1} (P : Docking α) {fill xOn yOn xOff yOff : α} {n t : ℕ → ℕ} (hfill : P.dock fill ≠ fill) (ht : ∀ (d : ℕ), d < t d) (hn : ∀ (d : ℕ), t d + d ≤ n d) (hon : ∀ (d : ℕ), P.Docks (flankWord xOn fill yOn (n d)) (t d)) (hoffL : ∀ (d : ℕ), ¬P.Docks (flankWord xOff fill yOn (n d)) (t d)) (hoffR : ∀ (d : ℕ), ¬P.Docks (flankWord xOn fill yOff (n d)) (t d)) : RequiresBothSides P.map

The flank-witness template at the docking level. A process that docks a change of the filler at a d-margined target of a flank word, and does not dock there when either flank alone is flipped, requires both sides.

Quantifier-free contexts

def Subregular.Docking.ofQF {α : Type u_1} [DecidableEq α] (φ : WindowFormula α) (dock : α → α) : Docking α

The docking process whose context is a quantifier-free formula.

Equations

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

theorem Subregular.Docking.ofQF_map_getElem?_congr {α : Type u_1} {i : ℕ} [DecidableEq α] {φ : WindowFormula α} {l r : ℕ} (hφ : WindowFormula.Bounded l r φ) (dock : α → α) {w w' : List α} (hlen : w.length = w'.length) (hag : ∀ (j : ℕ), i - l ≤ j → j ≤ i + r → w[j]? = w'[j]?) : ((ofQF φ dock).map w)[i]? = ((ofQF φ dock).map w')[i]?

With a guard bounded by l back and r forward, the output at a position reads only the input on that window.

theorem Subregular.Docking.ofQF_boundedDependence_left {α : Type u_1} [DecidableEq α] {φ : WindowFormula α} {l r : ℕ} (hφ : WindowFormula.Bounded l r φ) (dock : α → α) : BoundedDependence (ofQF φ dock).map Edge.left

A quantifier-free docking process with a bounded guard depends boundedly on the left.

theorem Subregular.Docking.ofQF_boundedDependence_right {α : Type u_1} [DecidableEq α] {φ : WindowFormula α} {l r : ℕ} (hφ : WindowFormula.Bounded l r φ) (dock : α → α) : BoundedDependence (ofQF φ dock).map Edge.right

A quantifier-free docking process with a bounded guard depends boundedly on the right.